apply sum_congr rfl
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) =
    ∑ d ∈ P.divisors, ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ ∀ x ∈ P.divisors,
    (if l ∣ x then ν x * s.selbergWeights x else 0) =
      ∑ k ∈ P.divisors, if l ∣ x ∧ x ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ x) else 0