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
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃)

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 simp [T]
-- 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
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃)
⊢ -n₀ + n₁ = 1

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
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃)
⊢ ∃ (X : C) (Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h :
    Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f g h)

Tactic:
exact ⟨_, _, t.le_shift _ _ _ (neg_add_cancel n₀) _ hX,
    t.ge_shift _ _ _ (by lia) _ hY, _, _, _, hT'⟩
-- 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
a n n' : ℤ
hn' : a + n = n'
h : ∀ (X : C), (t.le n).shift a X ↔ t.le n' X
⊢ (t.le n).shift a = t.le n'

Tactic:
ext X
-- 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
a n n' : ℤ
hn' : a + n = n'
X : C
h : (t.le n).shift a X → t.le n' X
h₁ : t.le n' X → (t.le n).shift a X
⊢ (t.le n).shift a X ↔ t.le n' X

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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : (t.le n).shift a X
⊢ -a + n' = n

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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : (t.le n).shift a X
⊢ t.le n' X

Tactic:
exact ((t.le n').prop_iff_of_iso ((shiftEquiv C a).unitIso.symm.app X)).1
      (t.le_shift n (-a) n' (by lia) _ hX)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.shiftEquiv, CategoryTheory.Triangulated.TStructure.le_shift, CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.symm, Iff.mp, CategoryTheory.Iso.app, Neg.neg, CategoryTheory.Triangulated.TStructure.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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : t.le n' X
⊢ (t.le n).shift a X

Tactic:
t.le_shift _ _ _ hn' X hX

Premises used: CategoryTheory.ObjectProperty.shift, 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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : t.le n' X
⊢ (t.le n).shift a X

Tactic:
exact t.le_shift _ _ _ hn' X hX

Premises used: 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
a n n' : ℤ
hn' : a + n = n'
h : ∀ (X : C), (t.ge n).shift a X ↔ t.ge n' X
⊢ (t.ge n).shift a = t.ge n'

Tactic:
ext X
-- 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
a n n' : ℤ
hn' : a + n = n'
X : C
h : (t.ge n).shift a X → t.ge n' X
h₁ : t.ge n' X → (t.ge n).shift a X
⊢ (t.ge n).shift a X ↔ t.ge n' X

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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : (t.ge n).shift a X
⊢ -a + n' = n

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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : (t.ge n).shift a X
⊢ t.ge n' X

Tactic:
exact ((t.ge n').prop_iff_of_iso ((shiftEquiv C a).unitIso.symm.app X)).1
      (t.ge_shift n (-a) n' (by lia) _ hX)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.shiftEquiv, CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.symm, Iff.mp, CategoryTheory.Triangulated.TStructure.ge_shift, CategoryTheory.Iso.app, CategoryTheory.Triangulated.TStructure.ge, Neg.neg
-- 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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : t.ge n' X
⊢ (t.ge n).shift a X

Tactic:
t.ge_shift _ _ _ hn' X hX

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.Triangulated.TStructure.ge_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
a n n' : ℤ
hn' : a + n = n'
X : C
hX : t.ge n' X
⊢ (t.ge n).shift a X

Tactic:
exact t.ge_shift _ _ _ hn' X hX

Premises used: CategoryTheory.Triangulated.TStructure.ge_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
H : (a : ℕ) → Prop := fun (a : ℕ) ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + (↑a : ℤ))
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
obtain : ∀ (a : ℕ) (ha : n₁ - n₀ = (↑a : ℤ)), t.le n₀ ≤ t.le n₁
⊢ t.le n₀ ≤ t.le 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.le n ≤ t.le (n + (↑a : ℤ))
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.le n ≤ t.le (n + (↑a : ℤ))
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.le n₀ ≤ t.le (n₀ + (↑a : ℤ))
⊢ t.le n₀ ≤ t.le 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.le n ≤ t.le (n + (↑a : ℤ))
this : ∀ (a : ℕ), H a
n₀ : ℤ
a : ℕ
h : n₀ ≤ n₀ + (↑a : ℤ)
ha : n₀ + (↑a : ℤ) - n₀ = (↑a : ℤ)
⊢ t.le n₀ ≤ t.le (n₀ + (↑a : ℤ))

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.le n ≤ t.le (n + (↑a : ℤ))
suffices : ∀ (a : ℕ), H a
⊢ Monotone t.le

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.le n ≤ t.le (n + (↑a : ℤ))
n : ℤ
simp : t.le n ≤ t.le n
⊢ t.le n ≤ t.le (n + (↑0 : ℤ))

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.le n ≤ t.le (n + (↑a : ℤ))
n : ℤ
⊢ t.le n ≤ t.le 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.le n ≤ t.le (n + (↑a : ℤ))
⊢ 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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
n : ℤ
X : C
hX : t.le n X
rw : t.le 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
⊢ t.le (n + (↑1 : ℤ)) X

Tactic:
rw [← t.shift_le n 1 (n + (1 : ℕ)) rfl, ObjectProperty.prop_shift_iff]

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff, CategoryTheory.Triangulated.TStructure.shift_le, Nat.cast, HAdd.hAdd, 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
n : ℤ
X : C
hX : t.le n X
⊢ t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)

Tactic:
rw [← t.shift_le n 0 n (add_zero n), ObjectProperty.prop_shift_iff] at hX

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff, CategoryTheory.Triangulated.TStructure.shift_le, 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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
n : ℤ
X : C
hX : t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
⊢ t.le 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)

Tactic:
t.le_zero_le _ hX

Premises used: CategoryTheory.Triangulated.TStructure.le_zero_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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
n : ℤ
X : C
hX : t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
⊢ t.le 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)

Tactic:
exact t.le_zero_le _ hX

Premises used: CategoryTheory.Triangulated.TStructure.le_zero_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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
⊢ H 1

Tactic:
have H_one : H 1 := fun n X hX => by
    rw [← t.shift_le n 1 (n + (1 : ℕ)) rfl, ObjectProperty.prop_shift_iff]
    rw [← t.shift_le n 0 n (add_zero n), ObjectProperty.prop_shift_iff] at hX
    exact t.le_zero_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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
rw : t.le n ≤ t.le (n + (↑a : ℤ) + (↑b : ℤ))
⊢ t.le n ≤ t.le (n + (↑c : ℤ))

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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.le n ≤ t.le (n + (↑a : ℤ) + (↑b : ℤ))

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

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.le n ≤ t.le (n + (↑a : ℤ))
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.le n ≤ t.le (n + (↑a : ℤ) + (↑b : ℤ))

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

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.le n ≤ t.le (n + (↑a : ℤ))
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 (ha n).trans (hb (n + a))
-- 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
⊢ 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.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
⊢ 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.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:
H_add a 1 _ rfl ha H_one

Premises used: OfNat.ofNat, rfl