no goals
α : Type u_1
β : Type ?u.333912
γ : Type ?u.333915
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (filter p s) (filter q s) ↔ ∀ (x : α), x ∈ s → p x → ¬q x
constructor <;> simp (config := { contextual := true }) [disjoint_left]