prime_between

@[blueprint  (title := "prime-between")  (statement := /-- For every $\eps>0$, there is a prime between $x$ and $(1+\eps)x$ for  all sufficiently large $x$. -/)  (proof := /-- Use Corollary \ref{pi_alt} to show that $\pi((1+\eps)x) - \pi(x)$ goes to infinity  as $x \to \infty$. -/)  (latexEnv := "corollary")]theorem prime_between {ε : ℝ} (hε : 0 < ε) :    ∀ᶠ x : ℝ in atTop, ∃ p : ℕ, Nat.Prime p ∧ x < p ∧ p < (1 + ε) * x := by  have squeeze := tendsto_by_squeeze (ε/2) (by linarith)  rw [Filter.tendsto_iff_forall_eventually_mem] at squeeze  specialize squeeze (Set.Ici 1) (by exact Ici_mem_atTop 1)  simp only [Set.mem_Ici, eventually_atTop] at squeeze  obtain ⟨a, ha⟩ := squeeze  rw [eventually_atTop]  use (max a 1)  intro b hb  rw [sup_le_iff] at hb  specialize ha b hb.1   have val_lt : (⌊b⌋₊.primeCounting : ℝ) < ⌊(1 + ε/2) * b⌋₊.primeCounting := by linarith  norm_cast at val_lt   have jump := prime_in_gap b ((1 + ε/2) * b) (by linarith) val_lt  obtain ⟨p, hp, b_lt_p, p_le⟩ := jump  have p_lt: p < (1 + ε) * b := by    linarith  use p