awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
mp :
  Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯) →
    IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
⊢ Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯) ↔
    IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
have mpr : IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry) →
  Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ S.Exact ↔ imageSubobject S.f = kernelSubobject S.g
have rw : IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry) ↔
  imageSubobject S.f = kernelSubobject S.g
Tactic: rw [exact_iff_isIso_imageToKernel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯) ↔
    imageSubobject S.f = kernelSubobject S.g
have mp : IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry) →
  imageSubobject S.f = kernelSubobject S.g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
mp :
  IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯) →
    imageSubobject S.f = kernelSubobject S.g
⊢ IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯) ↔
    imageSubobject S.f = kernelSubobject S.g
have mpr : imageSubobject S.f = kernelSubobject S.g →
  IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : imageSubobject S.f = kernelSubobject S.g
⊢ imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ =
    𝟙 (Functor.obj Subobject.underlying (imageSubobject S.f))
have h₁ : (imageToKernel S.f S.g sorry ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) sorry) ≫ (imageSubobject S.f).arrow =
  𝟙 (Functor.obj Subobject.underlying (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯ =
    𝟙 (Functor.obj Subobject.underlying (kernelSubobject S.g))
have h₁ : ((kernelSubobject S.g).ofLE (imageSubobject S.f) sorry ≫ imageToKernel S.f S.g sorry) ≫ (kernelSubobject S.g).arrow =
  𝟙 (Functor.obj Subobject.underlying (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
⊢ S.Exact ↔ Fork.ι cg ≫ Cofork.π cf = 0
have rw : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
Tactic: rw [exact_iff_kernel_ι_comp_cokernel_π_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
have eq₁ : CategoryStruct.comp (Y := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) sorry))
    (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
    (NatTrans.app (Cone.π (Fork.ofι (P := kernel S.g) (kernel.ι S.g) sorry)) WalkingParallelPair.zero) =
  cg.π.app WalkingParallelPair.zero
Tactic: have eq₁ := IsLimit.conePointUniqueUpToIso_inv_comp (kernelIsKernel S.g) hg (.zero)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
eq₁ :
  CategoryStruct.comp (Y := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯))
      (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
      (NatTrans.app (Cone.π (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯)) WalkingParallelPair.zero) =
    cg.π.app WalkingParallelPair.zero
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
have eq₂ : CategoryStruct.comp (Y :=
    Functor.obj.{0, v₁, 0, u₁}
      (Functor.obj (Functor.const WalkingParallelPair)
        (Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) sorry)))
      WalkingParallelPair.one)
    (NatTrans.app (Cocone.ι (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) sorry)) WalkingParallelPair.one)
    (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf)) =
  cf.ι.app WalkingParallelPair.one
Tactic: have eq₂ := IsColimit.comp_coconePointUniqueUpToIso_hom (cokernelIsCokernel S.f) hf (.one)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
eq₁ :
  CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
      (kernel.ι S.g) =
    Fork.ι cg
eq₂ :
  CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f)
      (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf)) =
    Cofork.π cf
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
have rw : CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
      (kernel.ι S.g) ≫
    Cofork.π cf =
  e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
Tactic: rw [← eq₁, ← eq₂, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
eq₁ :
  CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
      (kernel.ι S.g) =
    Fork.ι cg
eq₂ :
  CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f)
      (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf)) =
    Cofork.π cf
rw :
  CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
        (kernel.ι S.g) ≫
      Cofork.π cf =
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
have rw₁ : CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
      (kernel.ι S.g) ≫
    CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f)
      (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf)) =
  e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
Tactic: rw [← eq₁, ← eq₂, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
eq₁ :
  CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
      (kernel.ι S.g) =
    Fork.ι cg
eq₂ :
  CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f)
      (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf)) =
    Cofork.π cf
rw :
  CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
        (kernel.ι S.g) ≫
      Cofork.π cf =
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
rw₁ :
  CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
        (kernel.ι S.g) ≫
      CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f)
        (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf)) =
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
have rw₂ : CategoryStruct.comp (Y := kernel S.g) (Iso.inv (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg))
    (kernel.ι S.g ≫
      CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f)
        (Iso.hom (IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf))) =
  e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
Tactic: rw [← eq₁, ← eq₂, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
have this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
Tactic: have : cg.ι ≫ cf.π = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom := by
    have eq₁ := IsLimit.conePointUniqueUpToIso_inv_comp (kernelIsKernel S.g) hg (.zero)
    have eq₂ := IsColimit.comp_coconePointUniqueUpToIso_hom (cokernelIsCokernel S.f) hf (.one)
    dsimp at eq₁ eq₂
    rw [← eq₁, ← eq₂, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
have rw : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
  e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom = 0
Tactic: rw [this, IsIso.comp_left_eq_zero e₁.inv, ← Category.assoc,
    IsIso.comp_right_eq_zero _ e₂.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
rw :
  Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom = 0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
have rw₁ : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
  Eq (α := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) sorry) ⟶ cf.pt)
    (kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom) 0
Tactic: rw [this, IsIso.comp_left_eq_zero e₁.inv, ← Category.assoc,
    IsIso.comp_right_eq_zero _ e₂.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
rw :
  Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom = 0
rw₁ :
  Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
    Eq (α := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ⟶ cf.pt)
      (kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom) 0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
have rw₂ : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
  Eq (α := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) sorry) ⟶ cf.pt)
    ((kernel.ι S.g ≫ cokernel.π S.f) ≫ e₂.hom) 0
