apply Finset.sum_le_sum
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ i ∈ A, s.weights i * δ (P.gcd i) ≤ s.weights i * ∑ d ∈ (P.gcd i).divisors, μPlus.μPlus d