trans ↑((Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter (fun d => ∀ p:ℕ, p.Prime → p ≤ z → ¬p ∣ d)
    ∪ (Finset.Icc 1 (Nat.floor z))).card
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(primesBetween x (x + y)) ≤ (primeInterSieve x y z hz).siftedSum + z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(primesBetween x (x + y)) ≤
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊) ∪ Finset.Icc 1 ⌊z⌋₊).card ≤
    (primeInterSieve x y z hz).siftedSum + z