calc
  2 * Real.log 2 > 2 * (1 - 2 ^ (-ε)) / ε := ?_
  _ > 2 ^ ε * (1 - 2 ^ (-ε)) / ε := ?_
  _ = (2 ^ ε - 1) / ε := ?_
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ (2 ^ ε - 1) / ε < 2 * Real.log 2
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 * Real.log 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
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε

case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
⊢ 2 ^ ε * (1 - 2 ^ (-ε)) / ε = (2 ^ ε - 1) / ε