match hba : b == a with
| true =>
  dsimp; cases of_decide_eq_true hba
  intro ha; exact hhead _ ha rfl
| false =>
  dsimp; simp [not_or]
  apply And.intro
  . exact Ne.symm <| of_decide_eq_false hba
  . exact IH htail
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ¬a ∈
      match b == a with
      | true => l
      | false => b :: List.erase l a
no goals