exact mul_le_mul_of_nonneg_left (hμ (Nat.gcd P n)) (s.weights_nonneg n)
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * δ (P.gcd n) ≤ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
no goals