no goals
α : Type u_1
β : Type ?u.265412
γ : Type ?u.265415
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
ha : a ∈ t
s : Finset α
⊢ erase s a ∪ t = s ∪ t
rw [← insert_erase (mem_union_right s ha), erase_union_distrib, ← union_insert, insert_erase ha]