apply sum_congr rfl
s : Sieve
w : ℕ → ℝ
⊢ ∑ d1 ∈ P.divisors, ∑ d2 ∈ P.divisors, ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹ =
    ∑ 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
s : Sieve
w : ℕ → ℝ
⊢ ∀ x ∈ P.divisors,
    ∑ d2 ∈ P.divisors, ν x * w x * ν d2 * w d2 * (ν (x.gcd d2))⁻¹ =
      ∑ d2 ∈ P.divisors, ∑ l ∈ P.divisors, if l ∣ x.gcd d2 then 1 / g l * (ν x * w x) * (ν d2 * w d2) else 0