α : Type u_1
β : Type ?u.6239
γ : Type ?u.6242
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α
α : Type u_1
β : Type ?u.6239
γ : Type ?u.6242
inst✝ : Finite α
p : α → Prop
⊢ Nat.card { x // p x } ≤ Nat.card α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.6239
γ : Type ?u.6242
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_subtype_le p