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
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
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
W' : C
x : W' ⟶ cokernel S.f
hx : x ≫ g' = 0
⊢ Eq (α := W' ⟶ cokernel γ) (x ≫ cokernel.π γ) 0

Tactic:
simpa only [← cancel_mono e.hom, ← cancel_mono (Abelian.factorThruCoimage S.g), assoc,
          zero_comp, fac] using hx

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Abelian.factorThruCoimage, CategoryTheory.Limits.zero_comp, CategoryTheory.Iso.hom, 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
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
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
W' : C
x : W' ⟶ cokernel S.f
hx : x ≫ g' = 0
b : W' ⟶ kernel (Y := cokernel γ) (cokernel.π γ)
hb : b ≫ kernel.ι (cokernel.π γ) = x
⊢ b ≫ equalizer.ι (cokernel.π γ) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel γ) (cokernel.π γ) 0)
      ((fun {W' : C} (x : W' ⟶ cokernel S.f) (hx : x ≫ g' = 0) ↦
          (kernel.lift (cokernel.π γ) x ⋯ : W' ⟶ kernel (Y := cokernel γ) (cokernel.π γ)))
        x hx)
      (equalizer.ι (cokernel.π γ) 0)

Tactic:
simp only [hb, 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
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
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
have : (hι : IsLimit (KernelFork.ofι (kernel.ι (cokernel.π γ)) wι)) → S.RightHomologyData
⊢ S.RightHomologyData

Tactic:
have hι : IsLimit (KernelFork.ofι _ wι) :=
    KernelFork.IsLimit.ofι _ _
      (fun x hx => kernel.lift _ x (by
        simpa only [← cancel_mono e.hom, ← cancel_mono (Abelian.factorThruCoimage S.g), assoc,
          zero_comp, fac] using hx))
      (fun x hx => kernel.lift_ι _ _ _)
      (fun x hx b hb => equalizer.hom_ext (by simp only [hb, 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
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
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
hι : IsLimit (KernelFork.ofι (kernel.ι (cokernel.π γ)) wι)
⊢ S.RightHomologyData

Tactic:
exact
    { Q := cokernel S.f,
      H := Abelian.image (kernel.ι S.g ≫ cokernel.π S.f)
      p := cokernel.π _
      ι := kernel.ι _
      wp := cokernel.condition _
      hp := cokernelIsCokernel _
      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
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
refine_1 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₁) (Functor.mapCone π₁ (KernelFork.ofι i ⋯))
refine_2 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₂) (Functor.mapCone π₂ (KernelFork.ofι i ⋯))
refine_3 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₃) (Functor.mapCone π₃ (KernelFork.ofι i ⋯))
⊢ NormalMono i

Tactic:
refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
    (isLimitOfIsLimitπ _ ?_ ?_ ?_)

Premises used: CategoryTheory.Limits.cokernel.condition, CategoryTheory.NormalMono.mk, CategoryTheory.ShortComplex.isLimitOfIsLimitπ, CategoryTheory.Limits.cokernel.π
-- 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
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
⊢ IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₁) (Functor.mapCone π₁ (KernelFork.ofι i ⋯))

Tactic:
apply Abelian.isLimitMapConeOfKernelForkOfι

Premises used: CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfι
-- 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
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
⊢ IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₂) (Functor.mapCone π₂ (KernelFork.ofι i ⋯))

Tactic:
apply Abelian.isLimitMapConeOfKernelForkOfι

Premises used: CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfι
-- 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
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
⊢ IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₃) (Functor.mapCone π₃ (KernelFork.ofι i ⋯))

Tactic:
apply Abelian.isLimitMapConeOfKernelForkOfι

Premises used: CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfι
-- 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
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
refine_1 :
  IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₁) (Functor.mapCocone π₁ (CokernelCofork.ofπ p ⋯))
refine_2 :
  IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₂) (Functor.mapCocone π₂ (CokernelCofork.ofπ p ⋯))
refine_3 :
  IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₃) (Functor.mapCocone π₃ (CokernelCofork.ofπ p ⋯))
⊢ NormalEpi p

Tactic:
refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfIsColimitπ _ ?_ ?_ ?_)

Premises used: CategoryTheory.ShortComplex.isColimitOfIsColimitπ, CategoryTheory.Limits.kernel.condition, CategoryTheory.NormalEpi.mk, CategoryTheory.Limits.kernel.ι
-- 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
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
⊢ IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₁) (Functor.mapCocone π₁ (CokernelCofork.ofπ p ⋯))

Tactic:
apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ

Premises used: CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ
-- 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
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
⊢ IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₂) (Functor.mapCocone π₂ (CokernelCofork.ofπ p ⋯))

Tactic:
apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ

Premises used: CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ
-- 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
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
⊢ IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₃) (Functor.mapCocone π₃ (CokernelCofork.ofπ p ⋯))

Tactic:
apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ

Premises used: CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ
-- 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
⊢ S.homologyIsoImageICyclesCompPOpcycles.hom ≫ image.ι (S.iCycles ≫ S.pOpcycles) = S.homologyι

