conv => enter [1, 2, k]; rw [← ite_zero_mul]
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors, if k ∣ d then g k * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0 else 0) =
    s.selbergWeights d * ↑(μ d) * S
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (∑ k ∈ P.divisors,
      (if k ∣ d then g k else 0) * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) =
    s.selbergWeights d * ↑(μ d) * S