Theorem: Smooth1Properties_below_aux (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ x < 2 ^ (-ε)
Tactic:
calc
  x ≤ 1 - Real.log 2 * ε := hx
  _ < 2 ^ (-ε) := ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - Real.log 2 * ε < 2 ^ (-ε)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - Real.log 2 * ε < 2 ^ (-ε)
Tactic:
rw [sub_lt_iff_lt_add, add_comm, ← sub_lt_iff_lt_add]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < Real.log 2 * ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < Real.log 2 * ε
Tactic:
exact (div_lt_iff εpos).mp <| Smooth1Properties_estimate εpos
State after:
no goals