Extract value from fin.find

Stream: general

[Jure Taslak (Slovenia)]

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]

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

[Mario Carneiro]

actually, looking at the definition of fin.find_spec it seems that cases e : fin.find p should work

[Jure Taslak (Slovenia)]

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