-- 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₂
⊢ 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₃))

Tactic:
rfl