fix: isolate postponed in withSynthesize

src/Lean/Elab/SyntheticMVars.lean

@@ -660,16 +660,18 @@ def synthesizeSyntheticMVarsUsingDefault : TermElabM Unit := do
   synthesizeUsingDefaultLoop
 
 private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBehavior) : TermElabM α := do
-   let pendingMVarsSaved := (← get).pendingMVars
-   modify fun s => { s with pendingMVars := [] }
-   try
-     let a ← k
-     synthesizeSyntheticMVars (postpone := postpone)
-     if postpone == .yes then
-       synthesizeUsingDefaultLoop
-     return a
-   finally
-     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
+  let pendingMVarsSaved := (← get).pendingMVars
+  let postponedLevelUnifs ← getResetPostponed
+  modify fun s => { s with pendingMVars := [] }
+  try
+    let a ← k
+    synthesizeSyntheticMVars (postpone := postpone)
+    if postpone == .yes then
+      synthesizeUsingDefaultLoop
+    return a
+  finally
+    modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
+    modifyPostponed fun newPostponed => postponedLevelUnifs ++ newPostponed
 
 /--
   Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.

tests/elab/13875.lean

@@ -0,0 +1,8 @@
+/-!
+Regression test for https://github.com/leanprover/lean4/issues/13785.
+-/
+
+example (s : String) (x : Nat) : String :=
+  let := s.all (·.isAlphanum)
+  match x with
+  | _ => s