## Stream: Is there code for X?

### Topic: Classical Choice on finset

#### Marcus Rossel (Jan 15 2021 at 21:24):

Is it possible to somehow choose an item from a finset à la classical.choice?

#### Adam Topaz (Jan 15 2021 at 21:26):

You need nonempty. The empty set is still finite :)

#### Adam Topaz (Jan 15 2021 at 21:27):

What do you mean by choose? Are you in the middle of a tactic block? If so, you can do a case-split using docs#finset.nonempty

#### Yakov Pechersky (Jan 15 2021 at 21:28):

Yes, you can. docs#finset.choose

#### Yakov Pechersky (Jan 15 2021 at 21:29):

You have provide a proof that the element you'll be choosing is in the finset, and moreover, the unique one satisfying the property you're choosing for.

#### Marcus Rossel (Jan 15 2021 at 21:30):

What do you mean by choose? Are you in the middle of a tactic block? If so, you can do a case-split using docs#finset.nonempty

I mean extract some element from the set. So nonempty is exactly what I need for that.

#### Adam Topaz (Jan 15 2021 at 21:32):

gotcha.

Last updated: May 07 2021 at 22:14 UTC