case a
α : Type u_1
β : Type ?u.98777
γ : Type ?u.98780
s✝ t : Set α
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ filter (fun x => x ∈ s) Finset.univ ↔ a✝ ∈ toFinset s
α : Type u_1
β : Type ?u.98777
γ : Type ?u.98780
s✝ t : Set α
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ filter (fun x => x ∈ s) Finset.univ = toFinset s
ext
no goals
case a
α : Type u_1
β : Type ?u.98777
γ : Type ?u.98780
s✝ t : Set α
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x => x ∈ s
a✝ : α
⊢ a✝ ∈ filter (fun x => x ∈ s) Finset.univ ↔ a✝ ∈ toFinset s
simp only [Finset.mem_univ, decide_eq_true_eq, forall_true_left, mem_filter,
  true_and, mem_toFinset]