p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ card (filter p (range n)) ≤ card (Set.Finite.toFinset hp)
p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ count p n ≤ card (Set.Finite.toFinset hp)
rw [count_eq_card_filter_range]
no goals
p : ℕ → Prop
inst✝ : DecidablePred p
hp : Set.Finite (setOf p)
n : ℕ
⊢ card (filter p (range n)) ≤ card (Set.Finite.toFinset hp)
exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2