have := (mul_lt_mul_right pos).mpr this
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : 1 + 2 * Real.log 2 * ε ≤ x
hε : ε ∈ Ioo 0 1
this : 2 ^ ε < 2
pos : 0 < (1 - 2 ^ (-ε)) / ε
⊢ 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
pos : 0 < (1 - 2 ^ (-ε)) / ε
this : 2 ^ ε * ((1 - 2 ^ (-ε)) / ε) < 2 * ((1 - 2 ^ (-ε)) / ε)
⊢ 2 * (1 - 2 ^ (-ε)) / ε > 2 ^ ε * (1 - 2 ^ (-ε)) / ε