Convert tactic proof

Stream: new members

[Hunter Monroe]

How do you convert a tactic-based proof to a term? I saw this in a video and could not find it again.

[Hanting Zhang]

show_term

[Hanting Zhang]

around the thing you want

[Kevin Buzzard]

show_term will work on any tactic in the proof, or even a subset of tactics if you group them together with { }. If you just want to see the entire proof term then #print theorem_name should work.