exact fun x ↦ ⟨fun h ↦ ⟨(h _ ht.some_mem).1, fun hxt ↦ (h x hxt).2 rfl⟩,
  fun h y hyt ↦ ⟨h.1, fun hxy ↦ h.2 <| hxy.symm ▸ hyt⟩⟩
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ∀ (x : α), (∀ i ∈ t, x ∈ s ∧ ¬x = i) ↔ x ∈ s ∧ x ∉ t
no goals