Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_polyL_polybounded (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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ polyI A ≤ polyI A
Tactic:
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ polyL A ≤ 3 * polyI A
Tactic:
simp [polyL, sq_len_le_three_mul]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ 0 < 4
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ 3 ≤ 4
Tactic:
simp [←three_add_one_eq_four]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (4 * polyI A) # (4 * polyI A) ≤ (polyI A # polyI A) ^ (4 * 4)
Tactic:
simpa using four_mul_hash_self _
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (polyI A # polyI A) ^ (4 * 4) ≤ ((2 * A + 1) ^ 4) ^ (4 * 4)
Tactic:
simp only [pow_mul, pow_four_le_pow_four, polyI_hash_self_polybounded pos]
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ ((2 * A + 1) ^ 4) ^ (4 * 4) = (2 * A + 1) ^ 64
Tactic:
simp [←pow_mul]
State after:
no goals