dsimp only [rem]
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * s.rem d
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * (s.multSum d - ν d * X)