awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
simp :
  Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) →
    Mono (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
⊢ S.Exact ↔ IsIso (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
simp only [S.exact_iff_epi_imageToKernel', isIso_iff_mono_and_epi, iff_and_self]

Premises used: CategoryTheory.isIso_iff_mono_and_epi, iff_and_self, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel'
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
⊢ Mono (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
apply Limits.kernel.lift_mono

Premises used: CategoryTheory.Limits.kernel.lift_mono
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
rw :
  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 ⋯)
⊢ S.Exact ↔
    IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_imageToKernel]

Premises used: CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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 ⋯)
mpr :
  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 ⋯)
⊢ 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 ⋯)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h :
  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 ⋯)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h :
  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 ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
hS : S.Exact
⊢ IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)

Tactic:
S.exact_iff_isIso_imageToKernel.1 hS

Premises used: CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
hS : S.Exact
⊢ IsIso (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
S.exact_iff_isIso_imageToKernel'.1 hS

Premises used: CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', Iff.mp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
rw :
  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
⊢ S.Exact ↔ imageSubobject S.f = kernelSubobject S.g

Tactic:
rw [exact_iff_isIso_imageToKernel]

Premises used: CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
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 ⋯)
⊢ 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

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h :
  IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
⊢ Iso.hom (asIso (imageToKernel S.f S.g ⋯)) ≫ (kernelSubobject S.g).arrow = (imageSubobject S.f).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h :
  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

Tactic:
exact Subobject.eq_of_comm (asIso (imageToKernel _ _ S.zero)) (by simp)

Premises used: imageToKernel, CategoryTheory.ShortComplex.zero, CategoryTheory.Subobject.eq_of_comm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
h₁ :
  (imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Functor.obj Subobject.underlying (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow
⊢ imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ =
    𝟙 (Functor.obj Subobject.underlying (imageSubobject S.f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Functor.obj Subobject.underlying (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
h₁ :
  ((kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Functor.obj Subobject.underlying (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow
⊢ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯ =
    𝟙 (Functor.obj Subobject.underlying (kernelSubobject S.g))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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 ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Functor.obj Subobject.underlying (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
⊢ IsIso (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)

Tactic:
exact ⟨Subobject.ofLE _ _ h.ge, by ext; simp, by ext; simp⟩
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
rw : Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
⊢ S.Exact ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
rw [exact_iff_kernel_ι_comp_cokernel_π_zero]

Premises used: CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
⊢ 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

Tactic:
have eq₁ := IsLimit.conePointUniqueUpToIso_inv_comp (kernelIsKernel S.g) hg (.zero)
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
⊢ 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) ⋯)))
        WalkingParallelPair.one)
      (NatTrans.app (Cocone.ι (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯)) 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)
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
rw₂ 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

Tactic:
rw [← eq₁, ← eq₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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

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]
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
rw₃ 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) ⋯) ⟶
        Cocone.pt (F := parallelPair S.f 0) (Cofork.ofπ (P := cokernel S.f) (cokernel.π S.f) ⋯))
      (kernel.ι S.g ≫ cokernel.π S.f) 0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
rw [this, IsIso.comp_left_eq_zero e₁.inv, ← Category.assoc,
    IsIso.comp_right_eq_zero _ e₂.hom]

Premises used: CategoryTheory.Preadditive.IsIso.comp_left_eq_zero, CategoryTheory.Category.assoc, CategoryTheory.Preadditive.IsIso.comp_right_eq_zero, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
h : S.Exact
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h

Premises used: CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
rw₃ rw₄ : Eq.{v₁ + 1} (α := W' ⟶ cokernel S.f) 0 0
⊢ Eq (α := W' ⟶ cokernel S.f) (u ≫ cokernel.π S.f) 0

Tactic:
rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.ShortComplex.g
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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} (g' : W' ⟶ S.X₂) (eq' : g' ≫ S.g = 0),
    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)))
          g' eq')
        (Abelian.image.ι S.f) =
      g'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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)
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 ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
        x h_1)
      (Abelian.image.ι S.f)
rw₂ rw₃ : x = 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

Tactic:
rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι]

Premises used: CategoryTheory.Abelian.image.ι, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
⊢ IsLimit (KernelFork.ofι (Abelian.image.ι S.f) ⋯)

Tactic:
exact KernelFork.IsLimit.ofι _ _
    (fun u hu ↦ kernel.lift (cokernel.π S.f) u
      (by rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero])) (by simp)
    (fun _ _ _ hm => by rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι])

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.ofι, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.cokernel.π, CategoryTheory.Limits.kernel.lift
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
Z' : C
u : S.X₂ ⟶ Z'
hu : S.f ≫ u = 0
rw :
  Eq (α := kernel S.g ⟶ Z')
    (kernel.ι S.g ≫ CategoryStruct.comp (Y := cokernel S.f) (cokernel.π S.f) (cokernel.desc S.f u hu)) 0
rw₁ :
  Eq (α := kernel S.g ⟶ Z')
    (CategoryStruct.comp (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) (cokernel.desc S.f u hu)) 0
rw₂ : Eq (α := kernel S.g ⟶ Z') (CategoryStruct.comp (Y := cokernel S.f) 0 (cokernel.desc S.f u hu)) 0
rw₃ rw₄ : Eq.{v₁ + 1} (α := kernel S.g ⟶ Z') 0 0
⊢ Eq (α := kernel S.g ⟶ Z') (kernel.ι S.g ≫ u) 0

Tactic:
rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
⊢ ∀ {Z' : C} (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0),
    CategoryStruct.comp (Y := Abelian.coimage S.g) (Abelian.coimage.π S.g)
        ((fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq') =
      g'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
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
refine :
  ∀ {Z' : C} (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0) (m : Abelian.coimage S.g ⟶ Z'),
    Abelian.coimage.π S.g ≫ m = g' →
      m =
        (fun {Z' : C} (u : S.X₂ ⟶ Z') (hu : S.f ≫ u = 0) ↦
            (cokernel.desc (kernel.ι S.g) u ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
          g' eq'
⊢ IsColimit (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)

Tactic:
refine CokernelCofork.IsColimit.ofπ _ _
    (fun u hu => cokernel.desc (kernel.ι S.g) u
      (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
    (by simp) ?_

Premises used: CategoryTheory.Limits.cokernel.desc, CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ, CategoryTheory.ShortComplex.g, CategoryTheory.Limits.kernel.ι