no goals
α : Type u_1
β : Type ?u.213387
γ : Type ?u.213390
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
x✝ : α
⊢ x✝ ≠ a ∧ x✝ ∈ s ↔ x✝ ∈ ↑s \ {a}
rw [and_comm, Set.mem_diff, Set.mem_singleton_iff, mem_coe]