diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index cf5ad83f3002..986585e997a2 100644
--- 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
new file mode 100644
index 000000000000..967e7360ab69
--- /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