-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapHomologyIso_hom_naturality [S₁.HasHomology] [S₂.HasHomology]
    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ ≫
      (S₂.mapHomologyIso F).hom = (S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso F).hom = (S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ)

Tactic:
dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso,
  LeftHomologyData.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
  Iso.symm, Iso.trans, Iso.refl]

Result:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap' (F.mapShortComplex.map φ) (S₁.map F).homologyData.left (S₂.map F).homologyData.left ≫
      leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).homologyData.left (S₂.map F).leftHomologyData ≫
        leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.homologyData.left.map F) =
    (leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).homologyData.left (S₁.map F).leftHomologyData ≫
        leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.homologyData.left.map F)) ≫
      F.map (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{u_3, u_1} C
inst✝⁹ : Category.{u_4, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap' (F.mapShortComplex.map φ) (S₁.map F).homologyData.left (S₂.map F).homologyData.left ≫
      leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).homologyData.left (S₂.map F).leftHomologyData ≫
        leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.homologyData.left.map F) =
    (leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).homologyData.left (S₁.map F).leftHomologyData ≫
        leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.homologyData.left.map F)) ≫
      F.map (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)

Tactic:
simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]

Result:
no goals