Theorem: MediumPNT (PrimeNumberTheoremAnd/MediumPNT.lean)

State before:
⊢ ∃ c, ∃ (_ : c > 0), (ChebyshevPsi - id) =O[atTop] fun x => x * rexp (-c * x.log ^ (1 / 18))
Tactic:
sorry
State after:
no goals