diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index f53b8a8fcd..42ca3eb343 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -73,9 +73,10 @@ def getRhs : TacticM Expr :=
 
 /-- `⊢ lhs = rhs` ~~> `⊢ lhs' = rhs` using `h : lhs = lhs'`. -/
 def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
+  let mvarId ← getMainGoal
   let rhs ← getRhs
-  let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoalRaw (← mkEq lhs' rhs))
-  (← getMainGoal).assign (← mkEqTrans h newGoal)
+  let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoalRaw (← mkEq lhs' rhs)) (← mvarId.getTag)
+  mvarId.assign (← mkEqTrans h newGoal)
   replaceMainGoal [newGoal.mvarId!]
 
 /-- Replace `lhs` with the definitionally equal `lhs'`. -/