no goals
α : Type u_1
β : Type ?u.378630
γ : Type ?u.378633
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ filter p t = filter p (s ∩ t)
rw [inter_comm, filter_inter, inter_comm]