awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw₄ : (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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) = ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw₅ : (isoHomology S hkf hcc fac).hom ≫ (isoHomology S hkf hcc fac).inv ≫ ι = ι
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ≫ ι = ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw₆ : ι = ι
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 (α := (KernelFork.ofι S.f ⋯).pt ⟶ H)
    ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ π) 0
have dsimp : Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f sorry) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f sorry).pt ⟶ H)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw : Eq (α := S.X₁ ⟶ S.homology)
  (((hkf.lift (KernelFork.ofι S.f sorry) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
  (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₁ : Eq (α := S.X₁ ⟶ S.homology)
  ((hkf.lift (KernelFork.ofι S.f sorry) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
  (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₂ : Eq (α := S.X₁ ⟶ S.homology)
  (hkf.lift (KernelFork.ofι S.f sorry) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
  (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₃ : Eq (α := S.X₁ ⟶ S.homology) (hkf.lift (KernelFork.ofι S.f sorry) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
  (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₄ : Eq (α := S.X₁ ⟶ S.homology)
  (hkf.lift (KernelFork.ofι S.f sorry) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
  (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₄ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₅ : Eq (α := S.X₁ ⟶ S.homology)
  (hkf.lift (KernelFork.ofι S.f sorry) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
  (0 : S.X₁ ⟶ S.homology)
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₄ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₅ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 : S.X₁ ⟶ S.homology)
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₆ : Eq (α := S.X₁ ⟶ S.homology)
  (CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf)) ≫
    Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ)
  0
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₄ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₅ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 : S.X₁ ⟶ S.homology)
rw₆ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf)) ≫
      Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ)
    0
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₇ : Eq (α := S.X₁ ⟶ S.homology)
  (CategoryStruct.comp (Y := S.cycles) S.toCycles
    (Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ))
  0
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₄ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₅ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 : S.X₁ ⟶ S.homology)
rw₆ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf)) ≫
      Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ)
    0
rw₇ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles
      (Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ))
    0
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₈ : Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.homologyπ) 0
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
rw :
  Eq (α := S.X₁ ⟶ S.homology)
    (((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₁ :
  Eq (α := S.X₁ ⟶ S.homology)
    ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₂ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₃ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ π ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₄ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 ≫ (isoHomology S hkf hcc fac).hom : S.X₁ ⟶ S.homology)
rw₅ :
  Eq (α := S.X₁ ⟶ S.homology)
    (hkf.lift (KernelFork.ofι S.f ⋯) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ : S.X₁ ⟶ S.homology)
    (0 : S.X₁ ⟶ S.homology)
rw₆ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf)) ≫
      Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ)
    0
rw₇ :
  Eq (α := S.X₁ ⟶ S.homology)
    (CategoryStruct.comp (Y := S.cycles) S.toCycles
      (Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ))
    0
rw₈ : Eq (α := S.X₁ ⟶ S.homology) (S.toCycles ≫ S.homologyπ) 0
⊢ Eq (α := S.X₁ ⟶ H) ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π : S.X₁ ⟶ H) (0 : (KernelFork.ofι S.f ⋯).pt ⟶ H)
have rw₉ : Eq.{v + 1} (α := S.X₁ ⟶ S.homology) 0 0
Tactic: rw [← cancel_mono (isoHomology S hkf hcc fac).hom, assoc, assoc, id_comp,
      π_comp_isoHomology_hom, zero_comp, f'_eq,
      assoc, Iso.inv_hom_id_assoc, toCycles_comp_homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
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 ι
⊢ IsColimit (CokernelCofork.ofπ π ⋯)
have refine_1 : parallelPair (X := (KernelFork.ofι S.f sorry).pt)
    ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) sorry)).lift (KernelFork.ofι S.f sorry)) 0 ≅
  parallelPair (Y := S.cycles) S.toCycles 0
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsCokernel