-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma LeftHomologyData.mapHomologyIso_eq [S.HasHomology]
    [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] :
    S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm

Proof state:
case w
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 : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapHomologyIso F).hom = ((hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm).hom

Tactic:
dsimp only [mapHomologyIso, homologyIso, ShortComplex.leftHomologyIso,
  leftHomologyMapIso', leftHomologyIso, Functor.mapIso,
  Iso.symm, Iso.trans, Iso.refl]

Result:
case w
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 : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ 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 (hl.map F)) ≫
      F.map
        (leftHomologyMap' (𝟙 S) hl S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData 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 : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm

Tactic:
ext

Result:
case w
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 : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapHomologyIso F).hom = ((hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm).hom

Proof state:
case w
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 : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ 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 (hl.map F)) ≫
      F.map
        (leftHomologyMap' (𝟙 S) hl S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left)

Tactic:
simp only [F.map_comp, map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id,
  Functor.map_id, Functor.mapShortComplex_obj]

Result:
no goals