chore: withLocation * should not fail if it closes the main goal (lea…

…nprover#2917)

Arising from discussion at
https://github.com/leanprover/lean4/pull/2909/files#r1398527730.

src/Lean/Elab/Tactic/Location.lean

@@ -41,13 +41,11 @@ open Meta
 
 /--
 Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
-
 * If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is included),
   and fails if any of the tactic applications fail.
 * If `loc` is `*`, runs at the target first and then the hypotheses in reverse order.
+  If `atTarget` closes the main goal, `withLocation` does not run `atLocal`.
   If all tactic applications fail, `withLocation` with call `failed` with the main goal mvar.
-  If the tactic application closes the main goal, `withLocation` will then fail with `no goals to be solved`
-  upon reaching the first hypothesis.
 -/
 def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit := do
   match loc with
@@ -59,7 +57,8 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
       withMainContext atTarget
   | Location.wildcard =>
     let worked ← tryTactic <| withMainContext <| atTarget
-    withMainContext do
+    let g ← try getMainGoal catch _ => return () -- atTarget closed the goal
+    g.withContext do
       let mut worked := worked
       -- We must traverse backwards because the given `atLocal` may use the revert/intro idiom
       for fvarId in (← getLCtx).getFVarIds.reverse do