fix: rw: add all uninstantiated mvars as goals

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

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

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