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 S₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι
rw₁ : h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.ι = 0 ≫ h₂.ι
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
have rw₂ : h₁.f' ≫ h₁.i ≫ h₂.p = 0 ≫ h₂.ι
Tactic: rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι
rw₁ : h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.ι = 0 ≫ h₂.ι
rw₂ : h₁.f' ≫ h₁.i ≫ h₂.p = 0 ≫ h₂.ι
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
have rw₃ : S.f ≫ h₂.p = 0 ≫ h₂.ι
Tactic: rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι
rw₁ : h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.ι = 0 ≫ h₂.ι
rw₂ : h₁.f' ≫ h₁.i ≫ h₂.p = 0 ≫ h₂.ι
rw₃ : S.f ≫ h₂.p = 0 ≫ h₂.ι
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
have rw₄ : Eq (α := S.X₁ ⟶ h₂.Q) 0 (0 ≫ h₂.ι)
Tactic: rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
rw : (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι
rw₁ : h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.ι = 0 ≫ h₂.ι
rw₂ : h₁.f' ≫ h₁.i ≫ h₂.p = 0 ≫ h₂.ι
rw₃ : S.f ≫ h₂.p = 0 ≫ h₂.ι
rw₄ : Eq (α := S.X₁ ⟶ h₂.Q) 0 (0 ≫ h₂.ι)
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0
have rw₅ : Eq.{v + 1} (α := S.X₁ ⟶ h₂.Q) 0 0
Tactic: rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, 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
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
have rw : leftRightHomologyComparison' h₁ h₂ =
  leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
Tactic: rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, 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 : ShortComplex.{v, u} C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
rw :
  leftRightHomologyComparison' h₁ h₂ =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
have rw₁ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S ≫ 𝟙 S) h₂ h₂
Tactic: rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, 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 : ShortComplex.{v, u} C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
rw :
  leftRightHomologyComparison' h₁ h₂ =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
rw₁ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S ≫ 𝟙 S) h₂ h₂
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
have rw₂ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂
Tactic: rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, 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 : ShortComplex.{v, u} C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
rw :
  leftRightHomologyComparison' h₁ h₂ =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
rw₁ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S ≫ 𝟙 S) h₂ h₂
rw₂ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
have rw₃ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ 𝟙 h₂.H
Tactic: rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, 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 : ShortComplex.{v, u} C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
rw :
  leftRightHomologyComparison' h₁ h₂ =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
