Show partial proof term in the proof mode

Stream: general

[Mingzhe Wang]

I am new to Lean. I know we can print the proof term after proving a lemma. Is there a way to display the partial proof term when we are writing the proof, like the command "Show Proof" in coq?

[Gabriel Ebner]

There's the show_term tactic. https://leanprover-community.github.io/mathlib_docs/tactics.html#show_term

[Mingzhe Wang]

Thanks Gabriel! This is really helpful!