Tactic: rw [this, IsIso.comp_left_eq_zero e₁.inv, ← Category.assoc,
    IsIso.comp_right_eq_zero _ e₂.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ≅ cg.pt :=
  IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) hg
e₂ : Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯) ≅ cf.pt :=
  IsColimit.coconePointUniqueUpToIso (cokernelIsCokernel S.f) hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
rw :
  Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom = 0
rw₁ :
  Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
    Eq (α := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ⟶ cf.pt)
      (kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom) 0
rw₂ :
  Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
    Eq (α := Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) ⋯) ⟶ cf.pt)
      ((kernel.ι S.g ≫ cokernel.π S.f) ≫ e₂.hom) 0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
have rw₃ : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔
  Eq (α :=
    Cone.pt (F := parallelPair S.g 0) (Fork.ofι (P := kernel S.g) (kernel.ι S.g) sorry) ⟶
      Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) sorry))
    (kernel.ι S.g ≫ cokernel.π S.f) 0
Tactic: rw [this, IsIso.comp_left_eq_zero e₁.inv, ← Category.assoc,
    IsIso.comp_right_eq_zero _ e₂.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : S.Exact
⊢ IsLimit (KernelFork.ofι (Abelian.image.ι S.f) ⋯)
have h₁ : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Tactic: rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
W' : C
u : W' ⟶ S.X₂
hu : u ≫ S.g = 0
⊢ Eq (α := W' ⟶ cokernel S.f) (u ≫ cokernel.π S.f) 0
have rw : Eq (α := W' ⟶ cokernel S.f)
  (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g) ≫ cokernel.π S.f) 0
Tactic: rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
W' : C
u : W' ⟶ S.X₂
hu : u ≫ S.g = 0
rw :
  Eq (α := W' ⟶ cokernel S.f)
    (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g) ≫ cokernel.π S.f) 0
⊢ Eq (α := W' ⟶ cokernel S.f) (u ≫ cokernel.π S.f) 0
have rw₁ : Eq (α := W' ⟶ cokernel S.f)
  (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g ≫ cokernel.π S.f)) 0
Tactic: rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
W' : C
u : W' ⟶ S.X₂
hu : u ≫ S.g = 0
rw :
  Eq (α := W' ⟶ cokernel S.f)
    (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g) ≫ cokernel.π S.f) 0
rw₁ :
  Eq (α := W' ⟶ cokernel S.f)
    (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g ≫ cokernel.π S.f)) 0
⊢ Eq (α := W' ⟶ cokernel S.f) (u ≫ cokernel.π S.f) 0
have rw₂ : Eq (α := W' ⟶ cokernel S.f) (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) 0) 0
Tactic: rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
W' : C
u : W' ⟶ S.X₂
hu : u ≫ S.g = 0
rw :
  Eq (α := W' ⟶ cokernel S.f)
    (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g) ≫ cokernel.π S.f) 0
rw₁ :
  Eq (α := W' ⟶ cokernel S.f)
    (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) (kernel.ι S.g ≫ cokernel.π S.f)) 0
rw₂ : Eq (α := W' ⟶ cokernel S.f) (CategoryStruct.comp (Y := kernel S.g) (kernel.lift S.g u hu) 0) 0
⊢ Eq (α := W' ⟶ cokernel S.f) (u ≫ cokernel.π S.f) 0
have rw₃ : Eq.{v₁ + 1} (α := W' ⟶ cokernel S.f) 0 0
Tactic: rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
W' : C
x : W' ⟶ S.X₂
h_1 : x ≫ S.g = 0
x_1 : W' ⟶ Abelian.image S.f
hm : x_1 ≫ Abelian.image.ι S.f = x
⊢ x_1 =
    (fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
        (kernel.lift (cokernel.π S.f) u ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
      x h_1
have rw : x_1 ≫ Abelian.image.ι S.f =
  CategoryStruct.comp (Y := Abelian.image S.f)
    ((fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
        (kernel.lift (cokernel.π S.f) u sorry : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
      x h_1)
    (Abelian.image.ι S.f)
Tactic: rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
W' : C
x : W' ⟶ S.X₂
h_1 : x ≫ S.g = 0
x_1 : W' ⟶ Abelian.image S.f
hm : x_1 ≫ Abelian.image.ι S.f = x
rw :
  x_1 ≫ Abelian.image.ι S.f =
    CategoryStruct.comp (Y := Abelian.image S.f)
      ((fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
          (kernel.lift (cokernel.π S.f) u ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
        x h_1)
      (Abelian.image.ι S.f)
⊢ x_1 =
    (fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
        (kernel.lift (cokernel.π S.f) u ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
      x h_1
have rw₁ : x =
  CategoryStruct.comp (Y := Abelian.image S.f)
    ((fun {W' : C} (u : W' ⟶ S.X₂) (hu : u ≫ S.g = 0) ↦
        (kernel.lift (cokernel.π S.f) u sorry : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
      x h_1)
    (Abelian.image.ι S.f)
Tactic: rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι]