Theorem: Set.biInter_diff_singleton_eq_diff (Matroid/ForMathlib/Set.lean)

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

State before:
α : Type u_1
ι : Type u_2
s t : Set α
ht : t.Nonempty
⊢ ∀ (x : α), (∀ i ∈ t, x ∈ s ∧ ¬x = i) ↔ x ∈ s ∧ x ∉ t
Tactic:
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⟩⟩
State after:
no goals