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