-- 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)
H_zero : H 0
H_one : H 1
⊢ ∀ (a b c : ℕ), a + b = c → H a → H b → H c

Tactic:
intro a b c h ha hb n

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

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)
⊢ 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 omega
  apply this

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)
⊢ ∀ (a : ℕ), H a

Proof state:
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)

Tactic:
exact H_add a 1 _ rfl ha H_one

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
⊢ Monotone t.le

Tactic:
intro n₀ n₁ h

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)
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ 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 0 ((shiftFunctor C n).obj X)
⊢ t.le 1 ((shiftFunctor C n).obj X)

Tactic:
exact t.le_zero_le _ hX

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

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

Tactic:
rfl

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

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

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

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₀ : ℤ
a : ℕ
h : n₀ ≤ n₀ + ↑a
ha : n₀ + ↑a - n₀ = ↑a
⊢ t.le n₀ ≤ t.le (n₀ + ↑a)

Tactic:
apply this

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)
H_zero : H 0
⊢ ∀ (a : ℕ), H a

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

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
⊢ ∀ (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
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:
intro 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