dsimp only [errSum]
s : SelbergSieve
⊢ s.errSum μ⁺ ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
s : SelbergSieve
⊢ ∑ d ∈ P.divisors, |s.selbergMuPlus d| * |s.rem d| ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0