Theorem: pi_alt (PrimeNumberTheoremAnd/Consequences.lean)

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