case h
α : Type u_1
β : Type ?u.29702
γ : Type ?u.29705
s : Finset α
a✝ b a x✝ : α
⊢ x✝ ∈ ↑{a} ↔ x✝ ∈ {a}
α : Type u_1
β : Type ?u.29702
γ : Type ?u.29705
s : Finset α
a✝ b a : α
⊢ ↑{a} = {a}
ext
no goals
case h
α : Type u_1
β : Type ?u.29702
γ : Type ?u.29705
s : Finset α
a✝ b a x✝ : α
⊢ x✝ ∈ ↑{a} ↔ x✝ ∈ {a}
simp