simp only [one_div, ArithmeticFunction.pdiv_apply, ArithmeticFunction.natCoe_apply,
  ArithmeticFunction.zeta_apply_ne (show m ≠ 0 by omega), Nat.cast_ite, CharP.cast_eq_zero, Nat.cast_one,
  ArithmeticFunction.id_apply]
case a
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
m : ℕ
hm : 1 ≤ m ∧ m ≤ ⌊√s.level⌋₊
⊢ 1 / ↑m = ((↑ζ).pdiv ↑ArithmeticFunction.id) m
no goals