no goals
α : Type u_1
β : Type ?u.369340
γ : Type ?u.369343
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ filter p s ∪ filter q s ↔ x ∈ filter (fun x => p x ∨ q x) s
simp [mem_filter, mem_union, ←and_or_left]