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