have : 1 - 1 / (2 : ℝ) ^ ε = ((2 : ℝ) ^ ε - 1) / (2 : ℝ) ^ ε := by
  rw [sub_div, div_self (by positivity)]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
this : 1 - 1 / 2 ^ ε = (2 ^ ε - 1) / 2 ^ ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2