feat: show_term for grind interactive mode (#10862)

This PR implements the `show_term` combinator in `grind` interactive
mode.

src/Init/Grind/Interactive.lean

@@ -88,6 +88,10 @@ syntax (name := showCases) "show_cases" ppSpace grindFilter : grind
 syntax (name := «showState») "show_state" ppSpace grindFilter : grind
 /-- Show active local theorems and their anchors for heuristic instantiation. -/
 syntax (name := showLocalThms) "show_local_thms" : grind
+/--
+`show_term tac` runs `tac`, then displays the generated proof in the InfoView.
+-/
+syntax (name := showTerm) "show_term " grindSeq : grind
 
 declare_syntax_cat grind_ref (behavior := both)
 

src/Lean/Elab/Tactic/Grind/ShowState.lean

@@ -126,4 +126,10 @@ public def showState (filter : Filter) (isSilent := false) : GrindTacticM Unit :
   let msg := MessageData.trace { cls := `thms, collapsed := false } "Local theorems" msgs
   logInfo msg
 
+@[builtin_grind_tactic showTerm] def evalShowTerm : GrindTactic := fun stx => do
+  let `(grind| show_term $seq:grindSeq) := stx | throwUnsupportedSyntax
+  let mvarId := (← getMainGoal).mvarId
+  evalGrindTactic seq
+  mvarId.withContext do logInfo (← instantiateMVars (mkMVar mvarId))
+
 end Lean.Elab.Tactic.Grind