awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
inst_6 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
h :
  t.IsLE
    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) n
⊢ t.IsLE X n

Tactic:
exact t.isLE_of_iso (show X⟦a⟧⟦-a⟧ ≅ X from (shiftEquiv C a).unitIso.symm.app X) n

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.shiftEquiv, CategoryTheory.Triangulated.TStructure.isLE_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
inst_6 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsGE
    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) n

Tactic:
have h := t.isGE_shift (X⟦a⟧) n' (-a) n
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
inst_6 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
h :
  t.IsGE
    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) n
⊢ t.IsGE X n

Tactic:
t.isGE_of_iso (show X⟦a⟧⟦-a⟧ ≅ X from (shiftEquiv C a).unitIso.symm.app X) n

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.shiftEquiv, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
inst_6 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
h :
  t.IsGE
    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) n
⊢ t.IsGE X n

Tactic:
exact t.isGE_of_iso (show X⟦a⟧⟦-a⟧ ≅ X from (shiftEquiv C a).unitIso.symm.app X) n

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Triangulated.TStructure.isGE_of_iso, CategoryTheory.shiftEquiv, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
mp : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' → t.IsLE X n
mpr : t.IsLE X n → t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' ↔ t.IsLE X n

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsLE X n

Tactic:
t.isLE_of_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsLE X n

Tactic:
exact t.isLE_of_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsLE X n
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'

Tactic:
t.isLE_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isLE_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsLE X n
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'

Tactic:
exact t.isLE_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isLE_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
mp : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' → t.IsGE X n
mpr : t.IsGE X n → t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' ↔ t.IsGE X n

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsGE X n

Tactic:
t.isGE_of_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
⊢ t.IsGE X n

Tactic:
exact t.isGE_of_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsGE X n
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'

Tactic:
t.isGE_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isGE_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
h : t.IsGE X n
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'

Tactic:
exact t.isGE_shift X n a n' hn'

Premises used: CategoryTheory.Triangulated.TStructure.isGE_shift
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0

Tactic:
have := t.isLE_shift X n₀ n₀ 0 (add_zero n₀)
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)

Tactic:
have := t.isGE_shift Y n₁ n₀ (n₁ - n₀)
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1

Tactic:
have := t.isGE_of_ge (Y⟦n₀⟧) 1 (n₁ - n₀)
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
a :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) (Functor.map (shiftFunctor C n₀) 0)
⊢ f = 0

Tactic:
apply (shiftFunctor C n₀).map_injective

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
a :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) (Functor.map (shiftFunctor C n₀) 0)

Tactic:
simp only [Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
a : t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X)
a₁ : t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) 0

Tactic:
apply t.zero'

Premises used: CategoryTheory.Triangulated.TStructure.zero'
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
⊢ t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X)

Tactic:
apply t.le_of_isLE

Premises used: CategoryTheory.Triangulated.TStructure.le_of_isLE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
⊢ t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)

Tactic:
apply t.ge_of_isGE

Premises used: CategoryTheory.Triangulated.TStructure.ge_of_isGE
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
h_1 : t.IsLE X n₀
h_2 : t.IsGE Y n₁
⊢ f = 0

Tactic:
t.zero f n₀ n₁ h

Premises used: CategoryTheory.Triangulated.TStructure.zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE X n₁
rw : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ IsZero.{v_1, u_1} X

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE X n₁
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
t.zero _ n₀ n₁ h

Premises used: CategoryTheory.Triangulated.TStructure.zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE X n₁
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
exact t.zero _ n₀ n₁ h

Premises used: CategoryTheory.Triangulated.TStructure.zero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
e : X ≅ Y
n : ℤ
h : t.IsLE X n
⊢ t.minus Y

Tactic:
⟨_, t.isLE_of_iso e n⟩

Premises used: CategoryTheory.Triangulated.TStructure.minus, CategoryTheory.Triangulated.TStructure.isLE_of_iso, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
e : X ≅ Y
n : ℤ
h : t.IsLE X n
⊢ t.minus Y

Tactic:
exact ⟨_, t.isLE_of_iso e n⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
n : ℤ
X : C
i : ℤ
h : t.IsLE X i
⊢ n + (i - n) = i

Tactic:
omega
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
n : ℤ
X : C
i : ℤ
h : t.IsLE X i
⊢ t.minus.shift n X

Tactic:
exact ⟨i - n, t.isLE_shift _ i _ _ (by omega)⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
e : X ≅ Y
n : ℤ
h : t.IsGE X n
⊢ t.plus Y

Tactic:
⟨_, t.isGE_of_iso e n⟩

Premises used: CategoryTheory.Triangulated.TStructure.plus, CategoryTheory.Triangulated.TStructure.isGE_of_iso, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
X Y : C
e : X ≅ Y
n : ℤ
h : t.IsGE X n
⊢ t.plus Y

Tactic:
exact ⟨_, t.isGE_of_iso e n⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
n : ℤ
X : C
i : ℤ
h : t.IsGE X i
⊢ n + (i - n) = i

Tactic:
omega
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
n : ℤ
X : C
i : ℤ
h : t.IsGE X i
⊢ t.plus.shift n X

Tactic:
exact ⟨i - n, t.isGE_shift _ i _ _ (by omega)⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
⊢ (t.plus ⊓ t.minus).IsClosedUnderIsomorphisms

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
⊢ (t.plus ⊓ t.minus).IsStableUnderShift ℤ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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 : TStructure.{v_1, u_1} C
f : Quiver.Hom (V := EInt) ⊥ ⊥
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id