From 349cff6f0557ed55f9293bb20b13f7b3a137b8f6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 26 Jun 2025 16:41:49 -0700
Subject: [PATCH] test(goal): Collision of aux lemma names

---
 Pantograph/Goal.lean | 3 ++-
 Test/Metavar.lean    | 1 +
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index fbc9f14..8dd09dd 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -136,8 +136,9 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n]
   Meta.mapMetaM <| state.withContext' state.root
 
 private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
+  let { nextMacroScope, ngen, .. } := state
   modifyGetThe Core.State (fun st => ((),
-    { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
+    { st with nextMacroScope, ngen }))
 -- Restore the name generator and macro scopes of the core state
 protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
   restoreCoreMExtra state.coreState
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 2da177a..19d6ecd 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -291,6 +291,7 @@ def test_replay_environment : TestM Unit := do
     pure type
   let .success state1 _  ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "left"
 
+  state.restoreMetaM
   let goal := state.goals[1]!
   let type ← goal.withContext do
     let .ok type ← elabTerm (← `(term|(3: Nat) ≤ 5)) (.some $ .sort 0) | unreachable!