have : (2 : ℝ) ^ ε < 2 := by
  nth_rewrite 1 [← pow_one 2]
  convert rpow_lt_rpow_of_exponent_lt (x := 2) (by norm_num) hε.2 <;> norm_num
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε