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

State before:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (x y : α) (xs : List α), (x == y) = false → removeAll (x :: xs) [y] = x :: removeAll xs [y]
Tactic:
intros x y xs hneq
State after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
hneq : (x == y) = false
⊢ removeAll (x :: xs) [y] = x :: removeAll xs [y]

State before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
hneq : (x == y) = false
⊢ removeAll (x :: xs) [y] = x :: removeAll xs [y]
Tactic:
simp only [removeAll, filter, notElem, elem, hneq, not]
State after:
no goals