simp only [ext_iff, mem_iInter, mem_diff, mem_singleton_iff]
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ⋂ i ∈ t, s \ {i} = s \ t
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ∀ (x : α), (∀ i ∈ t, x ∈ s ∧ ¬x = i) ↔ x ∈ s ∧ x ∉ t