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

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