fix: rw should not include existing goal metavariables in the resul…

…ting subgoals (#4385)

closes #4381

src/Lean/Meta/Tactic/Rewrite.lean

@@ -25,6 +25,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
   mvarId.withContext do
     mvarId.checkNotAssigned `rewrite
+    let heqIn := heq
     let heqType ← instantiateMVars (← inferType heq)
     let (newMVars, binderInfos, heqType) ← forallMetaTelescopeReducing heqType
     let heq := mkAppN heq newMVars
@@ -56,7 +57,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
             (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
-          let otherMVarIds ← getMVarsNoDelayed eqPrf
+          let otherMVarIds ← getMVarsNoDelayed heqIn
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
           let newMVarIds := newMVarIds ++ otherMVarIds
           pure { eNew := eNew, eqProof := eqPrf, mvarIds := newMVarIds.toList }

tests/lean/run/4381.lean

@@ -0,0 +1,18 @@
+/--
+info: case h
+d g : Nat
+H1 : d = g
+⊢ ?w = g
+
+case w
+d g : Nat
+H1 : d = g
+⊢ Nat
+-/
+#guard_msgs in
+example : ∀ d g, d = g → exists x : Nat, x = d := by
+  intros d g H1
+  constructor
+  rewrite [H1,←H1,H1,←H1,H1]
+  trace_state
+  assumption