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