-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma homologyMap_eq :
    homologyMap φ = h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ = h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv

Tactic:
dsimp [homologyMap, homologyMap', RightHomologyData.homologyIso,
  rightHomologyIso, RightHomologyData.rightHomologyIso]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    ((S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData ≫
          rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
γ' : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    ((S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData ≫
          rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv

Tactic:
simp only [← γ.rightHomologyMap'_eq, assoc, ← rightHomologyMap'_comp_assoc,
  id_comp, comp_id, γ'.left.leftHomologyMap'_eq, γ'.right.rightHomologyMap'_eq, ← γ'.comm_assoc,
  Iso.hom_inv_id]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    ((S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData ≫
          rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv

Tactic:
have γ' : HomologyMapData φ S₁.homologyData S₂.homologyData := default

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
γ' : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    ((S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData ≫
          rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv