-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma homologyMap_op [HasHomology S₁] [HasHomology S₂] :
    (homologyMap φ).op =
      (S₂.homologyOpIso).inv ≫ homologyMap (opMap φ) ≫ (S₁.homologyOpIso).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₂.homologyData.iso.inv.op ≫
      homologyMap' (opMap φ) S₂.homologyData.op S₁.homologyData.op ≫ S₁.homologyData.iso.hom.op =
    (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫
      homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫
        (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom

Tactic:
dsimp only [Iso.symm, Iso.trans, Iso.op, Iso.refl, rightHomologyIso, leftHomologyIso,
  leftHomologyOpIso, leftHomologyMapIso', rightHomologyMapIso',
  LeftHomologyData.leftHomologyIso, homologyMap']

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

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap φ).op = S₂.homologyOpIso.inv ≫ homologyMap (opMap φ) ≫ S₁.homologyOpIso.hom

Tactic:
dsimp only [homologyMap, homologyOpIso]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap' φ S₁.homologyData S₂.homologyData).op =
    (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫
      homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫
        (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap' φ S₁.homologyData S₂.homologyData).op =
    (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫
      homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫
        (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom

Tactic:
rw [homologyMap'_op]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₂.homologyData.iso.inv.op ≫
      homologyMap' (opMap φ) S₂.homologyData.op S₁.homologyData.op ≫ S₁.homologyData.iso.hom.op =
    (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫
      homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫
        (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom

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

Tactic:
simp only [assoc, rightHomologyMap'_op, op_comp, ← leftHomologyMap'_comp_assoc, id_comp,
  opMap_id, comp_id, HomologyData.op_left]

Result:
no goals