awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0
have rw : Eq (α := A ⟶ S.homology) (0 ≫ Iso.hom S.leftHomologyIso) 0
Tactic: rw [S.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc k x hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : Eq (α := A ⟶ S.homology) (0 ≫ Iso.hom S.leftHomologyIso) 0
⊢ Eq (α := A ⟶ S.homology) (S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ Iso.hom S.leftHomologyIso) 0
have rw₁ : Eq.{v + 1} (α := A ⟶ S.homology) 0 0
Tactic: rw [S.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc k x hx, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0
have rw : S.f ≫ S.g ≫ x = 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
⊢ S.f ≫ k = 0
have rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
⊢ S.f ≫ k = 0
have rw₂ : Eq.{v + 1} (α := S.X₁ ⟶ A) 0 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ Eq (α := S.homology ⟶ A) (S.homologyι ≫ S.descOpcycles k ⋯) 0
have dsimp : Eq (α := S.homology ⟶ A) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.descOpcycles k sorry) 0
Tactic: dsimp only [homologyι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ Eq (α := S.homology ⟶ A) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯) 0
have rw : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι ≫ S.descOpcycles k sorry) 0
Tactic: rw [assoc, S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι ≫ S.descOpcycles k ⋯) 0
⊢ Eq (α := S.homology ⟶ A) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯) 0
have rw₁ : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ 0) 0
Tactic: rw [assoc, S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S : ShortComplex.{v, u} C
A : C
inst_2 : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ S.rightHomologyι ≫ S.descOpcycles k ⋯) 0
rw₁ : Eq (α := S.homology ⟶ A) (Iso.inv S.rightHomologyIso ≫ 0) 0
⊢ Eq (α := S.homology ⟶ A) ((Iso.inv S.rightHomologyIso ≫ S.rightHomologyι) ≫ S.descOpcycles k ⋯) 0
have rw₂ : Eq.{v + 1} (α := S.homology ⟶ A) 0 0
Tactic: rw [assoc, S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have h : Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
Tactic: have h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0 := by
    simp only [← cancel_epi φ.τ₁, ← toCycles_naturality_assoc,
      IsIso.hom_inv_id_assoc, toCycles_comp_homologyπ, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have have : ∀
  (z :
    Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
        (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ sorry : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
      S₁.homology)
  (hz :
    Eq (α := S₂.cycles ⟶ S₁.homology)
      (Cofork.π (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ sorry) ≫ z : S₂.cycles ⟶ S₁.homology)
      (inv (cyclesMap φ) ≫ S₁.homologyπ : S₂.cycles ⟶ S₁.homology)),
  IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
Tactic: have ⟨z, hz⟩ := CokernelCofork.IsColimit.desc' S₂.homologyIsCokernel _ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have refine_1 : homologyMap φ ≫ z = 𝟙 S₁.homology
Tactic: refine ⟨⟨z, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : homologyMap φ ≫ z = 𝟙 S₁.homology
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have refine_2 : z ≫ homologyMap φ = 𝟙 S₂.homology
Tactic: refine ⟨⟨z, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1 : CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ ≫ z) = S₁.homologyπ ≫ 𝟙 S₁.homology
Tactic: rw [← cancel_epi S₁.homologyπ, homologyπ_naturality_assoc, hz,
      IsIso.hom_inv_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ ≫ z) = S₁.homologyπ ≫ 𝟙 S₁.homology
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₁ : cyclesMap φ ≫ S₂.homologyπ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology
Tactic: rw [← cancel_epi S₁.homologyπ, homologyπ_naturality_assoc, hz,
      IsIso.hom_inv_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ ≫ z) = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₁ : cyclesMap φ ≫ S₂.homologyπ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₂ : CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) (inv (cyclesMap φ) ≫ S₁.homologyπ) = S₁.homologyπ ≫ 𝟙 S₁.homology
Tactic: rw [← cancel_epi S₁.homologyπ, homologyπ_naturality_assoc, hz,
      IsIso.hom_inv_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ ≫ z) = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₁ : cyclesMap φ ≫ S₂.homologyπ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₂ :
  CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) (inv (cyclesMap φ) ≫ S₁.homologyπ) = S₁.homologyπ ≫ 𝟙 S₁.homology
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₃ : S₁.homologyπ = S₁.homologyπ ≫ 𝟙 S₁.homology
Tactic: rw [← cancel_epi S₁.homologyπ, homologyπ_naturality_assoc, hz,
      IsIso.hom_inv_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_1 : CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ ≫ z) = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₁ : cyclesMap φ ≫ S₂.homologyπ ≫ z = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₂ :
  CategoryStruct.comp (Y := S₂.cycles) (cyclesMap φ) (inv (cyclesMap φ) ≫ S₁.homologyπ) = S₁.homologyπ ≫ 𝟙 S₁.homology
