Theorems / novel_cat_01

Authored

Category theory · easy

Statement, exactly as the model and Lean see it
open CategoryTheory in
theorem lg_target {C : Type*} [Category C] {X Y : C} (α : X ≅ Y) : α.hom ≫ α.inv = 𝟙 X := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified1 model calls · 1 Lean checks · $0.00004

Attempts

  1. sample 0 · round 0Verified1.2 s model time
    Proof
    rw [α.hom_inv_id]

Verified proof

open CategoryTheory in
theorem lg_target {C : Type*} [Category C] {X Y : C} (α : X ≅ Y) : α.hom ≫ α.inv = 𝟙 X := by
  rw [α.hom_inv_id]

Axioms used: none

Reference proof

The proof we wrote and certified before any model ran.

simp