apply primeSieve_rem_sum_le x y z hx hy
case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ (∑ d ∈ (primeInterSieve x y z ⋯).prodPrimes.divisors,
      if ↑d ≤ (primeInterSieve x y z ⋯).level then 3 ^ ω d * |(primeInterSieve x y z ⋯).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
no goals