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]
α : 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
no goals