-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
dsimp :
  Eq (α :=
    Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K) ⟶
      Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
    ((-CategoryTheory.Functor.map
          (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ)) ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryStruct.comp (Y :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))
      (CategoryStruct.comp (Y :=
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) K))
          (NatTrans.app (Iso.inv (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (HomotopyEquiv.hom (rotateHomotopyEquiv φ))) :
        Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K) ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)))
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (triangle (L := mappingCone φ) (inr φ)).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) L :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone (G := mappingCone φ) (inr φ)) ⟶
          Functor.obj (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
⊢ (triangleh φ).rotate.mor₃ ≫
      CategoryTheory.Functor.map
        (CategoryTheory.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangleh φ).rotate.obj₁)) =
    Iso.hom
        (Iso.app (Iso.symm (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1)) K ≪≫
          HomotopyCategory.isoOfHomotopyEquiv (rotateHomotopyEquiv φ)) ≫
      (triangleh (L := mappingCone φ) (inr φ)).mor₃

Tactic:
dsimp