awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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
⊢ ∃ (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)
have 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₃)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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'
⊢ (t.le n).shift a = t.le n'
have h : ∀ (X : C), (t.le n).shift a X ↔ t.le n' X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ (t.le n).shift a X ↔ t.le n' X
have h : (t.le n).shift a X → t.le n' X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ (t.le n).shift a X ↔ t.le n' X
have h₁ : t.le n' X → (t.le n).shift a X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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'
⊢ (t.ge n).shift a = t.ge n'
have h : ∀ (X : C), (t.ge n).shift a X ↔ t.ge n' X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ (t.ge n).shift a X ↔ t.ge n' X
have h : (t.ge n).shift a X → t.ge n' X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ (t.ge n).shift a X ↔ t.ge n' X
have h₁ : t.ge n' X → (t.ge n).shift a X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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₁
⊢ t.le n₀ ≤ t.le n₁
have obtain : ∀ (a : ℕ) (ha : n₁ - n₀ = (↑a : ℤ)), t.le n₀ ≤ t.le n₁
Tactic: obtain ⟨a, ha⟩ := Int.nonneg_def.1 h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 : ℤ)
⊢ t.le n₀ ≤ t.le n₁
have obtain : ∀ (h : n₀ ≤ n₀ + (↑a : ℤ)) (ha : n₀ + (↑a : ℤ) - n₀ = (↑a : ℤ)), t.le n₀ ≤ t.le (n₀ + (↑a : ℤ))
Tactic: obtain rfl : n₁ = n₀ + a := by lia
Cleared hypotheses: n₁, h, ha
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 : ℤ))
⊢ Monotone t.le
have suffices : ∀ (a : ℕ), H a
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 + (↑0 : ℤ))
have simp : t.le n ≤ t.le n
Tactic: simp only [Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 : ℤ))
⊢ ∀ (a : ℕ), H a
have H_zero : H 0
Tactic: have H_zero : H 0 := fun n => by
    simp only [Nat.cast_zero, add_zero]
    rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 (n + (↑1 : ℤ)) X
have rw : t.le 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
Tactic: rw [← t.shift_le n 1 (n + (1 : ℕ)) rfl, ObjectProperty.prop_shift_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)
have hX₁ : 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
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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
⊢ ∀ (a : ℕ), H a
have H_one : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 + (↑c : ℤ))
have rw : t.le n ≤ t.le (n + (↑a : ℤ) + (↑b : ℤ))
Tactic: rw [← h, Nat.cast_add, ← add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 : ℕ), H a
have H_add : ∀ (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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ H a
have succ : ∀ (a : ℕ) (ha : H a), H (a + 1)
Tactic: induction a with
  | zero => exact H_zero
  | succ a ha => exact H_add a 1 _ rfl ha H_one
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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₁
⊢ t.ge n₁ ≤ t.ge n₀
have obtain : ∀ (a : ℕ) (ha : n₁ - n₀ = (↑a : ℤ)), t.ge n₁ ≤ t.ge n₀
Tactic: obtain ⟨a, ha⟩ := Int.nonneg_def.1 h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 : ℤ)
⊢ t.ge n₁ ≤ t.ge n₀
have obtain : ∀ (h : n₀ ≤ n₀ + (↑a : ℤ)) (ha : n₀ + (↑a : ℤ) - n₀ = (↑a : ℤ)), t.ge (n₀ + (↑a : ℤ)) ≤ t.ge n₀
Tactic: obtain rfl : n₁ = n₀ + a := by lia
Cleared hypotheses: n₁, h, ha
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ Antitone t.ge
have suffices : ∀ (a : ℕ), H a
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 + (↑0 : ℤ)) ≤ t.ge n
have simp : t.ge n ≤ t.ge n
Tactic: simp only [Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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
⊢ ∀ (a : ℕ), H a
have H_zero : H 0
Tactic: have H_zero : H 0 := fun n => by
    simp only [Nat.cast_zero, add_zero]
    rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 n X
have hX₁ : 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
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 n X
have rw : (t.ge 0).shift n X
Tactic: rw [← t.shift_ge n 0 n (add_zero n)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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
⊢ ∀ (a : ℕ), H a
have H_one : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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 + (↑c : ℤ)) ≤ t.ge n
have rw : t.ge (n + (↑a : ℤ) + (↑b : ℤ)) ≤ t.ge n
Tactic: rw [← h, Nat.cast_add, ← add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 : ℕ), H a
have H_add : ∀ (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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ H a
have succ : ∀ (a : ℕ) (ha : H a), H (a + 1)
Tactic: induction a with
  | zero => exact H_zero
  | succ a ha => exact H_add a 1 _ rfl ha H_one
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ t.le n Y
have simp : ∀ (h : t.IsLE X n), t.IsLE Y n
Tactic: simp only [le_iff_isLE] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ t.ge n Y
have simp : ∀ (h : t.IsGE X n), t.IsGE Y n
Tactic: simp only [ge_iff_isGE] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 X n
have 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
Tactic: have h := t.isLE_shift (X⟦a⟧) n' (-a) n
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
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 X n
have 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
Tactic: have h := t.isGE_shift (X⟦a⟧) n' (-a) n
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' ↔ t.IsLE X n
have mp : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' → t.IsLE X n
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' ↔ t.IsLE X n
have mpr : t.IsLE X n → t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
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
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' ↔ t.IsGE X n
have mp : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' → t.IsGE X n
Tactic: constructor