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

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

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAllEq (x :: xs) [x] = removeAllEq xs [x]
Tactic:
simp [removeAllEq, filter, notElem, elem]
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs
Tactic:
have hmem : x ∈ [x] := by constructor
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
hmem : x ∈ [x]
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
hmem : x ∈ [x]
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs
Tactic:
simp only [hmem, decide_true, not]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ x ∈ [x]
Tactic:
constructor
State after:
no goals