calc _ ≤ y / (Real.log z / 2) + 5 * z * (1+Real.log z)^3 := ?_
     _ = _ := by ring
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ 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) ≤
    2 * y / z.log + 5 * z * (1 + z.log) ^ 3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ ((primeInterSieve x y z ⋯).totalMass / (primeInterSieve x y z ⋯).selbergBoundingSum +
      ∑ 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) ≤
    y / (z.log / 2) + 5 * z * (1 + z.log) ^ 3