From ec775df6ccc02451058821e4e170dabf28aa87e5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 11 Jun 2024 04:50:58 +0200
Subject: [PATCH] fix: `rw` should not include existing goal metavariables in
 the resulting subgoals (#4385)

closes #4381
---
 src/Lean/Meta/Tactic/Rewrite.lean |  3 ++-
 tests/lean/run/4381.lean          | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/4381.lean

diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index cf5ad83f30..1dd87ab102 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/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 }
diff --git a/tests/lean/run/4381.lean b/tests/lean/run/4381.lean
new file mode 100644
index 0000000000..967e7360ab
--- /dev/null
+++ b/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