refine_1₃ : S₁.homologyπ = S₁.homologyπ ≫ 𝟙 S₁.homology
⊢ homologyMap φ ≫ z = 𝟙 S₁.homology
have refine_1₄ : Eq (α := S₁.cycles ⟶ S₁.homology) S₁.homologyπ S₁.homologyπ
Tactic: rw [← cancel_epi S₁.homologyπ, homologyπ_naturality_assoc, hz,
      IsIso.hom_inv_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2 : S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
Tactic: rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_2 : S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₁ : CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ) : S₂.cycles ⟶ S₁.cycles)
    (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology) =
  S₂.homologyπ ≫ 𝟙 S₂.homology
Tactic: rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_2 : S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₁ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ) : S₂.cycles ⟶ S₁.cycles)
      (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology) =
    S₂.homologyπ ≫ 𝟙 S₂.homology
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₂ : CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ)) (cyclesMap φ ≫ S₂.homologyπ) = S₂.homologyπ ≫ 𝟙 S₂.homology
Tactic: rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_2 : S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₁ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ) : S₂.cycles ⟶ S₁.cycles)
      (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology) =
    S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₂ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ)) (cyclesMap φ ≫ S₂.homologyπ) = S₂.homologyπ ≫ 𝟙 S₂.homology
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₃ : S₂.homologyπ = S₂.homologyπ ≫ 𝟙 S₂.homology
Tactic: rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.cycles) (Y := S₂.cycles) (cyclesMap φ)
h₂ : Epi φ.τ₁
h :
  Eq (α := S₂.X₁ ⟶ S₁.homology) (CategoryStruct.comp (Y := S₂.cycles) S₂.toCycles (inv (cyclesMap φ) ≫ S₁.homologyπ)) 0
z :
  Cocone.pt (F := parallelPair (Y := S₂.cycles) S₂.toCycles 0)
      (CokernelCofork.ofπ (Z := S₂.homology) S₂.homologyπ ⋯ : CokernelCofork (Y := S₂.cycles) S₂.toCycles) ⟶
    S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
refine_2 : S₂.homologyπ ≫ z ≫ homologyMap φ = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₁ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ) : S₂.cycles ⟶ S₁.cycles)
      (CategoryStruct.comp (Y := S₁.homology) S₁.homologyπ (homologyMap φ) : S₁.cycles ⟶ S₂.homology) =
    S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₂ :
  CategoryStruct.comp (Y := S₁.cycles) (inv (cyclesMap φ)) (cyclesMap φ ≫ S₂.homologyπ) = S₂.homologyπ ≫ 𝟙 S₂.homology
refine_2₃ : S₂.homologyπ = S₂.homologyπ ≫ 𝟙 S₂.homology
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology
have refine_2₄ : Eq (α := S₂.cycles ⟶ S₂.homology) S₂.homologyπ S₂.homologyπ
Tactic: rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have h : Eq (α := S₂.homology ⟶ S₁.X₃)
  (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
Tactic: have h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0 := by
    simp only [← cancel_mono φ.τ₃, zero_comp, assoc, ← fromOpcycles_naturality,
      IsIso.inv_hom_id_assoc, homologyι_comp_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have have : ∀
  (z :
    S₂.homology ⟶
      Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
        (KernelFork.ofι (Z := S₁.homology) S₁.homologyι sorry : KernelFork (X := S₁.opcycles) S₁.fromOpcycles))
  (hz :
    Eq (α := S₂.homology ⟶ S₁.opcycles)
      (z ≫ Fork.ι (KernelFork.ofι (Z := S₁.homology) S₁.homologyι sorry) : S₂.homology ⟶ S₁.opcycles)
      (S₂.homologyι ≫ inv (opcyclesMap φ) : S₂.homology ⟶ S₁.opcycles)),
  IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
Tactic: have ⟨z, hz⟩ := KernelFork.IsLimit.lift' S₁.homologyIsKernel _ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have refine_1 : homologyMap φ ≫ z = 𝟙 S₁.homology
Tactic: refine ⟨⟨z, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Homology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
S₁ S₂ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
h₁ : IsIso (X := S₁.opcycles) (Y := S₂.opcycles) (opcyclesMap φ)
h₂ : Mono φ.τ₃
h :
  Eq (α := S₂.homology ⟶ S₁.X₃)
    (CategoryStruct.comp (Y := S₁.opcycles) (S₂.homologyι ≫ inv (opcyclesMap φ)) S₁.fromOpcycles) 0
z :
  S₂.homology ⟶
    Cone.pt (F := parallelPair (X := S₁.opcycles) S₁.fromOpcycles 0)
      (KernelFork.ofι (Z := S₁.homology) S₁.homologyι ⋯ : KernelFork (X := S₁.opcycles) S₁.fromOpcycles)
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
refine_1 : homologyMap φ ≫ z = 𝟙 S₁.homology
⊢ IsIso (X := S₁.homology) (Y := S₂.homology) (homologyMap φ)
have refine_2 : z ≫ homologyMap φ = 𝟙 S₂.homology
Tactic: refine ⟨⟨z, ?_, ?_⟩⟩