apply hP p hpp hple
case hP
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
hple : ↑p ≤ s.level
⊢ p ∣ s.prodPrimes
no goals