-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.OpOp (goal)
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₃))
⊢ 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₃))
have 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 sorry)) T.obj₃)
            (Functor.map (shiftFunctor C (A := ℤ) 1)
              (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
                NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) 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]