diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 322bfcb859..52b497d09e 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -347,7 +347,10 @@ mutual
               -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
               withTacticInfoContext tacticCode[0] do
                 withNarrowedArgTacticReuse (argIdx := 1) (evalTactic ·) tacticCode
-            synthesizeSyntheticMVars (postpone := .no)
+            -- Pending tactic mvars may escape from `evalTactic` to here (#4436), so make sure
+            -- incrementality is disabled so they cannot be confused for top-level tactic blocks
+            withoutTacticIncrementality true do
+              synthesizeSyntheticMVars (postpone := .no)
           unless remainingGoals.isEmpty do
             if report then
               reportUnsolvedGoals remainingGoals
diff --git a/tests/lean/interactive/incrementalTactic.lean b/tests/lean/interactive/incrementalTactic.lean
index 25aa68e46e..a1783204ff 100644
--- a/tests/lean/interactive/incrementalTactic.lean
+++ b/tests/lean/interactive/incrementalTactic.lean
@@ -71,3 +71,12 @@ def dup_goals : True := by
 --^ goals
 -- (note that request positions are computed relative to the original document, so the checks above
 -- will point at a `show` at run time)
+
+/-!
+A tactic mvar may sometimes escape the term elaboration it was created from and should not break
+incremental reporting in this case.
+-/
+-- RESET
+def tacInTermInTac : True := by
+  · rw [show 0 = 0 by rfl]
+--^ collectDiagnostics
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index 9417b2fa17..1b64ca06ef 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -62,3 +62,15 @@ s
                isRemoved? := none,
                hyps := #[] }] }
 
+{"version": 1,
+ "uri": "file:///incrementalTactic.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 2, "character": 8}, "end": {"line": 2, "character": 25}},
+   "message":
+   "tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n  0\n⊢ True",
+   "fullRange":
+   {"start": {"line": 2, "character": 8},
+    "end": {"line": 2, "character": 25}}}]}