rw [sum_comm]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ d ∈ P.divisors, ∑ k ∈ P.divisors, if l ∣ d ∧ d ∣ k ∧ ↑k ^ 2 ≤ y then g k * S⁻¹ * ↑(μ d) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (∑ y ∈ P.divisors, ∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ y ∧ ↑y ^ 2 ≤ y then g y * S⁻¹ * ↑(μ x) else 0) =
    ∑ k ∈ P.divisors, if ↑k ^ 2 ≤ y then (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ k then ↑(μ d) else 0) * g k * S⁻¹ else 0