no goals
α : Type u_1
β : Type ?u.263332
γ : Type ?u.263335
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ erase (s ∪ t) a = erase s a ∪ erase t a
simp_rw [erase_eq, union_sdiff_distrib]