-- 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:
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₃ ≅ (shiftFunctor (Triangle C) (-n₀)).obj (Triangle.mk f g h)

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_

Result:
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₃

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
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
let T := (Triangle.shiftFunctor C (-n₀)).obj (Triangle.mk f g h)

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)
⊢ ∃ X Y, ∃ (_ : t.le n₀ X) (_ : t.ge n₁ Y), ∃ f g h, Triangle.mk f g h ∈ distinguishedTriangles

Proof state:
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
⊢ T.mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) =
    𝟙 T.obj₃ ≫ ((-n₀).negOnePow • (shiftFunctor C (-n₀)).map h ≫ (shiftFunctorComm C 1 (-n₀)).hom.app X)

Tactic:
simp [T]

Result:
no goals