-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology)
    (CategoryStruct.comp (Y := RightHomologyData.H (S := S.map F) (S.homologyData.right.map F))
      (CategoryStruct.comp (Y := rightHomology (S.map F))
        (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
          Iso.inv
            (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
              (rightHomologyData (S.map F)) (HomologyData.right (homologyData (S.map F)))))
        (Iso.hom
          (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (rightHomologyData (S.map F)) (S.homologyData.right.map F))))
      (F.map
        (CategoryStruct.comp (Y := S.rightHomology)
          (Iso.inv
            (rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData
              S.homologyData.right))
          (Iso.hom
              (rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData
                S.homologyData.right) ≫
            S.homologyData.iso.inv))))
    (CategoryStruct.comp (Y := LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))
      (CategoryStruct.comp (Y := leftHomology (S.map F))
        (Iso.inv
          (leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (leftHomologyData (S.map F)) (HomologyData.left (homologyData (S.map F)))))
        (Iso.hom
          (leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (leftHomologyData (S.map F)) (S.homologyData.left.map F))))
      (F.map
        (CategoryStruct.comp (Y := S.leftHomology)
          (Iso.inv
            (leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData
              S.homologyData.left))
          (Iso.hom
            (leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData
              S.homologyData.left)))))
have w : Eq (α := homology (S.map F) ⟶ F.obj S.homology)
  (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
      rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (S.homologyData.right.map F) ≫
        F.map S.homologyData.iso.inv :
    homology (S.map F) ⟶ F.obj S.homology)
  (leftHomologyMap' (𝟙 (S.map F)) (HomologyData.left (homologyData (S.map F))) (S.homologyData.left.map F) :
    LeftHomologyData.H (S := S.map F) (HomologyData.left (homologyData (S.map F))) ⟶
      LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))
Tactic: simp only [RightHomologyData.map_H, rightHomologyMapIso'_inv, rightHomologyMapIso'_hom, assoc,
    Functor.map_comp, RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
    Functor.map_id, LeftHomologyData.map_H, leftHomologyMapIso'_inv, leftHomologyMapIso'_hom,
    LeftHomologyData.map_leftHomologyMap', ← rightHomologyMap'_comp_assoc, ← leftHomologyMap'_comp,
    id_comp]