-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasBinaryBiproducts.{v, u_1} C
X₁ X₂ X₃ : CochainComplex.{v, u_1, 0} C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
inst_3 : HasZeroObject.{v, u_1} C
dsimp :
  Eq (α :=
    Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f)))
    (CategoryStruct.comp (Y :=
        Functor.obj (quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (mappingCone f)))
        (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          ((mappingCone.triangle g).mor₃ ≫
            CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u_1, 0} C ℤ) (A := ℤ) 1)
              (mappingCone.inr f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f)) ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (𝟙 (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f))))
    (CategoryStruct.comp (Y :=
      Functor.obj (quotient C (ComplexShape.up ℤ))
        (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
          (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
          (HomotopyEquiv.hom (mappingConeCompHomotopyEquiv f g)) :
        Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone g) ⟶
          Functor.obj (quotient C (ComplexShape.up ℤ))
            (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))))
      (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ))
            (mappingCone.triangle (K := mappingCone f) (L := mappingCone (f ≫ g))
                (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) (mappingCone f) :
        Functor.obj (quotient C (ComplexShape.up ℤ))
            (mappingCone (F := mappingCone f) (G := mappingCone (f ≫ g))
              (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯ : mappingCone f ⟶ mappingCone (f ≫ g))) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (quotient C (ComplexShape.up ℤ)) (mappingCone f))))
⊢ (mappingConeCompTriangleh f g).mor₃ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Iso.hom (Iso.refl (mappingConeCompTriangleh f g).obj₁)) =
    Iso.hom (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)) ≫
      (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₃

Tactic:
dsimp [mappingConeCompTriangleh]

Premises used: CochainComplex.mappingConeCompTriangleh