diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 9be5164..d92a807 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -247,7 +247,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
     -- See Lean.Elab.Tactic.Conv.convTarget
     let convMVar ← Elab.Tactic.withMainContext do
       let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
-      Elab.Tactic.setGoals [newGoal.mvarId!]
+      Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
       pure rhs.mvarId!
     return (← MonadBacktrack.saveState, convMVar)
   try
diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean
index acf5d16..8a5b998 100644
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@@ -25,7 +25,7 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
     (tagSuffix := .anonymous )
     (allowNaturalHoles := true)
   goal.assign expr
-  Elab.Tactic.setGoals nextGoals
+  Elab.Tactic.replaceMainGoal nextGoals
 
 
 end Pantograph.Tactic
diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean
index 2ff23d2..dfb329d 100644
--- a/Pantograph/Tactic/Congruence.lean
+++ b/Pantograph/Tactic/Congruence.lean
@@ -31,7 +31,7 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
 def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let nextGoals ← congruenceArg goal
-  Elab.Tactic.setGoals nextGoals
+  Elab.Tactic.replaceMainGoal nextGoals
 
 def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
   mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
@@ -60,7 +60,7 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
 def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let nextGoals ← congruenceFun goal
-  Elab.Tactic.setGoals nextGoals
+  Elab.Tactic.replaceMainGoal nextGoals
 
 def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
   mvarId.checkNotAssigned `Pantograph.Tactic.congruence
@@ -93,6 +93,6 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
 def evalCongruence: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
   let nextGoals ← congruence goal
-  Elab.Tactic.setGoals nextGoals
+  Elab.Tactic.replaceMainGoal nextGoals
 
 end Pantograph.Tactic
diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 99e499d..2c52f12 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -100,6 +100,6 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
 def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   let recursor ← Elab.Term.elabTerm (stx := stx) .none
   let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
-  Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
+  Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
 
 end Pantograph.Tactic
diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean
index f4ce78f..e9ff459 100644
--- a/Pantograph/Tactic/NoConfuse.lean
+++ b/Pantograph/Tactic/NoConfuse.lean
@@ -17,6 +17,6 @@ def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
   let goal ← Elab.Tactic.getMainGoal
   let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
   noConfuse goal h
-  Elab.Tactic.setGoals []
+  Elab.Tactic.replaceMainGoal []
 
 end Pantograph.Tactic