Theorem: List.removeAll_singleton_hd_eq (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (xs : List α), removeAll (x :: xs) [x] = removeAll xs [x]
Tactic:
intros x xs
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAll (x :: xs) [x] = removeAll xs [x]

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAll (x :: xs) [x] = removeAll xs [x]
Tactic:
simp [removeAll, filter, notElem, elem]
State after:
no goals