diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index 0be0607ad4..f057ee311d 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -45,8 +45,11 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let eqRefl ← mkEqRefl e
           let eqPrf ← mkEqNDRec motive eqRefl heq
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
-          let newMVars ← newMVars.filterM fun mvar => not <$> isExprMVarAssigned mvar.mvarId!
-          pure { eNew := eNew, eqProof := eqPrf, mvarIds := newMVars.toList.map Expr.mvarId! }
+          let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM (not <$> isExprMVarAssigned ·)
+          let otherMVarIds ← getMVarsNoDelayed eqPrf
+          let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
+          let newMVarIds := newMVarIds ++ otherMVarIds
+          pure { eNew := eNew, eqProof := eqPrf, mvarIds := newMVarIds.toList }
         match symm with
         | false => cont heq heqType lhs rhs
         | true  => do
diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean
index 16d893a646..5e9245a74b 100644
--- a/tests/lean/rewrite.lean
+++ b/tests/lean/rewrite.lean
@@ -45,3 +45,6 @@ exact h₁ h₃
 theorem ex7 (p q r : Prop) (h₁ : q → r) (h₂ : p ↔ q) (h₃ : p) : r := by
 rw [h₂] at h₃;
 exact h₁ h₃
+
+example (α : Type) (p : Prop) (a b c : α) (h : p → a = b) : a = c := by
+  rw [h _]  -- should manifest goal `⊢ p`, like `rw [h]` would
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index 5c4d117b7a..c619e3c911 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -19,3 +19,15 @@ m n k : Nat
  : n = m
 h : k = m
 ⊢ k = n
+rewrite.lean:49:69-50:10: error: unsolved goals
+α : Type
+p : Prop
+a b c : α
+h : p → a = b
+⊢ b = c
+
+α : Type
+p : Prop
+a b c : α
+h : p → a = b
+⊢ p