no goals
α : Type u_1
β : Type ?u.394516
γ : Type ?u.394519
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ filter (fun a => p a ∧ q a) s ↔ x✝ ∈ filter p s ∩ filter q s
simp [mem_filter, mem_inter, and_comm, and_left_comm, and_self_iff, and_assoc]