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