-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_2 inst_4 _) T
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) T.obj₃ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
    (Functor.map (𝟭 C) T.mor₃ ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1) T.mor₃)
dsimp :
  Eq.{v_1 + 1} (α :=
    unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (op (op T.obj₁))) ⟶ op T.obj₃)
    (CategoryStruct.comp (Y := unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (op (op T.obj₁))))
      (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (𝟙 (op (op T.obj₁)))) :
        unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (op (op T.obj₁))) ⟶
          unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (op (op T.obj₁))))
      (Quiver.Hom.unop (NatTrans.app (Iso.hom (Functor.commShiftIso (opOp C) 1)) T.obj₁) ≫ T.mor₃.op :
        unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1) (op (op T.obj₁))) ⟶ op T.obj₃))
    (CategoryStruct.comp (Y :=
        unop
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1)
            (op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) (op T.obj₃)))))
        (Quiver.Hom.unop
          (Functor.map (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1)
            (CategoryStruct.comp (Y :=
              op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                  (op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁))))
              (Quiver.Hom.op (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.mor₃.op))
              (Quiver.Hom.op
                (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) (op T.obj₁))))))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence Cᵒᵖ 1))) (op (op T.obj₃)))) ≫
      𝟙 (op T.obj₃))
⊢ (Triangle.mor₃ (Functor.obj (Functor.mapTriangle (opOp C)) T) ≫
        Functor.map (shiftFunctor Cᵒᵖᵒᵖ (A := ℤ) 1)
          (Iso.hom (Iso.refl (Triangle.obj₁ (Functor.obj (Functor.mapTriangle (opOp C)) T))))).unop =
    (Iso.hom (Iso.refl (Triangle.obj₃ (Functor.obj (Functor.mapTriangle (opOp C)) T))) ≫
        (Functor.obj (Equivalence.functor (triangleOpEquivalence Cᵒᵖ))
            (op (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))).mor₃).unop

Tactic:
dsimp at this ⊢