no goals
α : Type u_1
β : Type ?u.261878
γ : Type ?u.261881
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ erase s a \ t = erase (s \ t) a
simp_rw [erase_eq, sdiff_right_comm]