no goals
α : Type u_1
β : Type ?u.264321
γ : Type ?u.264324
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, sdiff_sdiff, sup_sdiff_eq_sup le_rfl, sup_comm]