linarith [siftedSum_le _ _ _ hx hy hz, primesBetween_le_siftedSum_add x y z hz.le]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
this : z ≤ z * (1 + z.log) ^ 3
⊢ ↑(primesBetween x (x + y)) ≤ 2 * y / z.log + 6 * z * (1 + z.log) ^ 3
no goals