fix: rw should not include existing metavariables in the resulting …

…subgoals closes #4381
leanprover · Jun 6, 2024 · 349f4a7 · 349f4a7
1 parent 287d46e
commit 349f4a7
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 1 deletion.
diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -56,7 +56,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 heq
           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
@@ -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