Tool for extracting current goal into a dedicated lemma?

Stream: general

[aprilgrimoire]

Hi! Sometimes I need to write long proofs due to things with many parameters, for example, Subfield.closure_induction. In such cases, I need to split some of the proof into a dedicated lemma to prevent timeout at whnf. Just like simp?, is there a tactic or tool that could help me formulate such lemmas?

[Luigi Massacci]

Yes, it's called extract_goal ; )

[Luigi Massacci]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/ExtractGoal.html

[Eric Wieser]

Note that when using Subfield.closure_induction, you probably want to write it using induction hx using Subfield.closure_induction, which might also help simplify your proof / make it easier to follow.

[aprilgrimoire]

Thanks!
image.png
Why did it contain omits? Where can I see the full version?

[Eric Wieser]

I think if you hover over the ..., lean will tell you the setting to make it show that detail

[aprilgrimoire]

Yeah, but then I can't simply copy the statement out. How can I invoke the linter in a terminal?

[aprilgrimoire]

Oh sorry seems the link you provided contained info about it

[Eric Wieser]

I don't really understand your question; did you solve it?

[Eric Wieser]

In the particular example you gave above, I think running dsimp before extract_goal will help

[aprilgrimoire]

Yeah I solved it. set_option pp.proofs true in extract_goal worked. Sorry for the late reply, I was working on an assignment yesterday.