eq.rec in goal sub-proof

Stream: new members

[Chase Norman]

I'm experiencing the issue discussed by Bjørn below:

Bjørn Kjos-Hanssen said:

When I #print the proof term, it is very long, and moreover when I try to use it directly in my code, I get invalid 'eq.rec' application,

I'm attempting to reference a subproof (in the form of an underscore) that is contained within my goal. This subproof does not work when copied because of an invalid 'eq.rec' application. Is there a more proper way to reference these proofs? library_search manages to solve the goal, but using its output does not. I presume this is unintended behavior.

[Bryan Gin-ge Chen]

Can you give a #mwe ?

[Chase Norman]

Getting a mwe might be difficult for this sort of scenario. I found a solution, albeit a 100 line copy-paste solution. For those who are experiencing the same issue, try temporarily setting set_option pp.all true .

[Bjørn Kjos-Hanssen]

There was maybe a relevant recent discussion here:
Bryan Gin-ge Chen said:

You can wrap your tactic in show_term { ... } to see the term that the tactic constructs (see tactic#show_term). In many cases the term is much too large and complex to be of any use though.

[Eric Wieser]

It would be great if there were a tactic to extract _ proofs within the goal state into local hypotheses

[Reid Barton]

It sounds like you took a wrong turn earlier.