Stream: Is there code for X?

Topic: ne of mem and not mem

Marcus Rossel (Mar 02 2021 at 18:41):

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 (Mar 02 2021 at 18:42):

You can just intro and use the stupid triangle

Marcus Rossel (Mar 02 2021 at 18:42):

@Kevin Buzzard What's the stupid triangle?

Kevin Buzzard (Mar 02 2021 at 18:43):

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

Kevin Buzzard (Mar 02 2021 at 18:43):

On mobile, no idea if it will work

Kevin Buzzard (Mar 02 2021 at 18:45):

begin
rintro rfl,
exact h' h
end


Might also work

Kevin Buzzard (Mar 02 2021 at 18:46):

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

Kevin Buzzard (Mar 02 2021 at 18:46):

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

Kevin Buzzard (Mar 02 2021 at 18:46):

And not= is = -> false

Marcus Rossel (Mar 02 2021 at 19:25):

Kevin Buzzard said:

begin
rintro rfl,
exact h' h
end


This worked! Thanks :)

Bhavik Mehta (Mar 03 2021 at 03:47):

docs#ne_of_mem_of_not_mem

Last updated: May 16 2021 at 05:21 UTC