-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T₁ T₂ : (Triangle.{v_1, u_1} C)ᵒᵖ
φ : T₁ ⟶ T₂
rw :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Opposite.unop T₁).obj₁ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
            (Opposite.op (Opposite.unop T₁).obj₁) :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₁).obj₁) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Opposite.unop T₁).obj₁))
        (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₂).obj₁)))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) φ.unop.hom₁)))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃)) :
      Opposite.op (Opposite.unop T₁).obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (opShiftFunctorEquivalence C 1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (opShiftFunctorEquivalence C 1))
            (Opposite.op (Opposite.unop T₁).obj₁)))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
            (Opposite.op (Opposite.unop T₁).obj₁) :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₁).obj₁) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C 1) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C 1))
              (Opposite.op (Opposite.unop T₁).obj₁))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (opShiftFunctorEquivalence C 1))
            (Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (opShiftFunctorEquivalence C 1))
              (Opposite.op (Opposite.unop T₂).obj₁)))
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) φ.unop.hom₁.op.unop)))
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op)) :
      Opposite.op (Opposite.unop T₁).obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
⊢ Eq.{v_1 + 1} (α :=
    Opposite.op (Opposite.unop T₁).obj₁ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃))
        (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
                (Opposite.op (Opposite.unop T₁).obj₁) :
              Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₁).obj₁) ⟶
                Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                  (Opposite.op (Opposite.unop T₁).obj₁))
            (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₁).mor₃.op :
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁).obj₁)) ⟶
                Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃)) :
          Opposite.op (Opposite.unop T₁).obj₁ ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃))
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) φ.unop.hom₃.op :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₁).obj₃) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃)) :
      Opposite.op (Opposite.unop T₁).obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))
    (φ.unop.hom₁.op ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₂).obj₁)))
          (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1)))
              (Opposite.op (Opposite.unop T₂).obj₁) :
            Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op (Opposite.unop T₂).obj₁) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Opposite.unop T₂).obj₁))
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.unop T₂).mor₃.op :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₂).obj₁)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃)) :
      Opposite.op (Opposite.unop T₁).obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Opposite.op (Opposite.unop T₂).obj₃))

Tactic:
rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp,
          opShiftFunctorEquivalence_counitIso_inv_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, Quiver.Hom.unop, CategoryTheory.Functor.map_comp