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