Zulip Chat Archive

Stream: Is there code for X?

Topic: set with two elements


view this post on Zulip Rémy Degenne (Dec 15 2020 at 21:04):

I want to use the following result and I don't know how to prove it.

example {α} (i j x : α) (h_mem : x  ({i, j} : set α)) (h_ne : x  i) : x = j := sorry

My problem seems to be the following: I have no idea what {i, j} really is in mathlib (some kind of finset I suppose). For example I don't know how to get anything from the statement x ∈ {i, j}. Can someone point me to some lemmas I can use with that?

view this post on Zulip Rémy Degenne (Dec 15 2020 at 21:11):

Well, my editor answered: when hovering with the mouse over the set, it showed info about insert :) . I often forget how useful those tips can be.

view this post on Zulip Alex J. Best (Dec 15 2020 at 21:13):

In this case the tactics tidy and finish both prove this for you.

view this post on Zulip Alex J. Best (Dec 15 2020 at 21:15):

And a term mode proof is

example {α} (i j x : α) (h_mem : x  ({i, j} : set α)) (h_ne : x  i) : x = j :=
set.eq_of_mem_singleton $ set.mem_of_mem_insert_of_ne h_mem h_ne

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 21:15):

You can probably do cases h_mem on h_mem : x \in {i,j}! It's not how you're supposed to deal with it -- there will be a proper API for it -- but under the hood it's probably something like x = i \or x = j or maybe x = i \or x = j \or x \in emptyset (it used to be this but they might have changed it)

view this post on Zulip Rémy Degenne (Dec 15 2020 at 21:18):

cases did not work. That's why i wanted to know the name of the thing, to be able to find related functions, like finset.mem_insert. Now in my original proof I do rw finset.mem_insert at h_mem, cases h_mem, and continue with my buisness.

view this post on Zulip Alex J. Best (Dec 15 2020 at 21:23):

The proof tidy finds is basically what kevin suggests, its

by {cases h_mem, {induction h_mem, simp at h_ne, cases h_ne }, assumption}

view this post on Zulip Rémy Degenne (Dec 15 2020 at 21:26):

Ok, that's strange. It means that my example was in fact not representative of what happens in my bigger lemma, because cases does not work there. I'll try to understand the difference. Thanks!

view this post on Zulip Rémy Degenne (Dec 15 2020 at 21:32):

example {α} (i j x : α) (h_mem : x  ({i, j} : finset α)) (h_ne : x  i) : x = j := by finish

That corresponds better to what I needed. The difference is finset vs set. cases h_mem does not work here.

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 21:45):

Aah yeah, for finset you have to use the API. probably it's still insert i (insert j empty) though

view this post on Zulip Rémy Degenne (Dec 15 2020 at 21:47):

yes, looks like that. It's all easy now that I know that it is called insert. Knowing what word to search in the documentation is the key :)

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 22:02):

Yeah, these things are hard to figure out because some of the notation is tricky to get to the bottom of. You just have to learn what's going on. Even if you can find where it's defined in the source code it might say some stuff about scoped this and some strange syntax or maybe it's all hard coded in the C++ or whatever

view this post on Zulip Yury G. Kudryashov (Dec 17 2020 at 02:46):

{a, b, c} notation is implemented in C++


Last updated: May 07 2021 at 22:14 UTC