set with two elements

Stream: Is there code for X?

[Rémy Degenne]

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?

[Rémy Degenne]

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.

[Alex J. Best]

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

[Alex J. Best]

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

[Kevin Buzzard]

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)

[Rémy Degenne]

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.

[Alex J. Best]

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}

[Rémy Degenne]

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!

[Rémy Degenne]

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.

[Kevin Buzzard]

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

[Rémy Degenne]

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 :)

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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