trans (∑ d in  Finset.filter (fun d:ℕ => ↑d ≤ s.level) (s.toSieve.prodPrimes.divisors),  3 ^ ω d * C )
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    C * s.level * (1 + s.level.log) ^ 3
s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ a ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω a * |s.rem a| ≤
    ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C

s : SelbergSieve
C : ℝ
hrem : ∀ d > 0, |s.rem d| ≤ C
⊢ ∑ d ∈ Finset.filter (fun d => ↑d ≤ s.level) s.prodPrimes.divisors, 3 ^ ω d * C ≤ C * s.level * (1 + s.level.log) ^ 3