rw [sum_comm, sum_congr rfl]
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ (∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0) =
    ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ P.divisors, (∑ x_1 ∈ A, if x ∣ x_1 then s.weights x_1 * μPlus.μPlus x else 0) = μPlus.μPlus x * s.multSum x