-- Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
lemma le_monotone : Monotone t.le

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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₁

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

Result:
case intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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₁

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
⊢ ∀ (a : ℕ), H a

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))

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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 : ℕ), H a

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
⊢ Monotone t.le

Tactic:
let H := fun (a : ℕ) => ∀ (n : ℤ), t.le n ≤ t.le (n + a)

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
⊢ Monotone t.le

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
⊢ ∀ (a : ℕ), H a

Tactic:
have H_zero : H 0 := fun n => by
  simp only [Nat.cast_zero, add_zero]
  rfl

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
⊢ ∀ (a : ℕ), H a

Proof state:
case zero
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
n : ℤ
⊢ t.le n ≤ t.le (n + ↑0)

Tactic:
simp only [Nat.cast_zero, add_zero]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
n : ℤ
⊢ t.le n ≤ t.le n

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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 ((shiftFunctor C n).obj X)

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

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a => ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
n : ℤ
X : C
hX : t.le 0 ((shiftFunctor C n).obj X)
⊢ t.le 1 ((shiftFunctor C n).obj X)

Proof state:
case intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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₁

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

Result:
case intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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 : ℕ
⊢ H a

Tactic:
induction' a with a ha

Result:
case zero
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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

case succ
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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

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

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → 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 ((shiftFunctor C n).obj X)