intro 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
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 * s.multSum d