refactor: don't create a new metavariable

It's allowed to reassign a meta-variable, so there's no need to create a new goal

Tactics/Common.lean

@@ -290,23 +290,14 @@ This seems redundant, but allows us to spread out the cost of metavariable
 instantiation, and hopefully avoid some quadratic behaviour we've observed.
 -/
 def withInstantiateMainGoal (x : m α) : m α := do
-  let oldGoal ← getMainGoal
-  let newGoal ← @id (TacticM _) <| do
-    let newGoal ← mkFreshMVarId
-    let oldDecl ← oldGoal.getDecl
-    newGoal.modifyDecl (fun decl => { decl with
-      type := oldDecl.type
-      kind := oldDecl.kind
-      userName := oldDecl.userName
-      lctx := oldDecl.lctx
-      localInstances := oldDecl.localInstances
-    })
-    replaceMainGoal [newGoal]
-    pure newGoal
+  let goals ← getUnsolvedGoals
   let a ← x
-  withTraceNode `Tactic.sym (fun _ => pure m!"instantiating goal")
-    (tag := "instantiateMVar") <| do
-      let _ ← oldGoal.assign (← instantiateMVars (Expr.mvar newGoal))
+  for goal in goals do
+    if ← goal.isAssigned then
+      withTraceNode `Tactic.sym (fun _ => pure m!"instantiating goal")
+        (tag := "withInstantiateMainGoal.instantiateMVar") <| do
+          let e ← instantiateMVars (Expr.mvar goal)
+          goal.assign e
   return a
 
 /-- An emoji to show that a tactic is processing at an intermediate step. -/

Tactics/Sym.lean

@@ -367,7 +367,8 @@ in which case a new goal of the appropriate type will be added.
 The other hypotheses *must* be present,
 since we infer required information from their types. -/
 elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic =>
-  withTraceNode "" (tag := "sym_n") <| do
+  withTraceNode "" (tag := "sym_n") <|
+  withInstantiateMainGoal <| do
   traceHeartbeats "initial heartbeats"
 
   let s ← s.mapM fun
@@ -386,7 +387,6 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic =>
 
   let c ← SymContext.fromMainContext s
   SymM.run' c <|
-  withInstantiateMainGoal <|
   withMainContext' <|  do
     -- Check pre-conditions
     assertStepTheoremsGenerated