Theorem: pn_asymptotic (PrimeNumberTheoremAnd/Consequences.lean)

State before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (n : ℕ), ↑(nth Nat.Prime n) = (1 + c n) * ↑n * (↑n).log
Tactic:
sorry
State after:
no goals