rw [inv_mul_cancel (s.nu_ne_zero h_dvd), s.selbergTerms_mult.map_mul_of_coprime
  $ coprime_comm.mp h.2]
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 * g m) = 1 * g d * ↑(μ d) / S * g m