From 5f5cc55d6a4b7eea594222727cd686f0b9529871 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Mar 2021 12:04:14 -0800
Subject: [PATCH] feat: add helper method

---
 src/Lean/Elab/Tactic/Basic.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index e710ed0940..e606d7bd2d 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -195,6 +195,17 @@ def getMainTag : TacticM Name := do
   let (g, _) ← getMainGoal
   pure (← getMVarDecl g).userName
 
+/- Evaluate `tac` at `mvarId`, and return the list of resulting subgoals. -/
+def evalTacticAt (tac : Syntax) (mvarId : MVarId) : TacticM (List MVarId) := do
+  let gs ← getGoals
+  try
+    setGoals [mvarId]
+    evalTactic tac
+    pruneSolvedGoals
+    getGoals
+  finally
+    setGoals gs
+
 def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   let e ← instantiateMVars e
   let pendingMVars ← getMVars e