trans ((ν d)⁻¹ * (ν d) * g d * μ d / S * g m)
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * g (d * m) = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)
s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ S⁻¹ * ↑(μ d) * g (d * m) = (ν d)⁻¹ * ν d * g d * ↑(μ d) / S * g m

s : SelbergSieve
d : ℕ
h_dvd : d ∣ P
m : ℕ
hm : m ∈ P.divisors
h : (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ (ν d)⁻¹ * ν d * g d * ↑(μ d) / S * g m = ν d * ((ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * g m)