Theorem: LO.FirstOrder.Arith.Model.Nuon.bexp_four_mul (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 a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ bexp a (4 * x) = bexp a' x ^ 4
Tactic:
rw [four_mul_eq_two_mul_two_mul, bexp_two_mul (a' := a), bexp_two_mul (a := a), pow_four_eq_sq_sq]
State after:
case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖

case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ x < ‖a'‖

case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * (2 * x) < ‖a‖

case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖

State before:
case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖
Tactic:
exact lt_of_le_of_lt (by simp [four_mul_eq_two_mul_two_mul]) hx
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 a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x ≤ 4 * x
Tactic:
simp [four_mul_eq_two_mul_two_mul]
State after:
no goals

State before:
case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ x < ‖a'‖
Tactic:
exact hx'
State after:
no goals

State before:
case hx
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * (2 * x) < ‖a‖
Tactic:
simpa [four_mul_eq_two_mul_two_mul] using hx
State after:
no goals

State before:
case hx'
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
a a' x : M
hx : 4 * x < ‖a‖
hx' : x < ‖a'‖
⊢ 2 * x < ‖a‖
Tactic:
exact lt_of_le_of_lt (by simp [four_mul_eq_two_mul_two_mul]) hx
State after:
no goals