From a366cbcd2047874cd8dc3c1528654a292c8645c7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 20 Oct 2025 19:30:16 -0700
Subject: [PATCH] feat: `show_term` for `grind` interactive mode (#10862)

This PR implements the `show_term` combinator in `grind` interactive
mode.
---
 src/Init/Grind/Interactive.lean           | 4 ++++
 src/Lean/Elab/Tactic/Grind/ShowState.lean | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index 7df86d5fce..908b884446 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/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)
 
diff --git a/src/Lean/Elab/Tactic/Grind/ShowState.lean b/src/Lean/Elab/Tactic/Grind/ShowState.lean
index efef401ed4..0a831066cb 100644
--- a/src/Lean/Elab/Tactic/Grind/ShowState.lean
+++ b/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