no goals
α : Type u_1
β : Type ?u.105476
γ : Type ?u.105479
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
x : α
⊢ x ∈ ↑(insert a s) ↔ x ∈ insert a ↑s
simp only [mem_coe, mem_insert, Set.mem_insert_iff]