rw [←ite_zero_mul, mul_comm]
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝¹ : d ∈ P.divisors
n : ℕ
a✝ : n ∈ A
⊢ (if d ∣ n then s.weights n * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ n then s.weights n else 0
no goals