# Zulip Chat Archive

## Stream: new members

### Topic: finset members

#### Damiano Testa (Sep 22 2020 at 09:29):

Dear All,

I am trying to prove either one of the two lemmas below, but Lean is not allowing me to. I would like to `convert set.mem_union_right ↑s`

, but I am not able to proceed from there. As usual, I imagine that Lean is obtaining different sources for something and cannot reconcile them, but I am not able to figure out what.

Thank you!

```
import tactic
lemma mem_in_union {α : Type*} [decidable_eq α] [has_union (finset α)] {s t : finset α} (x : α) : x ∈ t → x ∈ (s ∪ t) :=
begin
sorry,
end
lemma mem_in_union_singleton {α : Type*} [decidable_eq α] [has_union (finset α)] {s : finset α} (x : α) : x ∈ (s ∪ {x}) :=
begin
sorry,
end
```

#### Johan Commelin (Sep 22 2020 at 09:30):

You shouldn't need `has_union`

... Lean should figure it out by itself.

#### Johan Commelin (Sep 22 2020 at 09:30):

That indeed adds a second (unrelated, out-of-the-blue) notion of union for `finset \a`

#### Johan Commelin (Sep 22 2020 at 09:32):

```
lemma mem_in_union {α : Type*} [decidable_eq α] {s t : finset α} (x : α) : x ∈ t → x ∈ (s ∪ t) :=
begin
library_search
end
```

#### Damiano Testa (Sep 22 2020 at 09:32):

I added `has_union`

since Lean wanted it, but I will try to remove it again!

#### Johan Commelin (Sep 22 2020 at 09:32):

The `decidable_eq`

enables the union instance. Without it, lean can't find it. (But then, if you `open_locale classical`

everything works again)

#### Damiano Testa (Sep 22 2020 at 09:33):

ah, I think that I added first `has_union`

, prompted by Lean, and then added `decidable_eq`

(again prompted by Lean)

#### Johan Commelin (Sep 22 2020 at 09:33):

@Damiano Testa this is the "eternal(?)" conflict between proving and computing...

#### Johan Commelin (Sep 22 2020 at 09:34):

I think, if you do maths, you should forget about the `decidable_eq`

stuff, and just use `open_locale classical`

at the top of your files.

#### Johan Commelin (Sep 22 2020 at 09:34):

But sometimes `decidable_*`

is really powerful.

#### Damiano Testa (Sep 22 2020 at 09:34):

ok, I will do that!

#### Johan Commelin (Sep 22 2020 at 09:35):

E.g., if you want to know that squares mod 8 are equal to 0, 1, or 4, then `dec_trivial`

will prove it for you.

#### Johan Commelin (Sep 22 2020 at 09:35):

And that 1 line proof is of course a lot more convenient than whatever crazy case-split you would have to do otherwise.

#### Damiano Testa (Sep 22 2020 at 09:36):

ok, indeed, with `open_locale classical`

i do not need to add `decidable_eq`

!! Thank you very much!

#### Johan Commelin (Sep 22 2020 at 09:56):

@Damiano Testa What `open_locale classical`

does, is that it makes every proposition decidable, using LEM. Of course it is "cheating" and using an axiom, and Lean knows this. So you can't use it to decide the truth of you favourite conjecture afterwards. But at the same time, Lean also won't get hung up on the fact that it doesn't know how to decide whether `x \in s`

is true or not.

#### Patrick Massot (Sep 22 2020 at 10:42):

I don't understand why you write "cheating". This has nothing to do with cheating.

#### Johan Commelin (Sep 22 2020 at 10:42):

It is "cheating" in the sense that "decidable" no longer means what it usually means.

#### Patrick Massot (Sep 22 2020 at 10:43):

This command simply gives up hope to get Lean to *compute* a number of things. That's all. You can still do reasoning, without cheating, but you cannot compute.

#### Patrick Massot (Sep 22 2020 at 10:43):

The command says "don't try to use decidability".

#### Johan Commelin (Sep 22 2020 at 10:45):

If someone tells you that the Riemann Hypothesis is decidable, usually that would mean that you can run an algorithm and it will spit out `true`

or `false`

in the end. But if you have `open_locale classical`

, then everything is decidable, and no such algorithms need to exist.

#### Damiano Testa (Sep 22 2020 at 12:00):

Well, there is an algorithm that spits out `true`

if the Riemann hypothesis is true and `false`

otherwise. Just no one seems to know which one it is, at the moment!

#### Damiano Testa (Sep 22 2020 at 12:00):

Anyway, I think that I am getting an idea of what is going on here: thank you!

Last updated: May 17 2021 at 22:15 UTC