From db110f5dfe87912b5f45350855dabacd50846824 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 27 Sep 2022 19:52:22 -0400 Subject: [PATCH] fix: preserve tags in `simp` conv --- src/Lean/Elab/Tactic/Conv/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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'`. -/