-- 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))
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))
rw₄ :
  Eq (α := S₁.homology ⟶ h₂.H)
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂)
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
        CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
          (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
rw₅ :
  Eq (α := S₁.homology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ)
      (Iso.hom S₂.leftHomologyData.homologyIso ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂))
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
        CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
          (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
rw₆ :
  Eq (α := S₁.homology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ)
      (Iso.hom S₂.leftHomologyData.homologyIso ≫
        CategoryStruct.comp (Y := S₂.homology) (Iso.inv S₂.leftHomologyData.homologyIso) (Iso.hom h₂.homologyIso)))
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫
        CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
          (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
rw₇ :
  Eq (α := S₁.homology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ)
      (Iso.hom S₂.leftHomologyData.homologyIso ≫
        CategoryStruct.comp (Y := S₂.homology) (Iso.inv S₂.leftHomologyData.homologyIso) (Iso.hom h₂.homologyIso)))
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv S₁.leftHomologyData.homologyIso) (Iso.hom h₁.homologyIso) ≫
        CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
          (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso)))
rw₈ :
  Eq (α := S₁.homology ⟶ h₂.H)
    (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ)
      (Iso.hom S₂.leftHomologyData.homologyIso ≫
        CategoryStruct.comp (Y := S₂.homology) (Iso.inv S₂.leftHomologyData.homologyIso) (Iso.hom h₂.homologyIso)))
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv S₁.leftHomologyData.homologyIso)
        (Iso.hom h₁.homologyIso ≫
          CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
            (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))))
rw₉ :
  Eq (α := S₁.homology ⟶ h₂.H) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
    (Iso.hom S₁.leftHomologyData.homologyIso ≫
      CategoryStruct.comp (Y := S₁.homology) (Iso.inv S₁.leftHomologyData.homologyIso)
        (Iso.hom h₁.homologyIso ≫
          CategoryStruct.comp (Y := S₁.homology) (Iso.inv h₁.homologyIso)
            (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))))
rw₁₀ :
  Eq (α := S₁.homology ⟶ h₂.H) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom h₂.homologyIso))
    (Iso.hom h₁.homologyIso ≫
      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₁₁ : Eq (α := S₁.homology ⟶ h₂.H) (CategoryStruct.comp (Y := S₂.homology) (homologyMap φ) (Iso.hom 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]