Zulip Chat Archive

Stream: Is there code for X?

Topic: ne of mem and not mem


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:42):

You can just intro and use the stupid triangle

view this post on Zulip Marcus Rossel (Mar 02 2021 at 18:42):

@Kevin Buzzard What's the stupid triangle?

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:43):

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

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:43):

On mobile, no idea if it will work

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:45):

begin
  rintro rfl,
  exact h' h
end

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:45):

Might also work

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:46):

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

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:46):

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

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 18:46):

And not= is = -> false

view this post on Zulip Marcus Rossel (Mar 02 2021 at 19:25):

Kevin Buzzard said:

begin
  rintro rfl,
  exact h' h
end

This worked! Thanks :)

view this post on Zulip Bhavik Mehta (Mar 03 2021 at 03:47):

docs#ne_of_mem_of_not_mem


Last updated: May 16 2021 at 05:21 UTC