rw[sum_comm]
case a
s : Sieve
w : ℕ → ℝ
d1 : ℕ
a✝ : d1 ∈ P.divisors
⊢ (∑ x ∈ P.divisors, ∑ d2 ∈ P.divisors, if x ∣ d1.gcd d2 then 1 / g x * (ν d1 * w d1) * (ν d2 * w d2) else 0) =
    ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ d1.gcd d2 then 1 / g l * (ν d1 * w d1) * (ν d2 * w d2) else 0
no goals