fix: bug in replaceLocalDeclDefEq

fixes #1615

src/Lean/Meta/Tactic/Replace.lean

@@ -99,10 +99,10 @@ Remark: this method assumes that `typeNew` is definitionally equal to the curren
 -/
 def _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do
   mvarId.withContext do
-    let mvarDecl ← mvarId.getDecl
-    if typeNew == mvarDecl.type then
+    if typeNew == (← fvarId.getType) then
       return mvarId
     else
+      let mvarDecl ← mvarId.getDecl
       let lctxNew := (← getLCtx).modifyLocalDecl fvarId (·.setType typeNew)
       let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) mvarDecl.type mvarDecl.kind mvarDecl.userName
       mvarId.assign mvarNew

tests/lean/run/1615.lean

@@ -0,0 +1,17 @@
+import Lean.Elab.ElabRules
+import Lean.Meta.Tactic.Replace
+
+elab "test" h:ident : tactic => do
+  let g ← Lean.Elab.Tactic.getMainGoal
+  g.withContext do
+    let ldec ← Lean.Meta.getLocalDeclFromUserName h.getId
+    let f := ldec.fvarId
+    let e ← Lean.Meta.whnf (← Lean.instantiateMVars ldec.type)
+    let newgoal ← g.replaceLocalDeclDefEq f e
+    Lean.Elab.Tactic.replaceMainGoal [newgoal]
+
+def Nat.dvd (a b : Nat) := ∃ c, b = a * c
+
+example (n : Nat) (h : Nat.dvd 2 n) : ∃ c, n = 2 * c := by
+  test h
+  with_reducible exact h