no goals
α : Type u_1
β : Type ?u.269737
γ : Type ?u.269740
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
h : a ∈ s
⊢ s \ erase t a = insert a (s \ t)
rw [← sdiff_singleton_eq_erase, sdiff_sdiff_eq_sdiff_union (singleton_subset_iff.2 h), insert_eq,
  union_comm]