dsimp only [mainSum, errSum]
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|