no goals
α : Type u_1
β : Type ?u.121015
γ : Type ?u.121018
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ _root_.Disjoint (insert a s) t ↔ ¬a ∈ t ∧ _root_.Disjoint s t
simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]