rw [siftedSum_as_delta]
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d