A code action to extract/generate lemmas

Stream: general

[György Kurucz]

Basically I want to press a button in tactic mode, and get a lemma generated that exactly solves the goal. (It receives all hypotheses as arguments.)

Does this exist? I haven't found anything about something like this. Would others also find something like this useful?

Prior art from Idris2: https://idris2.readthedocs.io/en/latest/implementation/ide-protocol.html

(:make-lemma LINE NAME)
Create a top level function with a type which solves the hole named NAME on line LINE.

[Eric Wieser]

We have extract_goal

[György Kurucz]

Ah cool. What's the UX like? I type extract_goal, copy-paste the lemma statement from the InfoView, and then manually replace extract_goal with exact lemma_name param1 param2 ...? (Do I have to figure out the parameterization manually, or can maybe the apply tactic do that?)