Not a member of List

Stream: lean4

[Abdalrhman M Mohamed]

I am trying to prove a theorem and came across a goal of the following form:

example : x ≠ y → x ∉ [y] := _

I can easily prove the version without the negations, but I cannot think of a way to prove this one. Can someone give some guidance on how to prove this simple statement?

[Mario Carneiro]

I would hope by simp does it

[Mario Carneiro]

the non-automated version is to apply mt to turn it into x \in [y] -> x = y, and then apply a theorem called List.mem_single or something which says x \in [y] <-> x = y

[Leonardo de Moura]

List.Mem is an inductive predicate with two constructors. You can also use pattern matching to prove this goal.

-- `cases` tactic version
example : x ≠ y → x ∉ [y] := by
  intro hne hin
  cases hin <;> contradiction

-- `match` version
example : x ≠ y → x ∉ [y] :=
  fun hne hin =>
    match hin with
    | List.Mem.head _ => hne rfl -- `match` refined `hne` type to `x ≠ x`
    -- Remark `match` can figure out that the case `List.Mem.tail` is "unreachable"

-- Compressed version of the previous example.
example : x ≠ y → x ∉ [y] :=
  fun hne (List.Mem.head _) => hne rfl