rw [← rpow_mul]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y = ((x / y) ^ (1 / ε)) ^ ε
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y = (x / y) ^ (1 / ε * ε)

case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
y1 : y ≤ 1
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 ≤ x / y