ne of mem and not mem

Stream: Is there code for X?

[Marcus Rossel]

Is there a lemma that proves?:

example {ι : Type*} (l : list ι) (x x' : ι) (h : x ∈ l) (h' : x' ∉ l) : x ≠ x'

The finish tactic works, but I don't know how it does it.

[Kevin Buzzard]

You can just intro and use the stupid triangle

[Marcus Rossel]

@Kevin Buzzard What's the stupid triangle?

[Kevin Buzzard]

lam h1, h' $ h1.symm \t h

[Kevin Buzzard]

On mobile, no idea if it will work

[Kevin Buzzard]

begin
  rintro rfl,
  exact h' h
end

[Kevin Buzzard]

Might also work

[Kevin Buzzard]

Or intro h1, rw h1 at h, exact h' h

[Kevin Buzzard]

The point is that notin is defined to mean in -> false

[Kevin Buzzard]

And not= is = -> false

[Marcus Rossel]

Kevin Buzzard said:

begin
  rintro rfl,
  exact h' h
end

This worked! Thanks :)

[Bhavik Mehta]

docs#ne_of_mem_of_not_mem