awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
rw rw₁ : f' = f'
⊢ f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)

Tactic:
rw [kernel.lift_ι]

Premises used: CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)

Tactic:
have hf' : f' = kernel.lift γ f' (by simp [γ, f']) ≫ kernel.ι γ := by rw [kernel.lift_ι]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
rw :
  Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ))
    (CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ) ≫ cokernel.π (kernel.ι γ)) 0
⊢ Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0

Tactic:
rw [hf']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
⊢ Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ))
    (CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ) ≫ cokernel.π (kernel.ι γ)) 0

Tactic:
simp only [assoc, cokernel.condition, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.cokernel.condition
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
⊢ Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0

Tactic:
have wπ : f' ≫ cokernel.π (kernel.ι γ) = 0 := by
    rw [hf']
    simp only [assoc, cokernel.condition, comp_zero]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
⊢ e.hom ≫ kernel.ι γ = S.abelianImageToKernel

Tactic:
have he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel :=
    IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
rw :
  CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ) =
    Abelian.factorThruImage S.f ≫ S.abelianImageToKernel
⊢ f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ

Tactic:
rw [hf', he]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
⊢ CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ) =
    Abelian.factorThruImage S.f ≫ S.abelianImageToKernel

Tactic:
simp only [γ, f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g),
      assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.ShortComplex.g, CategoryTheory.Limits.kernel.ι, CategoryTheory.ShortComplex.abelianImageToKernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
⊢ f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ

Tactic:
have fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ := by
    rw [hf', he]
    simp only [γ, f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g),
      assoc]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
Z' : C
x : kernel S.g ⟶ Z'
hx : f' ≫ x = 0
⊢ Eq (α := kernel γ ⟶ Z') (kernel.ι γ ≫ x) 0

Tactic:
simpa only [← cancel_epi e.hom, ← cancel_epi (Abelian.factorThruImage S.f),
        comp_zero, fac, assoc] using hx

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.factorThruImage, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.f, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
Z' : C
x : kernel S.g ⟶ Z'
hx : f' ≫ x = 0
b : cokernel (X := kernel γ) (kernel.ι γ) ⟶ Z'
hb : cokernel.π (kernel.ι γ) ≫ b = x
⊢ coequalizer.π (kernel.ι γ) 0 ≫ b =
    CategoryStruct.comp (Y := coequalizer (X := kernel γ) (kernel.ι γ) 0) (coequalizer.π (kernel.ι γ) 0)
      ((fun {Z' : C} (x : kernel S.g ⟶ Z') (hx : f' ≫ x = 0) ↦
          (cokernel.desc (kernel.ι γ) x ⋯ : cokernel (X := kernel γ) (kernel.ι γ) ⟶ Z'))
        x hx)

Tactic:
simp only [hb, cokernel.π_desc]

Premises used: CategoryTheory.Limits.cokernel.π_desc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
have : (hπ : IsColimit (CokernelCofork.ofπ (cokernel.π (kernel.ι γ)) wπ)) → S.LeftHomologyData
⊢ S.LeftHomologyData

Tactic:
have hπ : IsColimit (CokernelCofork.ofπ _ wπ) :=
    CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => cokernel.desc _ x (by
      simpa only [← cancel_epi e.hom, ← cancel_epi (Abelian.factorThruImage S.f),
        comp_zero, fac, assoc] using hx))
    (fun x hx => cokernel.π_desc _ _ _)
    (fun x hx b hb => coequalizer.hom_ext (by simp only [hb, cokernel.π_desc]))
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
hπ : IsColimit (CokernelCofork.ofπ (cokernel.π (kernel.ι γ)) wπ)
⊢ S.LeftHomologyData

Tactic:
exact
    { K := kernel S.g,
      H := Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f)
      i := kernel.ι _,
      π := cokernel.π _
      wi := kernel.condition _
      hi := kernelIsKernel _
      wπ := wπ
      hπ := hπ }
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
⊢ Eq (α := S.X₁ ⟶ Abelian.coimage S.g) (S.f ≫ Abelian.coimage.π S.g) 0

Tactic:
simp only [← cancel_mono (Abelian.factorThruCoimage S.g), assoc,
      cokernel.π_desc, zero, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.ShortComplex.zero, CategoryTheory.Abelian.factorThruCoimage, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
⊢ cokernel.π S.f ≫ S.cokernelToAbelianCoimage = Abelian.coimage.π S.g

Tactic:
cokernel.π_desc _ _ _

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.ShortComplex.cokernelToAbelianCoimage
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
⊢ Epi S.cokernelToAbelianCoimage

Tactic:
epi_of_epi_fac S.cokernel_π_comp_cokernelToAbelianCoimage

Premises used: CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
⊢ Eq (α := kernel S.g ⟶ Abelian.coimage S.g) ((kernel.ι S.g ≫ cokernel.π S.f) ≫ S.cokernelToAbelianCoimage) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
Z' : C
k : cokernel S.f ⟶ Z'
hk : Eq (α := kernel S.g ⟶ Z') ((kernel.ι S.g ≫ cokernel.π S.f) ≫ k) 0
⊢ Eq (α := kernel S.g ⟶ Z') (kernel.ι S.g ≫ cokernel.π S.f ≫ k) 0

Tactic:
simpa only [assoc] using hk

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
Z' : C
k : cokernel S.f ⟶ Z'
hk : Eq (α := kernel S.g ⟶ Z') ((kernel.ι S.g ≫ cokernel.π S.f) ≫ k) 0
⊢ S.cokernelToAbelianCoimage ≫
      (fun {Z' : C} (k : cokernel S.f ⟶ Z') (hk : Eq (α := kernel S.g ⟶ Z') ((kernel.ι S.g ≫ cokernel.π S.f) ≫ k) 0) ↦
          (cokernel.desc (kernel.ι S.g) (cokernel.π S.f ≫ k) ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
        k hk =
    k

Tactic:
simp only [← cancel_epi (cokernel.π S.f),
        cokernel_π_comp_cokernelToAbelianCoimage_assoc, cokernel.π_desc]

Premises used: CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.cokernel.π, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
Z' : C
k : cokernel S.f ⟶ Z'
hk : Eq (α := kernel S.g ⟶ Z') ((kernel.ι S.g ≫ cokernel.π S.f) ≫ k) 0
b : Abelian.coimage S.g ⟶ Z'
hb : S.cokernelToAbelianCoimage ≫ b = k
⊢ b =
    (fun {Z' : C} (k : cokernel S.f ⟶ Z') (hk : Eq (α := kernel S.g ⟶ Z') ((kernel.ι S.g ≫ cokernel.π S.f) ≫ k) 0) ↦
        (cokernel.desc (kernel.ι S.g) (cokernel.π S.f ≫ k) ⋯ : cokernel (X := kernel S.g) (kernel.ι S.g) ⟶ Z'))
      k hk

Tactic:
simp only [← cancel_epi S.cokernelToAbelianCoimage, ← cancel_epi (cokernel.π S.f), hb,
        cokernel_π_comp_cokernelToAbelianCoimage_assoc, cokernel.π_desc]

Premises used: CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.ShortComplex.cokernelToAbelianCoimage, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.cokernel.π, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
⊢ γ ≫ g' = 0

Tactic:
simp [γ, g']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
rw rw₁ : g' = g'
⊢ g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)

Tactic:
rw [cokernel.π_desc]

Premises used: CategoryTheory.Limits.cokernel.π_desc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
⊢ g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)

Tactic:
have hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' (by simp [γ, g']) := by rw [cokernel.π_desc]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
rw :
  Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
    (kernel.ι (cokernel.π γ) ≫ CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)) 0
rw₁ :
  Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
    (CategoryStruct.comp (Y := cokernel γ) 0 (cokernel.desc γ g' ⋯)) 0
rw₂ rw₃ : Eq.{v + 1} (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) 0 0
⊢ Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0

Tactic:
rw [hg', kernel.condition_assoc, zero_comp]

Premises used: CategoryTheory.Limits.kernel.condition_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
⊢ Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0

Tactic:
have wι : kernel.ι (cokernel.π γ) ≫ g' = 0 := by rw [hg', kernel.condition_assoc, zero_comp]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
⊢ cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage

Tactic:
have he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage :=
    IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
rw :
  CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯) =
    S.cokernelToAbelianCoimage ≫ Abelian.factorThruCoimage S.g
⊢ g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g

Tactic:
rw [hg', reassoc_of% he]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
⊢ CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯) =
    S.cokernelToAbelianCoimage ≫ Abelian.factorThruCoimage S.g

Tactic:
simp only [γ, g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f),
      cokernel_π_comp_cokernelToAbelianCoimage_assoc]

Premises used: CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.cokernel.π, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
⊢ g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g

Tactic:
have fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g := by
    rw [hg', reassoc_of% he]
    simp only [γ, g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f),
      cokernel_π_comp_cokernelToAbelianCoimage_assoc]