I'm using this technique to look for functions :

```
Open Scope Z_scope.
Lemma foo : forall x,
exists function, 2 * x = function x.
Proof.
intros.
match goal with
| |- exists (_ : ?T), _ => assert T as F
end.
{ refine (fun x => x + x). }
exists F.
Fail unfold F.
Abort.
```

I pretty common to need to search for a function to convert one term to another, the idea is to state that such a function exists and use refine to search for its implementation. I use `match goal`

to capture the function type and make one assertion with it, then I prove the assertion by implementing the function with help of `refine`

. At this point copy and paste the function to another place, my question is: Is it possible to make the assertion transparent so that I can unfold the F and continue the proof from where I stopped (instead of copy/pasting)?

`refine (let F := _ : T in _)`

instead of `assert T as F`

or for exists goals you can just `unshelve eexists`

Oh, I didn't know about `unshelve eexists`

thanks, cool!

Daniel Hilst Selli has marked this topic as resolved.

Oh I can do `unshelve eassert (2 * x = _ x)`

and get a subgoal focused for this hole

Last updated: Jun 15 2024 at 08:01 UTC