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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
ha : H a
⊢ H (a + 1)

Tactic:
exact H_add a 1 _ rfl ha H_one

Premises used: OfNat.ofNat, rfl
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
zero : H 0
succ : ∀ (a : ℕ) (ha : H a), H (a + 1)
⊢ H a

Tactic:
induction a with
  | zero => exact H_zero
  | succ a ha => exact H_add a 1 _ rfl ha H_one
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
obtain : ∀ (a : ℕ) (ha : n₁ - n₀ = (↑a : ℤ)), t.ge n₁ ≤ t.ge n₀
⊢ t.ge n₁ ≤ t.ge n₀

Tactic:
obtain ⟨a, ha⟩ := Int.nonneg_def.1 h

Premises used: Iff.mp, Int.nonneg_def
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
a : ℕ
ha : n₁ - n₀ = (↑a : ℤ)
⊢ n₁ = n₀ + (↑a : ℤ)

Tactic:
lia
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
a : ℕ
ha : n₁ - n₀ = (↑a : ℤ)
obtain : ∀ (h : n₀ ≤ n₀ + (↑a : ℤ)) (ha : n₀ + (↑a : ℤ) - n₀ = (↑a : ℤ)), t.ge (n₀ + (↑a : ℤ)) ≤ t.ge n₀
⊢ t.ge n₁ ≤ t.ge n₀

Tactic:
obtain rfl : n₁ = n₀ + a := by lia

Premises used: rfl
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ : ℤ
a : ℕ
h : n₀ ≤ n₀ + (↑a : ℤ)
ha : n₀ + (↑a : ℤ) - n₀ = (↑a : ℤ)
⊢ t.ge (n₀ + (↑a : ℤ)) ≤ t.ge n₀

Tactic:
apply this
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
suffices : ∀ (a : ℕ), H a
⊢ Antitone t.ge

Tactic:
suffices ∀ (a : ℕ), H a by
    intro n₀ n₁ h
    obtain ⟨a, ha⟩ := Int.nonneg_def.1 h
    obtain rfl : n₁ = n₀ + a := by lia
    apply this
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
n : ℤ
simp : t.ge n ≤ t.ge n
⊢ t.ge (n + (↑0 : ℤ)) ≤ t.ge n

Tactic:
simp only [Nat.cast_zero, add_zero]

Premises used: Nat.cast_zero, add_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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
n : ℤ
⊢ t.ge n ≤ t.ge n

Tactic:
rfl
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
⊢ H 0

Tactic:
have H_zero : H 0 := fun n => by
    simp only [Nat.cast_zero, add_zero]
    rfl
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge (n + (↑1 : ℤ)) X
⊢ n + 1 = n + (↑1 : ℤ)

Tactic:
simp
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge (n + (↑1 : ℤ)) X
⊢ t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)

Tactic:
rw [← t.shift_ge n 1 (n + (1 : ℕ)) (by simp), ObjectProperty.prop_shift_iff] at hX

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff, Nat.cast, CategoryTheory.Triangulated.TStructure.shift_ge, HAdd.hAdd, OfNat.ofNat
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
rw : (t.ge 0).shift n X
⊢ t.ge n X

Tactic:
rw [← t.shift_ge n 0 n (add_zero n)]

Premises used: CategoryTheory.Triangulated.TStructure.shift_ge, add_zero, OfNat.ofNat
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
⊢ (t.ge 0).shift n X

Tactic:
t.ge_one_le _ hX

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.Triangulated.TStructure.ge_one_le
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
⊢ (t.ge 0).shift n X

Tactic:
exact t.ge_one_le _ hX

Premises used: CategoryTheory.Triangulated.TStructure.ge_one_le
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
⊢ H 1

Tactic:
have H_one : H 1 := fun n X hX => by
    rw [← t.shift_ge n 1 (n + (1 : ℕ)) (by simp), ObjectProperty.prop_shift_iff] at hX
    rw [← t.shift_ge n 0 n (add_zero n)]
    exact t.ge_one_le _ hX
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
rw : t.ge (n + (↑a : ℤ) + (↑b : ℤ)) ≤ t.ge n
⊢ t.ge (n + (↑c : ℤ)) ≤ t.ge n

Tactic:
rw [← h, Nat.cast_add, ← add_assoc]

Premises used: add_assoc, Nat.cast_add
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.ge (n + (↑a : ℤ) + (↑b : ℤ)) ≤ t.ge n

Tactic:
(hb (n + a)).trans (ha n)

Premises used: Nat.cast, HAdd.hAdd, LE.le.trans
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.ge (n + (↑a : ℤ) + (↑b : ℤ)) ≤ t.ge n

