simp only [ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
  ArithmeticFunction.zeta_apply, Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
  ArithmeticFunction.id_apply]
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
⊢ ((↑ζ).pdiv ↑ArithmeticFunction.id) 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
⊢ (if p = 0 then 0 else 1) / ↑p < 1