-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma RightHomologyData.mapHomologyIso'_eq [S.HasHomology]
    [(S.map F).HasHomology] [F.PreservesRightHomologyOf S] :
    S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.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
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapHomologyIso' F).hom = ((hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm).hom

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

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
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (((S.map F).homologyData.iso.hom ≫
          rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫
        rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.homologyData.right.map F)) ≫
      F.map
        (rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData ≫
          rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv) =
    (((S.map F).homologyData.iso.hom ≫
          rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫
        rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F)) ≫
      F.map
        (rightHomologyMap' (𝟙 S) hr S.rightHomologyData ≫
          rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv)

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
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.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
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapHomologyIso' F).hom = ((hr.map F).homologyIso ≪≫ F.mapIso hr.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
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (((S.map F).homologyData.iso.hom ≫
          rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫
        rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.homologyData.right.map F)) ≫
      F.map
        (rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData ≫
          rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv) =
    (((S.map F).homologyData.iso.hom ≫
          rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫
        rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F)) ≫
      F.map
        (rightHomologyMap' (𝟙 S) hr S.rightHomologyData ≫
          rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv)

Tactic:
simp only [assoc, F.map_comp, map_rightHomologyMap', ← rightHomologyMap'_comp_assoc]

Result:
no goals