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