# Zulip Chat Archive

## Stream: new members

### Topic: two finsets of all of fin n are the same

#### Evan Lohn (Dec 24 2021 at 13:57):

I wasn't sure how to prove the following:

```
import data.finset.basic
def rowindset : finset (fin 4) := list.to_finset [fin.of_nat 0, fin.of_nat 1, fin.of_nat 2, fin.of_nat 3]
example {r0 r1 r2 r3 : fin 4}
(h1 : r0 ≠ r1)
(h2 : r0 ≠ r2 ∧ r1 ≠ r2)
(h3 : r0 ≠ r3 ∧ r1 ≠ r3 ∧ r2 ≠ r3) :
rowindset = [r0, r1, r2, r3].to_finset :=
begin
sorry,
end
```

essentially "four different elements of fin 4 are the same as the explicitly constructed set of the elements of fin 4". I'd be grateful if someone could point me to relevant lemmas and/or weirdness in my definition!

#### Anne Baanen (Dec 24 2021 at 14:01):

Since there are finitely many options and we can compute with `fin`

, you can ask Lean to check all possibilities:

```
example : ∀ {r0 r1 r2 r3 : fin 4}
(h1 : r0 ≠ r1)
(h2 : r0 ≠ r2 ∧ r1 ≠ r2)
(h3 : r0 ≠ r3 ∧ r1 ≠ r3 ∧ r2 ≠ r3),
rowindset = [r0, r1, r2, r3].to_finset :=
by dec_trivial
```

#### Anne Baanen (Dec 24 2021 at 14:03):

Of course that doesn't scale to lots of `fin`

s :)

#### Evan Lohn (Dec 24 2021 at 14:05):

Thanks! Not sure if it's my version of Lean or mathlib that's causing this problem, but I had to use the exclam version `dec_trivial!`

for some reason.

#### Johan Commelin (Dec 24 2021 at 14:07):

Note that Anne put all the assumptions in the goal (that is, right of the `:`

)

#### Johan Commelin (Dec 24 2021 at 14:07):

`dec_trivial!`

tries to do that for you.

#### Anne Baanen (Dec 24 2021 at 14:17):

I didn't even realize that `dec_trivial!`

existed :grinning:

#### Kevin Buzzard (Dec 24 2021 at 15:22):

Whenever a tactic I try doesn't work, I always append an exclamation mark and try again ;-)

Last updated: Dec 20 2023 at 11:08 UTC