# Zulip Chat Archive

## Stream: new members

### Topic: Sets

#### Brandon Brown (May 15 2020 at 03:53):

How do I do something as trivial as proving set membership?

```
import data.finset
def x1 : finset ℕ := {1,2,3}
#reduce 1 ∈ x1 --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false
example : 1 ∈ x1 := sorry
```

#### Bryan Gin-ge Chen (May 15 2020 at 03:57):

In this case you can use `dec_trivial`

:

```
import data.finset
def x1 : finset ℕ := {1,2,3}
#reduce 1 ∈ x1 --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false
example : 1 ∈ x1 := dec_trivial
```

#### Johan Commelin (May 15 2020 at 03:58):

@Brandon Brown If you've got a very explicit set, like in your example, then it's `dec_trivial`

, like Bryan said. If you have a set if the form `finset.range n`

or `finset.filter foo bar`

, then there will be lemmas `finset.mem_range`

and `finset.mem_filter`

etc... that help you proving this.

#### Brandon Brown (May 15 2020 at 03:59):

Thanks!

#### Johan Commelin (May 15 2020 at 04:00):

Brandon Brown said:

`#reduce 1 ∈ x1 --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false`

Note that this is about to change to

```
#reduce 1 ∈ x1 --1 = 1 ∨ 1 = 2 ∨ 1 = 3
```

which I think is a big improvement (-;

#### Johan Commelin (May 15 2020 at 04:01):

Also, if you don't like `dec_trivial`

, you could use a combination of `or.inl`

, `or.inr`

and `rfl`

.

#### Bryan Gin-ge Chen (May 15 2020 at 04:02):

This reminds me a lot of one of my early threads here.

#### Brandon Brown (May 15 2020 at 04:17):

I have a more basic question. I understand constructions of the form

```
variables (p q : Prop)
example (h : p) : p ∨ q := or.inl h
```

Because I'm injecting h

#### Brandon Brown (May 15 2020 at 04:18):

But I don't really understand what's going on under the hood with

```
example : (1 = 1) ∨ false := or.inl (rfl)
```

#### Mario Carneiro (May 15 2020 at 04:18):

`or.inl _`

would expect a proof of `1 = 1`

at the location of the `_`

#### Johan Commelin (May 15 2020 at 04:18):

Well, you need to inject a proof of `1 = 1`

#### Bryan Gin-ge Chen (May 15 2020 at 04:18):

Let `p := 1=1`

, `q := false`

and `h := rfl`

.

#### Mario Carneiro (May 15 2020 at 04:18):

and `rfl`

is a proof of `1 = 1`

#### Brandon Brown (May 15 2020 at 04:22):

Ahh right I see

```
variable p : (1 = 1)
example : (1 = 1) ∨ false := or.inl p
```

So using rfl is inferring this since what else could it be

#### Mario Carneiro (May 15 2020 at 04:23):

`rfl`

is short for `eq.refl _`

#### Johan Commelin (May 15 2020 at 04:23):

rfl is a smart kid (-;

#### Kevin Buzzard (May 15 2020 at 05:59):

`refl`

is a powerful tactic!

#### Kenny Lau (May 15 2020 at 06:54):

the correct way, much as I hate it, is `by simp`

:

```
import data.finset
def x1 : finset ℕ := {1,2,3}
example : 1 ∈ x1 := by simp [x1]
variables {α : Type*} [has_one α] [has_add α] [decidable_eq α]
def x2 : finset α := {1,2,3}
example : (1 : α) ∈ (x2 : finset α) := dec_trivial -- fails
example : (1 : α) ∈ (x2 : finset α) := by simp [x2] -- works
```

#### Kenny Lau (May 15 2020 at 06:58):

the last line is equivalent to `simp only [x2, eq_self_iff_true, or_true, finset.mem_insert, finset.mem_singleton, finset.singleton_eq_singleton]`

#### Kenny Lau (May 15 2020 at 06:58):

(thanks, `squeeze_simp`

)

#### Bryan Gin-ge Chen (May 15 2020 at 07:01):

That's surprising to me. Are there some missing decidability instances somewhere?

#### Kenny Lau (May 15 2020 at 07:03):

no, it's just that asserting `\a`

has decidable_eq does not actually give an algorithm to decide whether two terms of `\a`

are equal

#### Kenny Lau (May 15 2020 at 07:03):

if `\a`

is anything concrete (like `\N`

) then it will work

#### Bryan Gin-ge Chen (May 15 2020 at 07:07):

Oh, right. The type class is a `variable`

so there's no actual definition.

#### Kenny Lau (May 15 2020 at 07:19):

yeah that also confused me for a while :P

Last updated: May 14 2021 at 00:42 UTC