case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Finset α
a✝ : α
⊢ a✝ ∈ Finite.toFinset (_ : Set.Finite ↑s) ↔ a✝ ∈ s
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Finset α
⊢ Finite.toFinset (_ : Set.Finite ↑s) = s
ext
no goals
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Finset α
a✝ : α
⊢ a✝ ∈ Finite.toFinset (_ : Set.Finite ↑s) ↔ a✝ ∈ s
rw [Set.Finite.mem_toFinset, mem_coe]