case a
α : Type u_1
β : Type ?u.93002
γ : Type ?u.93005
s t : Set α
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
a✝ : α
⊢ a✝ ∈ toFinset {x | p x} ↔ a✝ ∈ filter p Finset.univ
α : Type u_1
β : Type ?u.93002
γ : Type ?u.93005
s t : Set α
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
⊢ toFinset {x | p x} = filter p Finset.univ
ext
no goals
case a
α : Type u_1
β : Type ?u.93002
γ : Type ?u.93005
s t : Set α
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
a✝ : α
⊢ a✝ ∈ toFinset {x | p x} ↔ a✝ ∈ filter p Finset.univ
simp