Tactic:
image.isoStrongEpiMono_hom_comp_ι _ _ _

Premises used: CategoryTheory.Limits.image.isoStrongEpiMono_hom_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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
⊢ Eq (α := S.cycles ⟶ S.opcycles)
    ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)) (S.iCycles ≫ S.pOpcycles)

Tactic:
simp [← reassoc_of% 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
⊢ Eq (α := S.cycles ⟶ S.opcycles)
    ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)) (S.iCycles ≫ S.pOpcycles)

Tactic:
have : ((S.isoCyclesOfIsLimit hkf).inv ≫ π) ≫ ι ≫
    (S.isoOpcyclesOfIsColimit hcc).hom = S.iCycles ≫ S.pOpcycles := by
    simp [← reassoc_of% 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
this :
  Eq (α := S.cycles ⟶ S.opcycles)
    ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)) (S.iCycles ≫ S.pOpcycles)
⊢ H ≅ image (X := S.cycles) (Y := S.opcycles) (S.iCycles ≫ S.pOpcycles)

Tactic:
exact image.isoStrongEpiMono _ _ this

Premises used: CategoryTheory.Limits.image.isoStrongEpiMono
-- 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
comm :
  Eq (α := S.cycles ⟶ S.opcycles)
    ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)) (S.iCycles ≫ S.pOpcycles)
⊢ (isoImage S hkf hcc fac).hom ≫ image.ι (S.iCycles ≫ S.pOpcycles) = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)

Tactic:
apply image.isoStrongEpiMono_hom_comp_ι

Premises used: CategoryTheory.Limits.image.isoStrongEpiMono_hom_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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
⊢ Eq (α := S.cycles ⟶ S.opcycles)
    ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)) (S.iCycles ≫ S.pOpcycles)

Tactic:
simp [← reassoc_of% 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
dsimp :
  π ≫ (isoImage S hkf hcc fac).hom ≫ S.homologyIsoImageICyclesCompPOpcycles.inv =
    Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ
⊢ π ≫ (isoHomology S hkf hcc fac).hom = Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ

Tactic:
dsimp [isoHomology]

Premises used: CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology
-- 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
⊢ π ≫ (isoImage S hkf hcc fac).hom ≫ S.homologyIsoImageICyclesCompPOpcycles.inv =
    Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ

Tactic:
simp [← cancel_mono (S.homologyIsoImageICyclesCompPOpcycles.hom),
    ← cancel_mono (image.ι (S.iCycles ≫ S.pOpcycles)),
    ← reassoc_of% fac]

Premises used: CategoryTheory.Limits.image.ι, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.cancel_mono, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.iCycles, CategoryTheory.Iso.hom, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles
-- 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
⊢ (isoHomology S hkf hcc fac).inv ≫ ι = S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc)

Tactic:
simp [← cancel_epi S.homologyπ, ← cancel_epi (S.isoCyclesOfIsLimit hkf).hom,
    ← π_comp_isoHomology_hom_assoc S hkf hcc fac, ← fac]

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.isoCyclesOfIsLimit, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_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
kf : KernelFork S.g
hkf : IsLimit kf
⊢ Mono (Fork.ι kf)

Tactic:
have := Fork.IsLimit.mono hkf
-- 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
kf : KernelFork S.g
hkf : IsLimit kf
this : Mono (Fork.ι kf)
⊢ hkf.lift (KernelFork.ofι S.f ⋯) = CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf))

Tactic:
simp [← cancel_mono kf.ι]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.Fork.ι
-- 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
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ Epi (Cofork.π cc)

Tactic:
have := Cofork.IsColimit.epi hcc
-- 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
cc : CokernelCofork S.f
hcc : IsColimit cc
this : Epi (Cofork.π cc)
⊢ hcc.desc (CokernelCofork.ofπ S.g ⋯) =
    CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles

Tactic:
simp [← cancel_epi cc.π]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Limits.Cofork.π
-- 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
⊢ S.homologyπ ≫ (isoHomology S hkf hcc fac).inv = Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π

Tactic:
simp only [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, Iso.inv_hom_id, comp_id,
    π_comp_isoHomology_hom, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, 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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_2 : Epi π
inst_3 : Mono ι
rw :
  ((isoHomology S hkf hcc fac).hom ≫ S.homologyι) ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
rw₁ :
  (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
rw₂ :
  (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    ι ≫
      CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc))
        (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
rw₃ : (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) = ι ≫ 𝟙 cc.pt
rw₄ : (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) = ι
rw₅ : (isoHomology S hkf hcc fac).hom ≫ (isoHomology S hkf hcc fac).inv ≫ ι = ι
rw₆ rw₇ : ι = ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)

Tactic:
rw [← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, ← isoHomology_hom_comp_ι S hkf hcc fac, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Iso.inv, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
⊢ Iso.hom (Iso.refl kf.pt) ≫ Fork.ι (KernelFork.ofι (Fork.ι kf) ⋯) = Fork.ι kf

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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst_4 : Epi π
inst_5 : Mono ι
dsimp :
  Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ H)
    ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ π) 0

Tactic:
dsimp