diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 55122c71c5..c2da427e69 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -15,6 +15,8 @@ open Meta
 def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
+    if e.hasSyntheticSorry then
+      throwAbortTactic
     let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
     let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
     replaceMainGoal (mvarId' :: r.mvarIds)
@@ -25,6 +27,8 @@ def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Re
   -- See issues #2711 and #2727.
   let rwResult ← Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
+    if e.hasSyntheticSorry then
+      throwAbortTactic
     let localDecl ← fvarId.getDecl
     (← getMainGoal).rewrite localDecl.type e symm (config := config)
   let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
diff --git a/tests/lean/run/rwWithElabError.lean b/tests/lean/run/rwWithElabError.lean
new file mode 100644
index 0000000000..6013eea931
--- /dev/null
+++ b/tests/lean/run/rwWithElabError.lean
@@ -0,0 +1,22 @@
+/-!
+# Test for error reporting when `rw`/`rewrite` has an elaboration error
+-/
+
+/-!
+Elaboration failures abort tactic evaluation.
+Before, the second error was
+```
+error: tactic 'rewrite' failed, equality or iff proof expected
+  ?m.5
+⊢ True
+```
+-/
+/--
+error: unknown identifier 'not_a_theorem'
+---
+error: unsolved goals
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  rewrite [not_a_theorem]