no goals
α : Type u_1
β : Type ?u.268404
γ : Type ?u.268407
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
x : α
⊢ s \ insert x t = erase (s \ t) x
simp_rw [← sdiff_singleton_eq_erase, insert_eq, sdiff_sdiff_left', sdiff_union_distrib,
  inter_comm]