rw [four_mul_eq_two_mul_two_mul, bexp_two_mul (a' := a), bexp_two_mul (a := a), pow_four_eq_sq_sq]
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
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‖