rw [if_pos hdP, mul_assoc]
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤
    (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) *
      ↑(μ d)
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ((∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) * ↑(μ d))