rw [div_rpow, ← rpow_mul, mul_div_cancel₀ 1 <| ne_of_gt εpos, rpow_one] <;> positivity
case intro.intro.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
⊢ (2 ^ ε / y) ^ (1 / ε) = 2 / y ^ (1 / ε)
no goals