rw [mul_eq_zero_of_right _]
case pos
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
⊢ ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) = 0
case pos
s : SelbergSieve
d : ℕ
hd : ¬↑d ^ 2 ≤ y
h : d ∣ P
⊢ (∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) = 0