Theorem: LO.FirstOrder.Arith.Model.Nuon.NuonAux.succ (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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
H : NuonAux A k n
hk : k ≤ ‖A‖
⊢ NuonAux A (k + 1) (n + fbit A k)
Tactic:
rcases zero_le A with (rfl | pos)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n k : M
H : NuonAux 0 k n
hk : k ≤ ‖0‖
⊢ NuonAux 0 (k + 1) (n + fbit 0 k)

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
H : NuonAux A k n
hk : k ≤ ‖A‖
pos : 0 < A
⊢ NuonAux A (k + 1) (n + fbit A k)

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
H : NuonAux A k n
hk : k ≤ ‖A‖
pos : 0 < A
⊢ NuonAux A (k + 1) (n + fbit A k)
Tactic:
exact SeriesSegment.succ (sq_polyI_hash_polyL_polybounded pos) (by simp [polyL]) (lt_of_le_of_lt hk $ polyI_le pos) H
State after:
no goals

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n k : M
H : NuonAux 0 k n
hk : k ≤ ‖0‖
⊢ NuonAux 0 (k + 1) (n + fbit 0 k)
Tactic:
rcases show n = 0 from H.uniq (NuonAux.zero k)
State after:
case inl.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
k : M
hk : k ≤ ‖0‖
H : NuonAux 0 k 0
⊢ NuonAux 0 (k + 1) (0 + fbit 0 k)

State before:
case inl.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
k : M
hk : k ≤ ‖0‖
H : NuonAux 0 k 0
⊢ NuonAux 0 (k + 1) (0 + fbit 0 k)
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
H : NuonAux A k n
hk : k ≤ ‖A‖
pos : 0 < A
⊢ ‖‖polyI A‖ ^ 2‖ ≤ ‖polyL A‖
Tactic:
simp [polyL]
State after:
no goals