-- Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
lemma exists_triangle (A : C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
    ∃ (X Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y)
      (h : Y ⟶ X⟦(1 : ℤ)⟧), Triangle.mk f g h ∈ distTriang C

Proof state:
case refine_1
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
⊢ (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₁ ≫ e.symm.hom =
    (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁).hom ≫
      ((shiftFunctor (Triangle C) (-n₀)).obj (Triangle.mk f g h)).mor₁

case refine_2
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
⊢ (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₂ ≫
      (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃).hom =
    e.symm.hom ≫ ((shiftFunctor (Triangle C) (-n₀)).obj (Triangle.mk f g h)).mor₂

case refine_3
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
⊢ (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₃ ≫
      (shiftFunctor C 1).map (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁).hom =
    (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃).hom ≫
      ((shiftFunctor (Triangle C) (-n₀)).obj (Triangle.mk f g h)).mor₃

Tactic:
all_goals dsimp; simp [T]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
let e := (shiftEquiv C n₀).unitIso.symm.app A

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Proof state:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
have hT' : Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ∈ distTriang C := by
  refine isomorphic_distinguished _ (Triangle.shift_distinguished _ mem (-n₀)) _ ?_
  refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_
  all_goals dsimp; simp [T]

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
hT' : Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ∈ distinguishedTriangles
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
A : C
n₀ n₁ : ℤ
h✝ : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ (shiftFunctor C n₀).obj A
g : (shiftFunctor C n₀).obj A ⟶ Y
h : Y ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
T : Triangle C := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)
e : ((shiftEquiv C n₀).functor ⋙ (shiftEquiv C n₀).inverse).obj A ≅ (𝟭 C).obj A := (shiftEquiv C n₀).unitIso.symm.app A
hT' : Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ∈ distinguishedTriangles
⊢ -n₀ + n₁ = 1

Tactic:
omega

Result:
no goals