α : Type u_1
β : Type ?u.203129
γ : Type ?u.203132
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ _root_.Disjoint s t ∨ ¬_root_.Disjoint s t
α : Type u_1
β : Type ?u.203129
γ : Type ?u.203132
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ _root_.Disjoint s t ∨ Finset.Nonempty (s ∩ t)
rw [← not_disjoint_iff_nonempty_inter]
no goals
α : Type u_1
β : Type ?u.203129
γ : Type ?u.203132
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ _root_.Disjoint s t ∨ ¬_root_.Disjoint s t
exact em _