have : y ^ (1 / ε) ≤ y := by
  nth_rewrite 2 [← rpow_one y]
  exact rpow_le_rpow_of_exponent_ge ypos y1 (by linarith [one_lt_one_div εpos ε1])
case intro.intro.calc_3
𝕂 : 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
case intro.intro.calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x y ε : ℝ
hx2 : 2 ^ ε < x
εpos : 0 < ε
ε1 : ε < 1
ypos : 0 < y
y1 : y ≤ 1
this : y ^ (1 / ε) ≤ y
⊢ 2 / y ^ (1 / ε) ≥ 2 / y