pn_asymptotic

@[blueprint  (title := "pn-asymptotic")  (statement := /--   One has    $$ p_n = (1+o(1)) n \log n$$  as $n \to \infty$.  -/)  (proof := /--    Use Corollary \ref{pi_alt} to show that $n=\pi(p_n)\sim p_n/\log p_n$    Taking logs gives $\log n \sim \log p_n - \log\log p_n \sim \log p_n$.    Multiplying these gives $p_n\sim n\log n$ from which the result follows.  -/)  (latexEnv := "proposition")]theorem pn_asymptotic : ∃ c : ℕ → ℝ, c =o[atTop] (fun _ ↦ (1 : ℝ)) ∧    ∀ n : ℕ, n > 1 → nth_prime n = (1 + c n) * n * log n := by  let c : ℕ → ℝ := fun n ↦ (nth_prime n) / (n * log n) - 1  refine ⟨c, ?_, ?_⟩  swap  · intro n hn    have : log n ≠ 0 := by rw [Real.log_ne_zero]; rify at hn; grind    simp [c]    field_simp  apply isLittleO_of_tendsto  · simp  simp only [div_one]  unfold c  have := isEquivalent_iff_tendsto_one ?_|>.mp nth_prime_asymp  swap  · filter_upwards [eventually_ge_atTop 2] with n hn    simp    norm_cast    grind  convert! this.add_const (-1 : ℝ) using 2  norm_num