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

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