Theorem: pi_asymp (PrimeNumberTheoremAnd/Consequences.lean)

State before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (x : ℝ), ↑(π ⌊x⌋₊) = (1 + c x) * ∫ (t : ℝ) in Set.Icc 2 x, 1 / t.log
Tactic:
sorry
State after:
no goals