-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
rw₁ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso F)) (Iso.inv (S₂.mapHomologyIso F))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
rw₂ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (homologyMap (Functor.map F.mapShortComplex φ) ≫ 𝟙 (homology (S₂.map F)) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
rw₃ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (homologyMap (Functor.map F.mapShortComplex φ) : homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
rw₄ rw₅ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (homologyMap (Functor.map F.mapShortComplex φ) : homology (S₁.map F) ⟶ homology (S₂.map F))
    (homologyMap (Functor.map F.mapShortComplex φ) : homology (S₁.map F) ⟶ homology (S₂.map F))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
      (homologyMap (Functor.map F.mapShortComplex φ)))

Tactic:
rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom