Theorem: LO.FirstOrder.Arith.Model.Nuon.IsSeries.le_add (Arithmetization/OmegaOne/Nuon.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ ∀ l ≤ iter, T{L}[l] ≤ T{L}[0] + ‖I‖ * l
Tactic:
intro l
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
⊢ l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
⊢ l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
Tactic:
induction l using induction_iSigmaZero
State after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 𝚺₀-Predicate fun l => l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 0 ≤ iter → T{L}[0] ≤ T{L}[0] + ‖I‖ * 0

case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
x✝ : M
a✝ : x✝ ≤ iter → T{L}[x✝] ≤ T{L}[0] + ‖I‖ * x✝
⊢ x✝ + 1 ≤ iter → T{L}[x✝ + 1] ≤ T{L}[0] + ‖I‖ * (x✝ + 1)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 0 ≤ iter → T{L}[0] ≤ T{L}[0] + ‖I‖ * 0
Tactic:
case zero => simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ l + 1 ≤ iter → T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
case succ l IH =>
  intro h
  have IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l := IH (le_trans (by simp) h)
  calc
    T{L}[l + 1] ≤ T{L}[l] + ‖I‖           := (H l (succ_le_iff_lt.mp h)).le_add
    _           ≤ T{L}[0] + ‖I‖ * (l + 1) := by simpa [mul_add, ←add_assoc] using IH
State after:
no goals

State before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 𝚺₀-Predicate fun l => l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
Tactic:
definability
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
⊢ 0 ≤ iter → T{L}[0] ≤ T{L}[0] + ‖I‖ * 0
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ l + 1 ≤ iter → T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
intro h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
have IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l := IH (le_trans (by simp) h)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH✝ : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH✝ : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ T{L}[l + 1] ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
calc
  T{L}[l + 1] ≤ T{L}[l] + ‖I‖           := (H l (succ_le_iff_lt.mp h)).le_add
  _           ≤ T{L}[0] + ‖I‖ * (l + 1) := by simpa [mul_add, ←add_assoc] using IH
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
⊢ l ≤ l + 1
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A iter T : M
H : IsSeries U I L A iter T
l : M
IH✝ : l ≤ iter → T{L}[l] ≤ T{L}[0] + ‖I‖ * l
h : l + 1 ≤ iter
IH : T{L}[l] ≤ T{L}[0] + ‖I‖ * l
⊢ T{L}[l] + ‖I‖ ≤ T{L}[0] + ‖I‖ * (l + 1)
Tactic:
simpa [mul_add, ←add_assoc] using IH
State after:
no goals