no goals
α : Type u_1
β : Type ?u.45481
γ : Type ?u.45484
f : α → β
s t u : Finset α
a b : α
⊢ _root_.Disjoint s t ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
simp only [disjoint_left, imp_not_comm, forall_eq']