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