rw₁ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S ≫ 𝟙 S) h₂ h₂
rw₂ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂
rw₃ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ 𝟙 h₂.H
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
have rw₄ : leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂
Tactic: rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, 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₁ S₂ S₃ S₄ : ShortComplex.{v, u} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : S.HomologyData
⊢ IsIso (Y := h.right.H) (leftRightHomologyComparison' h.left h.right)
have rw : IsIso h.iso.hom
Tactic: rw [h.leftRightHomologyComparison'_eq]
-- 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₁_1 : S₁.HomologyData
h₂_1 : S₂.HomologyData
inst_2 : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ IsIso (leftRightHomologyComparison' h₁ h₂)
have rw : IsIso
  (leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
    CategoryStruct.comp (Y := S.homologyData.right.H)
      (leftRightHomologyComparison' S.homologyData.left S.homologyData.right)
      (rightHomologyMap' (𝟙 S) S.homologyData.right h₂))
Tactic: rw [leftRightHomologyComparison'_compatibility h₁ S.homologyData.left h₂
    S.homologyData.right]
-- 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
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst_2 : S.HasHomology
⊢ leftRightHomologyComparison' h₁ h₂ =
    CategoryStruct.comp (Y := S.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₂.homologyIso)
have rw : leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
    S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
  CategoryStruct.comp (Y := S.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₂.homologyIso)
Tactic: rw [leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
    S.homologyData h₁ 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 : ShortComplex.{v, u} C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst_2 : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    CategoryStruct.comp (Y := S.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₂.homologyIso)
have dsimp : leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
    S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
  CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData)
      (leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫
    CategoryStruct.comp (Y := S.rightHomology)
      (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData)
      (rightHomologyMap' (𝟙 S) S.rightHomologyData h₂)
Tactic: dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyMapIso', leftHomologyIso,
    RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', rightHomologyIso]
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
this : h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso
⊢ Eq (α := S.homology ≅ h.right.H) h.right.homologyIso (h.left.homologyIso ≪≫ h.iso)
have rw : Eq (α := S.homology ≅ h.right.H) h.right.homologyIso
  (h.left.homologyIso ≪≫ Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso)
Tactic: rw [this, Iso.self_symm_id_assoc]
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
this : h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso
rw :
  Eq (α := S.homology ≅ h.right.H) h.right.homologyIso
    (h.left.homologyIso ≪≫ Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso)
⊢ Eq (α := S.homology ≅ h.right.H) h.right.homologyIso (h.left.homologyIso ≪≫ h.iso)
have rw₁ : Eq (α := S.homology ≅ h.right.H) h.right.homologyIso h.right.homologyIso
Tactic: rw [this, Iso.self_symm_id_assoc]
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ≅ h.right.H) h.right.homologyIso (h.left.homologyIso ≪≫ h.iso)
have suffices : h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso
Tactic: suffices h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso by
    rw [this, Iso.self_symm_id_assoc]
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
⊢ h.iso = Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso
have w : h.iso.hom = (Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso).hom
Tactic: ext
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
⊢ h.iso.hom = (Iso.trans (Y := S.homology) (Iso.symm h.left.homologyIso) h.right.homologyIso).hom
have w : h.iso.hom = CategoryStruct.comp (Y := S.homology) (Iso.inv h.left.homologyIso) (Iso.hom h.right.homologyIso)
Tactic: dsimp
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
⊢ h.iso.hom = CategoryStruct.comp (Y := S.homology) (Iso.inv h.left.homologyIso) (Iso.hom h.right.homologyIso)
have w : h.iso.hom = leftRightHomologyComparison' h.left h.right
Tactic: rw [← leftRightHomologyComparison'_fac, leftRightHomologyComparison'_eq]
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
w : h.iso.hom = leftRightHomologyComparison' h.left h.right
⊢ h.iso.hom = CategoryStruct.comp (Y := S.homology) (Iso.inv h.left.homologyIso) (Iso.hom h.right.homologyIso)
have w₁ : h.iso.hom = h.iso.hom
Tactic: rw [← leftRightHomologyComparison'_fac, leftRightHomologyComparison'_eq]
-- 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
h : S.HomologyData
inst_2 : S.HasHomology
⊢ Eq (α := S.homology ≅ h.left.H) h.left.homologyIso (h.right.homologyIso ≪≫ h.iso.symm)
have rw : Eq (α := S.homology ≅ h.left.H) h.left.homologyIso ((h.left.homologyIso ≪≫ h.iso) ≪≫ h.iso.symm)
Tactic: rw [right_homologyIso_eq_left_homologyIso_trans_iso]
-- 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 : ShortComplex.{v, u} C
inst_2 : S.HasLeftHomology
inst_3 : S.HasRightHomology
h : IsIso (X := S.leftHomology) (Y := S.rightHomology) S.leftRightHomologyComparison
⊢ S.HasHomology
have this : IsIso (Y := S.rightHomologyData.H) (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData)
Tactic: haveI : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData) := 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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ leftHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have dsimp : Eq (α := S₁.homology ⟶ h₂.H)
  (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData)
      (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
    leftHomologyMap' φ h₁ h₂)
  (CategoryStruct.comp (Y := S₂.homology) (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)
    (CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) S₂.homologyData.left S₂.leftHomologyData)
      (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData h₂)))
Tactic: dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]
-- 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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ Eq (α := h₁.H ⟶ S₂.homology) (CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (homologyMap φ))
    (leftHomologyMap' φ h₁ h₂ ≫ Iso.inv h₂.homologyIso)
have dsimp : Eq (α := h₁.H ⟶ S₂.homology)
  (CategoryStruct.comp (Y := S₁.homology)
    (CategoryStruct.comp (Y := S₁.leftHomology) (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData)
      (leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left))
    (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left))
  (leftHomologyMap' φ h₁ h₂ ≫
    CategoryStruct.comp (Y := S₂.leftHomology) (leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData)
      (leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left))
Tactic: dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]
-- 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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have rw : CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂) =
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
Tactic: rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]
-- 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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw :
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂) =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have rw₁ : rightHomologyMap' φ h₁ h₂ =
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
Tactic: rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]
-- 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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw :
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂) =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₁ :
  rightHomologyMap' φ h₁ h₂ =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have rw₂ : leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ rightHomologyMap' φ h₁ h₂ =
  leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
Tactic: rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]
-- 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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw :
  CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂) =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₁ :
  rightHomologyMap' φ h₁ h₂ =
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
rw₂ :
  leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ rightHomologyMap' φ h₁ h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
        (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
⊢ Eq (α := S₁.homology ⟶ h₂.H) (Iso.hom h₁.homologyIso ≫ rightHomologyMap' φ h₁ h₂)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
have rw₃ : leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂ =
  leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
    CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
      (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
Tactic: rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
    ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
    ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
    ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
    LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]