obtain ⟨εpos, ε1⟩ := hε
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hε : ε ∈ Ioo 0 1
hy : y ∈ Ioc 0 1
hx2 : 2 ^ ε < x
⊢ 2 < (x / y) ^ (1 / ε)
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hy : y ∈ Ioc 0 1
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
⊢ 2 < (x / y) ^ (1 / ε)