fix: make rewrite/rw tactic abort on elaboration errors (#6891)

This PR modifies `rewrite`/`rw` to abort rewriting if the elaborated
lemma has any immediate elaboration errors (detected by presence of
synthetic sorries). Rewriting still proceeds if there are elaboration
issues arising from pending synthetic metavariables, like instance
synthesis failures. The purpose of the change is to avoid obscure
"tactic 'rewrite' failed, equality or iff proof expected ?m.5" errors
when for example a lemma does not exist.

This helps error reporting for the natural number game.
https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20doesn't.20add_left_comm.20work.20here.3F/near/497060022

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

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]