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