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

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x y : α) (xs : List α), x ≠ y → removeAllEq (x :: xs) [y] = x :: removeAllEq xs [y]
Tactic:
intro x y xs hneq
State after:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ removeAllEq (x :: xs) [y] = x :: removeAllEq xs [y]

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

State before:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
cases Decidable.em (x ∈ [y]) with
| inl hmem =>
   rw [mem_singleton_iff] at hmem
   contradiction
| inr hnmem =>
   simp [hnmem, decide_true, not_false_eq_true]
State after:
no goals

State before:
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x ∈ [y]
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
rw [mem_singleton_iff] at hmem
State after:
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x = y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs

State before:
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x = y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
contradiction
State after:
no goals

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hnmem : ¬x ∈ [y]
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
simp [hnmem, decide_true, not_false_eq_true]
State after:
no goals