case a
α : Type u_1
β : Type ?u.480823
γ : Type ?u.480826
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ List.toFinset (toList s) ↔ a✝ ∈ s
α : Type u_1
β : Type ?u.480823
γ : Type ?u.480826
inst✝ : DecidableEq α
s : Finset α
⊢ List.toFinset (toList s) = s
ext
no goals
case a
α : Type u_1
β : Type ?u.480823
γ : Type ?u.480826
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ List.toFinset (toList s) ↔ a✝ ∈ s
simp