case h
α : Type u_1
β : Type ?u.108687
γ : Type ?u.108690
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b✝ a b x✝ : α
⊢ x✝ ∈ ↑{a, b} ↔ x✝ ∈ {a, b}
α : Type u_1
β : Type ?u.108687
γ : Type ?u.108690
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b✝ a b : α
⊢ ↑{a, b} = {a, b}
ext
no goals
case h
α : Type u_1
β : Type ?u.108687
γ : Type ?u.108690
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b✝ a b x✝ : α
⊢ x✝ ∈ ↑{a, b} ↔ x✝ ∈ {a, b}
simp