From 2dbbe2509e1aa83dfbe8715beda0af0c6a145691 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 2 Jul 2025 15:46:29 -0700
Subject: [PATCH 1/2] fix(tactic): Erase finished calc goal

---
 Pantograph/Tactic/Fragment.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Tactic/Fragment.lean b/Pantograph/Tactic/Fragment.lean
index 1716942..6bd9fc7 100644
--- a/Pantograph/Tactic/Fragment.lean
+++ b/Pantograph/Tactic/Fragment.lean
@@ -144,11 +144,12 @@ protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (
       unless ← Meta.isDefEq proofType target do throwFailed
       remainder? := .some lastStepGoal.mvarId!
     goal.assign proof
+    let map := map.erase goal
 
     let goals := [ mvarBranch ] ++ remainder?.toList
     Elab.Tactic.setGoals goals
     match remainder? with
-    | .some goal => return map.erase goal |>.insert goal $ .calc (.some rhs)
+    | .some goal => return map.insert goal $ .calc (.some rhs)
     | .none => return map
   | .conv .. => do
     throwError "Direct operation on conversion tactic parent goal is not allowed"

From 92befda2ffe04a862f0ed7800797cb5fc4cfb308 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 7 Jul 2025 14:47:50 -0700
Subject: [PATCH 2/2] test(tactic): Check fragments have been erased

---
 Test/Tactic/Fragment.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Test/Tactic/Fragment.lean b/Test/Tactic/Fragment.lean
index 51b3a3e..cc51cf7 100644
--- a/Test/Tactic/Fragment.lean
+++ b/Test/Tactic/Fragment.lean
@@ -126,8 +126,8 @@ def test_conv_simple: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic ((← stateF.serializeGoals).map (·.devolatilize) =
-    #[])
+  checkEq tactic ((← stateF.serializeGoals).map (·.devolatilize)) #[]
+  checkEq "fragments" stateF.fragments.size 0
 
   where
     h := "b + a + c1 = b + a + c2"
@@ -180,6 +180,7 @@ def test_conv_unshielded : TestM Unit := do
   let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   let root? := state.rootExpr?
   checkTrue "root" root?.isSome
+  checkEq "fragments" state.fragments.size 0
   where
   interiorGoal (free: List (String × String)) (target: String) :=
     let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free