no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
⊢ insert a (s \ {a}) = insert a s
simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]