-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
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
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 := ⋯, 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)))))
⊢ 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))))

Tactic:
dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, RightHomologyData.homologyIso,
    rightHomologyIso, RightHomologyData.rightHomologyIso, LeftHomologyData.homologyIso,
    leftHomologyIso, LeftHomologyData.leftHomologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.leftHomologyIso, CategoryTheory.Functor.mapIso