# Zulip Chat Archive

## Stream: general

### Topic: Extract value from fin.find

#### Jure Taslak (Slovenia) (Sep 30 2021 at 10:07):

I have the following problem:

I'm trying to use the `fin.find`

function to extract a value `k : fin n`

for which `p k`

holds. Together with that I would like a proof that this indeed holds, of the form `pk : p k`

.

However if I use the `cases`

tactic on `fin.find p`

in the `some k`

case I only get the `k : fin n`

but no proof. I tried to get this proof using `fin.find_spec`

but I got to the point I have to show `fin.find p = some k`

, from where I don't really know where to go, as I thought this was the assumption of the case we are in.

#### Mario Carneiro (Sep 30 2021 at 10:08):

You probably need to match on docs#fin.find and docs#fin.find_spec together

#### Mario Carneiro (Sep 30 2021 at 10:08):

actually, looking at the definition of `fin.find_spec`

it seems that `cases e : fin.find p`

should work

#### Jure Taslak (Slovenia) (Sep 30 2021 at 10:10):

Aha you're right, I just had to specify e to have it as an assumption.

Thank you very much.

Last updated: Aug 03 2023 at 10:10 UTC