apply Finset.card_le_card
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.filter Nat.Prime (Finset.range N)).card ≤ (Finset.filter Nat.Prime (Finset.range (N + 1))).card
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter Nat.Prime (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range (N + 1))