Theorem: LO.FirstOrder.Arith.Model.Nuon.Series.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 n : M
H : Series U I L A iter n
⊢ n ≤ ‖I‖ * iter
Tactic:
rcases H with ⟨T, _, hT, hzero, rfl⟩
State after:
case intro.intro.intro.intro
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
left✝ : T < U
hT : IsSeries U I L A iter T
hzero : T{L}[0] = 0
⊢ T{L}[iter] ≤ ‖I‖ * iter

State before:
case intro.intro.intro.intro
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
left✝ : T < U
hT : IsSeries U I L A iter T
hzero : T{L}[0] = 0
⊢ T{L}[iter] ≤ ‖I‖ * iter
Tactic:
simpa [hzero] using hT.le_add iter (by rfl)
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
left✝ : T < U
hT : IsSeries U I L A iter T
hzero : T{L}[0] = 0
⊢ iter ≤ iter
Tactic:
rfl
State after:
no goals