the prime number theorem in Chebyshev form, stated with the fully qualified Mathlib function. The proof reuses the PrimeNumberTheoremAnd development preserved in LeanPool.MooreBound instead of duplicating its analytic closure.

theorem Zeta32.ArithSum.PNT.theta_isEquivalent_id : Asymptotics.IsEquivalent Filter.atTop Chebyshev.theta id