Theorem: mu_pnt_alt (PrimeNumberTheoremAnd/Consequences.lean)

State before:
⊢ (fun x => ∑ n ∈ range ⌊x⌋₊, ↑(μ n) / ↑n) =o[atTop] fun x => 1
Tactic:
sorry
State after:
no goals