no goals
α : Type u_1
β : Type ?u.261503
γ : Type ?u.261506
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ erase s a ∩ t = erase (s ∩ t) a
simpa only [inter_comm t] using inter_erase a t s