no goals
α : Type u_1
β : Type ?u.126146
γ : Type ?u.126149
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ _root_.Disjoint (insert a t) s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
rw [disjoint_insert_left, _root_.disjoint_comm]