trans (∑ n in s.support, ∑ d in divisors P, if d ∣ n then a n * μPlus d else 0)
case a
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d = ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0

s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ (∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0) =
    ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d