-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma mem_distinguishedTriangles_iff' (T : Triangle Cᵒᵖ) :
    T ∈ distinguishedTriangles C ↔
      ∃ (T' : Triangle C) (_ : T' ∈ distTriang C),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Proof state:
case mpr.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
T' : Triangle C
hT' : T' ∈ Pretriangulated.distinguishedTriangles
e : T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
refine isomorphic_distinguished _ hT' _ ?_

Result:
case mpr.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
T' : Triangle C
hT' : T' ∈ Pretriangulated.distinguishedTriangles
e : T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ≅ T'

Proof state:
case mp
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles →
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
intro hT

Result:
case mp
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
hT : Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
⊢ ∃ T',
    ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
      Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
rw [mem_distinguishedTriangles_iff]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Proof state:
case mpr.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
T' : Triangle C
hT' : T' ∈ Pretriangulated.distinguishedTriangles
e : T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ≅ T'

Tactic:
exact Iso.unop ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫
  (triangleOpEquivalence C).inverse.mapIso e.symm)

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles →
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

case mpr
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))) →
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Proof state:
case mpr
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))) →
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rintro ⟨T', hT', ⟨e⟩⟩

Result:
case mpr.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
T' : Triangle C
hT' : T' ∈ Pretriangulated.distinguishedTriangles
e : T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Proof state:
case mp
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
hT : Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
⊢ ∃ T',
    ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
      Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
exact ⟨_ ,hT, ⟨(triangleOpEquivalence C).counitIso.symm.app T⟩⟩

Result:
no goals