mathlib documentation

show_term { tac } runs the tactic tac, and then prints the term that was constructed.

This is useful for

• constructing term mode proofs from tactic mode proofs, and
• understanding what tactics are doing, and how metavariables are handled.

As an example, in

example {P Q R : Prop} (h₁ : Q → P) (h₂ : R) (h₃ : R → Q) : P ∧ R :=
by show_term { tauto }

the term mode proof ⟨h₁ (h₃ h₂), eq.mpr rfl h₂⟩ produced by tauto will be printed.

As another example, if the goal is ℕ × ℕ, show_term { split, exact 0 } will print refine (0, _), and afterwards there will be one remaining goal (of type ℕ). This indicates that split, exact 0 partially filled in the original metavariable, but created a new metavariable for the resulting sub-goal.