-- 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 (α :=
    T.obj₃ ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)))
    (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) (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃))
simp :
  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₃)
    (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ 1 (-1) instIsTriangulatedOppositeOpOp._proof_2))
          (op (op T.obj₁))) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C (-1) 1 instIsTriangulatedOppositeOpOp._proof_3)) (op T.obj₁) ≫
        (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁)).op)
    (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (shiftFunctorOpIso Cᵒᵖ 1 (-1) instIsTriangulatedOppositeOpOp._proof_2))
          (op (op T.obj₁))) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C (-1) 1 instIsTriangulatedOppositeOpOp._proof_3)) (op T.obj₁) ≫
        Quiver.Hom.op
            (CategoryStruct.comp (Y :=
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 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)
                (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
                  NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁))) ≫
          𝟙 (op T.obj₃))
⊢ 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₃))

Tactic:
simp only [shiftFunctor_op_map _ 1 (-1), Functor.op_obj,
      unop_id, shiftFunctor_op_map _ (-1) 1,
      commShiftIso_opOp_hom_app _ 1 (-1),
      opShiftFunctorEquivalence_counitIso_inv_app _ 1 (-1) (add_neg_cancel 1),
      unop_comp, Quiver.Hom.unop_op, Category.assoc, ← op_comp, Iso.inv_hom_id_app_assoc,
      shiftFunctorCompIsoId_op_hom_app, Iso.unop_hom_inv_id_app_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app, CategoryTheory.Category.assoc, add_neg_cancel, CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.Iso.unop_hom_inv_id_app_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.Pretriangulated.shiftFunctor_op_map, CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.Iso.inv_hom_id_app_assoc, Neg.neg, CategoryTheory.Functor.op_obj, CategoryTheory.unop_id