Tactic:
exact (hb (n + a)).trans (ha n)

Premises used: Nat.cast, HAdd.hAdd, LE.le.trans
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
⊢ ∀ (a b c : ℕ), a + b = c → H a → H b → H c

Tactic:
have H_add : ∀ (a b c : ℕ) (_ : a + b = c) (_ : H a) (_ : H b), H c := by
    intro a b c h ha hb n
    rw [← h, Nat.cast_add, ← add_assoc]
    exact (hb (n + a)).trans (ha 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
⊢ H 0

Tactic:
H_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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
⊢ H 0

Tactic:
exact H_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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
ha : H a
⊢ H (a + 1)

Tactic:
H_add a 1 _ rfl ha H_one

Premises used: OfNat.ofNat, rfl
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
ha : H a
⊢ H (a + 1)

Tactic:
exact H_add a 1 _ rfl ha H_one

Premises used: OfNat.ofNat, rfl
-- 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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.ge (n + (↑a : ℤ)) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
zero : H 0
succ : ∀ (a : ℕ) (ha : H a), H (a + 1)
⊢ H a

Tactic:
induction a with
  | zero => exact H_zero
  | succ a ha => exact H_add a 1 _ rfl ha H_one
-- 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 : ℤ
inst_6 : t.IsLE X n
⊢ t.le n X

Tactic:
IsLE.le

Premises used: CategoryTheory.Triangulated.TStructure.IsLE.le
-- 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 : ℤ
inst_6 : t.IsGE X n
⊢ t.ge n X

Tactic:
IsGE.ge

Premises used: CategoryTheory.Triangulated.TStructure.IsGE.ge
-- 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 : ℤ
⊢ t.le n X ↔ t.IsLE X n

Tactic:
⟨fun h ↦ ⟨h⟩, fun _ ↦ t.le_of_isLE X n⟩

Premises used: CategoryTheory.Triangulated.TStructure.le_of_isLE, CategoryTheory.Triangulated.TStructure.IsLE.mk, Iff.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 : C
n : ℤ
⊢ t.ge n X ↔ t.IsGE X n

Tactic:
⟨fun h ↦ ⟨h⟩, fun _ ↦ t.ge_of_isGE X n⟩

Premises used: CategoryTheory.Triangulated.TStructure.ge_of_isGE, Iff.intro, CategoryTheory.Triangulated.TStructure.IsGE.mk
-- 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 Y : C
e : X ≅ Y
h : t.le n X
simp : ∀ (h : t.IsLE X n), t.IsLE Y n
⊢ t.le n Y

Tactic:
simp only [le_iff_isLE] at h ⊢

Premises used: CategoryTheory.Triangulated.TStructure.le_iff_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
n : ℤ
X Y : C
e : X ≅ Y
h : t.IsLE X n
⊢ t.IsLE Y n

Tactic:
t.isLE_of_iso e _

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_iso
-- 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 Y : C
e : X ≅ Y
h : t.IsLE X n
⊢ t.IsLE Y n

Tactic:
exact t.isLE_of_iso e _

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_iso
-- 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 Y : C
e : X ≅ Y
h : t.ge n X
simp : ∀ (h : t.IsGE X n), t.IsGE Y n
⊢ t.ge n Y

Tactic:
simp only [ge_iff_isGE] at h ⊢

Premises used: CategoryTheory.Triangulated.TStructure.ge_iff_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
n : ℤ
X Y : C
e : X ≅ Y
h : t.IsGE X n
⊢ t.IsGE Y n

Tactic:
t.isGE_of_iso e _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso
-- 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 Y : C
e : X ≅ Y
h : t.IsGE X n
⊢ t.IsGE Y n

Tactic:
exact t.isGE_of_iso e _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso
-- 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 X n
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'

Tactic:
⟨t.le_shift n a n' hn' X (t.le_of_isLE X n)⟩

Premises used: CategoryTheory.Triangulated.TStructure.le_of_isLE, CategoryTheory.Triangulated.TStructure.IsLE.mk, CategoryTheory.Triangulated.TStructure.le_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
inst_6 : t.IsGE X n
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'

Tactic:
⟨t.ge_shift n a n' hn' X (t.ge_of_isGE X n)⟩

Premises used: CategoryTheory.Triangulated.TStructure.ge_of_isGE, CategoryTheory.Triangulated.TStructure.ge_shift, CategoryTheory.Triangulated.TStructure.IsGE.mk
-- 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'
⊢ 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

Tactic:
have h := t.isLE_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.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:
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