no goals
α : Type u_1
β : Type ?u.160671
γ : Type ?u.160674
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
⊢ _root_.Disjoint s (t ∪ u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
simp only [disjoint_right, mem_union, or_imp, forall_and]