no goals
α : Type u_1
β : Type ?u.400335
γ : Type ?u.400338
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅
simp [Subset.antisymm_iff, disjoint_iff_inter_eq_empty]