intro p hpp _
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
⊢ ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
case hnu_lt
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ s.nu p < 1