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