no goals
α : Type u_1
β : Type ?u.269252
γ : Type ?u.269255
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
x : α
hxs : x ∈ s
hxt : ¬x ∈ t
⊢ insert x (s \ insert x t) = s \ t
rw [sdiff_insert, insert_erase (mem_sdiff.mpr ⟨hxs, hxt⟩)]