no goals
α : Type u_1
β : Type ?u.266278
γ : Type ?u.266281
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk Setoid.r l)) = filter (fun a => p a ∧ q a) (Quot.mk Setoid.r l)
simp