-- 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)
    (Iso.hom
      (Iso.trans (Y := RightHomologyData.H (S := S.map F) (S.homologyData.right.map F))
        (RightHomologyData.homologyIso (S.homologyData.right.map F))
        (F.mapIso (Iso.symm S.homologyData.right.homologyIso))))
    (Iso.hom
      (Iso.trans (Y := LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))
        (LeftHomologyData.homologyIso (S.homologyData.left.map F))
        (F.mapIso (Iso.symm S.homologyData.left.homologyIso))))
have w : 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 := sorry, inv_hom_id := sorry }
            (rightHomologyData (S.map F)) (HomologyData.right (homologyData (S.map F)))))
      (Iso.hom
        (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := sorry, inv_hom_id := sorry }
          (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 := sorry, inv_hom_id := sorry } S.rightHomologyData
            S.homologyData.right))
        (Iso.hom
            (rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := sorry, inv_hom_id := sorry } 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 := sorry, inv_hom_id := sorry }
          (leftHomologyData (S.map F)) (HomologyData.left (homologyData (S.map F)))))
      (Iso.hom
        (leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := sorry, inv_hom_id := sorry }
          (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 := sorry, inv_hom_id := sorry } S.leftHomologyData
            S.homologyData.left))
        (Iso.hom
          (leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := sorry, inv_hom_id := sorry } S.leftHomologyData
            S.homologyData.left)))))
Tactic: dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, RightHomologyData.homologyIso,
    rightHomologyIso, RightHomologyData.rightHomologyIso, LeftHomologyData.homologyIso,
    leftHomologyIso, LeftHomologyData.leftHomologyIso]