-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma mapHomologyIso'_eq_mapHomologyIso [S.HasHomology] [F.PreservesLeftHomologyOf S]
    [F.PreservesRightHomologyOf S] :
    S.mapHomologyIso' F = S.mapHomologyIso F

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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapHomologyIso' F).hom = (S.mapHomologyIso F).hom

Tactic:
rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]

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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ ((S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm).hom =
    ((S.homologyData.left.map F).homologyIso ≪≫ F.mapIso S.homologyData.left.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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ ((S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm).hom =
    ((S.homologyData.left.map F).homologyIso ≪≫ F.mapIso S.homologyData.left.homologyIso.symm).hom

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

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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (((S.map F).homologyData.iso.hom ≫
          (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
              (S.map F).rightHomologyData (S.map F).homologyData.right).inv) ≫
        (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (S.map F).rightHomologyData (S.homologyData.right.map F)).hom) ≫
      F.map
        ((rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData
              S.homologyData.right).inv ≫
          (rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData
                S.homologyData.right).hom ≫
            S.homologyData.iso.inv) =
    ((leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (S.map F).leftHomologyData (S.map F).homologyData.left).inv ≫
        (leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ }
            (S.map F).leftHomologyData (S.homologyData.left.map F)).hom) ≫
      F.map
        ((leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData
              S.homologyData.left).inv ≫
          (leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData
              S.homologyData.left).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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)
⊢ (S.map F).homologyData.iso.hom ≫
      rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫
        F.map S.homologyData.iso.inv =
    leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)

Tactic:
have eq := γ.comm

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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)
eq : γ.left.φH ≫ (S.homologyData.map F).iso.hom = (S.map F).homologyData.iso.hom ≫ γ.right.φH
⊢ (S.map F).homologyData.iso.hom ≫
      rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫
        F.map S.homologyData.iso.inv =
    leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)

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

Tactic:
dsimp at eq

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

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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapHomologyIso' F = S.mapHomologyIso F

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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapHomologyIso' F).hom = (S.mapHomologyIso F).hom