intro d _
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ x ∈ P.divisors, μPlus.μPlus x * s.multSum x = X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x
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