case a
α : Type u_1
β : Type ?u.455035
γ : Type ?u.455038
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ toFinset s.val ↔ a✝ ∈ s
α : Type u_1
β : Type ?u.455035
γ : Type ?u.455038
inst✝ : DecidableEq α
s : Finset α
⊢ toFinset s.val = s
ext
no goals
case a
α : Type u_1
β : Type ?u.455035
γ : Type ?u.455038
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ toFinset s.val ↔ a✝ ∈ s
rw [Multiset.mem_toFinset, ← mem_def]