no goals
α : Type u_1
β : Type ?u.391377
γ : Type ?u.391380
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_union, and_or_left]