no goals
α : Type u_1
β : Type ?u.368807
γ : Type ?u.368810
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ filter p (s₁ ∪ s₂) ↔ x✝ ∈ filter p s₁ ∪ filter p s₂
simp only [mem_filter, mem_union, or_and_right]