Theorem: LO.FirstOrder.Arith.Model.Nuon.four_mul_hash_self (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
⊢ (4 * a) # (4 * a) ≤ ((4 * a) # (2 * a)) ^ 2
Tactic:
simp [four_mul_eq_two_mul_two_mul, hash_two_mul_le_sq_hash]
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
⊢ ((4 * a) # (2 * a)) ^ 2 ≤ ((4 * a) # a) ^ 4
Tactic:
simp [pow_four_eq_sq_sq, hash_two_mul_le_sq_hash]
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
⊢ ((4 * a) # a) ^ 4 ≤ ((a # (2 * a)) ^ 2) ^ 4
Tactic:
rw [hash_comm (4 * a) a]
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a : M
⊢ (a # (4 * a)) ^ 4 ≤ ((a # (2 * a)) ^ 2) ^ 4

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
⊢ (a # (4 * a)) ^ 4 ≤ ((a # (2 * a)) ^ 2) ^ 4
Tactic:
simp [four_mul_eq_two_mul_two_mul, pow_four_eq_sq_sq, hash_two_mul_le_sq_hash]
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
⊢ ((a # (2 * a)) ^ 2) ^ 4 ≤ ((a # a) ^ 4) ^ 4
Tactic:
simp [pow_four_eq_sq_sq, hash_two_mul_le_sq_hash]
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
⊢ ((a # a) ^ 4) ^ 4 ≤ (a # a) ^ 16
Tactic:
simp [←pow_mul]
State after:
no goals