-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
/-- If `F.op` is triangulated, so is `F`.
-/
lemma isTriangulated_of_op [F.op.IsTriangulated] : F.IsTriangulated where
  map_distinguished T dT

Proof state:
case hT
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this✝ :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence C).functor ⋙ (triangleOpEquivalence C).inverse).obj (op T)) ∈
      Pretriangulated.distinguishedTriangles ↔
    T ∈ Pretriangulated.distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (op T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rw [← this, Functor.comp_obj, ← mem_distTriang_op_iff] at dT

Result:
case hT
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : (triangleOpEquivalence C).functor.obj (op T) ∈ Pretriangulated.distinguishedTriangles
this✝ :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence C).functor ⋙ (triangleOpEquivalence C).inverse).obj (op T)) ∈
      Pretriangulated.distinguishedTriangles ↔
    T ∈ Pretriangulated.distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (op T) ∈ Pretriangulated.distinguishedTriangles

Proof state:
case hT
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this✝ :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence C).functor ⋙ (triangleOpEquivalence C).inverse).obj (op T)) ∈
      Pretriangulated.distinguishedTriangles ↔
    unop ((𝟭 (Triangle C)ᵒᵖ).obj (op T)) ∈ Pretriangulated.distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (op T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rw [Functor.id_obj, Opposite.unop_op T] at this

Result:
case hT
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this✝ :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence C).functor ⋙ (triangleOpEquivalence C).inverse).obj (op T)) ∈
      Pretriangulated.distinguishedTriangles ↔
    T ∈ Pretriangulated.distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (op T) ∈ Pretriangulated.distinguishedTriangles

Proof state:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).obj (op T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
apply F.op.map_distinguished

Result:
case hT
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (op T) ∈ Pretriangulated.distinguishedTriangles

Proof state:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
⊢ F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles

Tactic:
have := distinguished_iff_of_iso ((triangleOpEquivalence D).unitIso.app
  (Opposite.op (F.mapTriangle.obj T))).unop

Result:
C : Type u_1
D : Type u_2
inst✝¹³ : Category.{u_3, u_1} C
inst✝¹² : Category.{u_4, u_2} D
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
F : C ⥤ D
inst✝⁹ : F.CommShift ℤ
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasZeroObject D
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
inst✝ : F.op.IsTriangulated
T : Triangle C
dT : T ∈ Pretriangulated.distinguishedTriangles
this :
  unop (((triangleOpEquivalence D).functor ⋙ (triangleOpEquivalence D).inverse).obj (op (F.mapTriangle.obj T))) ∈
      Pretriangulated.distinguishedTriangles ↔
    unop ((𝟭 (Triangle D)ᵒᵖ).obj (op (F.mapTriangle.obj T))) ∈ Pretriangulated.distinguishedTriangles
⊢ F.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles