Factoring out a lemma

Stream: lean4

[Zack Weinberg]

Suppose I have a big messy goal which I would like, for presentational reasons, to separate from the current proof and solve as a separate theorem/lemma. Copying the goal expression out of the goal window and into a new theorem structure doesn't always work, for example if it includes chained up-arrow conversions, these may be ambiguous.

Is there a way to tell Lean to print out the current goal in an unambiguous form, one that can be copied into a new theorem without needing to be fixed up, and such that exact new_theorem will solve that goal (assuming a proof of new_theorem)?

[Zack Weinberg]

I found pp.all and that works but it goes way too far; my new_theorem's statement is now 129 lines of syntax tree.

[Ruben Van de Velde]

extract_goal, but it hits the same issue with not round tripping

[Zack Weinberg]

yeah, that is only slightly helpful

[Zack Weinberg]

it looks like it's printing the exact same thing that the goal window had

[Zack Weinberg]

in my specific case, set_option pp.coercions.types true got extract_goal to print expressions that are still pretty ugly, but not unmanageably so, and that do work

[Kevin Buzzard]

yeah up-arrow coercions is the classic reason for failure to round-trip. With the goals I often work with, just removing the up-arrows has a fair chance of rescuing the situation.

[Zack Weinberg]

Double conversions (from Fin to Nat to Int) were what was messing things up for me.

I wonder if a direct Fin->Int coercion would be useful.