Theorem: prime_between (PrimeNumberTheoremAnd/Consequences.lean)

State before:
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ p, p.Prime ∧ x < ↑p ∧ ↑p < (1 + ε) * x
Tactic:
sorry
State after:
no goals