α : Type u_1
β : Type ?u.55899
γ : Type ?u.55902
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x
α : Type u_1
β : Type ?u.55899
γ : Type ?u.55902
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ card { x // p x } = Finset.card (filter p univ)
refine' Fintype.card_of_subtype _ _
no goals
α : Type u_1
β : Type ?u.55899
γ : Type ?u.55902
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x
simp