diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index f58c7820cd..67cc91c88d 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -52,6 +52,7 @@ instance : Monad TacticM :=
 instance : Inhabited (TacticM α) where
   default := fun _ _ => default
 
+/-- Returns the list of goals. Goals may or may not already be assigned. -/
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 
@@ -300,13 +301,22 @@ instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState
   restoreState b := b.restore
 
+/--
+Non-backtracking `try`/`catch`.
+-/
 @[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
+  try x catch ex => h ex
+
+/--
+Backtracking `try`/`catch`. This is used for the `MonadExcept` instance for `TacticM`.
+-/
+@[inline] protected def tryCatchRestore {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do
   let b ← saveState
   try x catch ex => b.restore; h ex
 
 instance : MonadExcept Exception TacticM where
   throw    := throw
-  tryCatch := Tactic.tryCatch
+  tryCatch := Tactic.tryCatchRestore
 
 /-- Execute `x` with error recovery disabled -/
 def withoutRecover (x : TacticM α) : TacticM α :=
@@ -342,12 +352,26 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do
   let stx' ← exp stx
   withMacroExpansion stx stx' $ evalTactic stx'
 
-/-- Add the given goals at the end of the current goals collection. -/
+/-- Add the given goal to the front of the current list of goals. -/
+def pushGoal (mvarId : MVarId) : TacticM Unit :=
+  modify fun s => { s with goals := mvarId :: s.goals }
+
+/-- Add the given goals to the front of the current list of goals. -/
+def pushGoals (mvarIds : List MVarId) : TacticM Unit :=
+  modify fun s => { s with goals := mvarIds ++ s.goals }
+
+/-- Add the given goals at the end of the current list of goals. -/
 def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
   modify fun s => { s with goals := s.goals ++ mvarIds }
 
-/-- Discard the first goal and replace it by the given list of goals,
-keeping the other goals. -/
+/--
+Discard the first goal and replace it by the given list of goals,
+keeping the other goals. This is used in conjunction with `getMainGoal`.
+
+Contract: between `getMainGoal` and `replaceMainGoal`, nothing manipulates the goal list.
+
+See also `Lean.Elab.Tactic.popMainGoal` and `Lean.Elab.Tactic.pushGoal`/`Lean.Elab.Tactic.pushGoal` for another interface.
+-/
 def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
   let (_ :: mvarIds') ← getGoals | throwNoGoalsToBeSolved
   modify fun _ => { goals := mvarIds ++ mvarIds' }
@@ -365,6 +389,16 @@ where
         setGoals (mvarId :: mvarIds)
         return mvarId
 
+/--
+Return the first goal, and remove it from the goal list.
+
+See also: `Lean.Elab.Tactic.pushGoal` and `Lean.Elab.Tactic.pushGoals`.
+-/
+def popMainGoal : TacticM MVarId := do
+  let mvarId ← getMainGoal
+  replaceMainGoal []
+  return mvarId
+
 /-- Return the main goal metavariable declaration. -/
 def getMainDecl : TacticM MetavarDecl := do
   (← getMainGoal).getDecl
diff --git a/src/Lean/Elab/Tactic/Calc.lean b/src/Lean/Elab/Tactic/Calc.lean
index 0ade7b9434..ceea168630 100644
--- a/src/Lean/Elab/Tactic/Calc.lean
+++ b/src/Lean/Elab/Tactic/Calc.lean
@@ -14,9 +14,9 @@ open Meta
 @[builtin_tactic Lean.calcTactic]
 def evalCalc : Tactic := fun stx => withMainContext do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
-  let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
-    let target := (← getMainTarget).consumeMData
-    let tag ← getMainTag
+  let target := (← getMainTarget).consumeMData
+  let tag ← getMainTag
+  let (val, mvarIds) ← withCollectingNewGoalsFrom (parentTag := tag) (tagSuffix := `calc) do
     runTermElab do
     let mut val ← Term.elabCalcSteps steps
     let mut valType ← instantiateMVars (← inferType val)
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 94e92bad8b..d4c9d0a68e 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -56,11 +56,6 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
       Term.throwTypeMismatchError none expectedType eType e
     return e
 
-/-- Try to close main goal using `x target`, where `target` is the type of the main goal.  -/
-def closeMainGoalUsing (tacName : Name) (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit :=
-  withMainContext do
-    closeMainGoal (tacName := tacName) (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
-
 def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
    if (← Term.logUnassignedUsingErrorInfos mvarIds) then
      throwAbortTactic
@@ -69,14 +64,37 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
   let mctx ← getMCtx
   return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
 
+/--
+Try to close main goal using `x target tag`, where `target` is the type of the main goal and `tag` is its user name.
+
+If `checkNewUnassigned` is true, then throws an error if the resulting value has metavariables that were created during the execution of `x`.
+If it is false, then it is the responsibility of `x` to add such metavariables to the goal list.
+
+During the execution of `x`:
+* The local context is that of the main goal.
+* The goal list has the main goal removed.
+* It is allowable to modify the goal list, for example with `Lean.Elab.Tactic.pushGoals`.
+
+On failure, the main goal remains at the front of the goal list.
+-/
+def closeMainGoalUsing (tacName : Name) (x : Expr → Name → TacticM Expr) (checkNewUnassigned := true) : TacticM Unit := do
+  let mvarCounterSaved := (← getMCtx).mvarCounter
+  let mvarId ← popMainGoal
+  Tactic.tryCatch
+    (mvarId.withContext do
+      let val ← x (← mvarId.getType) (← mvarId.getTag)
+      if checkNewUnassigned then
+        let mvars ← filterOldMVars (← getMVars val) mvarCounterSaved
+        logUnassignedAndAbort mvars
+      unless (← mvarId.checkedAssign val) do
+        throwTacticEx tacName mvarId m!"attempting to close the goal using{indentExpr val}\nthis is often due occurs-check failure")
+    (fun ex => do
+      pushGoal mvarId
+      throw ex)
+
 @[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
   match stx with
-  | `(tactic| exact $e) =>
-    closeMainGoalUsing `exact (checkUnassigned := false) fun type => do
-      let mvarCounterSaved := (← getMCtx).mvarCounter
-      let r ← elabTermEnsuringType e type
-      logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
-      return r
+  | `(tactic| exact $e) => closeMainGoalUsing `exact fun type _ => elabTermEnsuringType e type
   | _ => throwUnsupportedSyntax
 
 def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
@@ -93,9 +111,12 @@ def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : List MVarId) : m (List
   return (← sortMVarIdArrayByIndex mvarIds.toArray).toList
 
 /--
-  Execute `k`, and collect new "holes" in the resulting expression.
+Execute `k`, and collect new "holes" in the resulting expression.
+
+* `parentTag` and `tagSuffix` are used to tag untagged goals with `Lean.Elab.Tactic.tagUntaggedGoals`.
+* If `allowNaturalHoles` is true, then `_`'s are allowed and create new goals.
 -/
-def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
+def withCollectingNewGoalsFrom (k : TacticM Expr) (parentTag : Name) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) :=
   /-
   When `allowNaturalHoles = true`, unassigned holes should become new metavariables, including `_`s.
   Thus, we set `holesAsSyntheticOpaque` to true if it is not already set to `true`.
@@ -144,7 +165,7 @@ where
     appear in the `.lean` file. We should tell users to prefer tagged goals.
     -/
     let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList
-    tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
+    tagUntaggedGoals parentTag tagSuffix newMVarIds
     return (val, newMVarIds)
 
 /-- Elaborates `stx` and collects the `MVarId`s of any holes that were created during elaboration.
@@ -153,8 +174,8 @@ With `allowNaturalHoles := false` (the default), any new natural holes (`_`) whi
 be synthesized during elaboration cause `elabTermWithHoles` to fail. (Natural goals appearing in
 `stx` which were created prior to elaboration are permitted.)
 
-Unnamed `MVarId`s are renamed to share the main goal's tag. If multiple unnamed goals are
-encountered, `tagSuffix` is appended to the main goal's tag along with a numerical index.
+Unnamed `MVarId`s are renamed to share the tag `parentTag?` (or the main goal's tag if `parentTag?` is `none`).
+If multiple unnamed goals are encountered, `tagSuffix` is appended to this tag along with a numerical index.
 
 Note:
 * Previously-created `MVarId`s which appear in `stx` are not returned.
@@ -163,8 +184,8 @@ metavariables.
 * When `allowNaturalHoles := true`, `stx` is elaborated under `withAssignableSyntheticOpaque`,
 meaning that `.syntheticOpaque` metavariables might be assigned during elaboration. This is a
 consequence of the implementation. -/
-def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
-  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) tagSuffix allowNaturalHoles
+def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) (parentTag? : Option Name := none) : TacticM (Expr × List MVarId) := do
+  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) (← parentTag?.getDM getMainTag) tagSuffix allowNaturalHoles
 
 /-- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
    Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
@@ -395,7 +416,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi
   return inst
 
 def evalDecideCore (tacticName : Name) (kernelOnly : Bool) : TacticM Unit :=
-  closeMainGoalUsing tacticName fun expectedType => do
+  closeMainGoalUsing tacticName fun expectedType _ => do
     let expectedType ← preprocessPropToDecide expectedType
     let pf ← mkDecideProof expectedType
     -- Get instance from `pf`
@@ -501,7 +522,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
   pure auxName
 
 @[builtin_tactic Lean.Parser.Tactic.nativeDecide] def evalNativeDecide : Tactic := fun _ =>
-  closeMainGoalUsing `nativeDecide fun expectedType => do
+  closeMainGoalUsing `nativeDecide fun expectedType _ => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d