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