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

State before:
α : Type u_1
ι : Type u_2
s : Set α
x : α
h : x ∈ s
⊢ x ∉ s \ {x}
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
s : Set α
x : α
h : x ∈ s
⊢ s = insert x (s \ {x})
Tactic:
simp [insert_eq_of_mem h]
State after:
no goals