diff --git a/src/Init/Lean/Elab/SyntheticMVars.lean b/src/Init/Lean/Elab/SyntheticMVars.lean
index 688baf4901..5f0e7f684e 100644
--- a/src/Init/Lean/Elab/SyntheticMVars.lean
+++ b/src/Init/Lean/Elab/SyntheticMVars.lean
@@ -211,6 +211,18 @@ private partial def synthesizeSyntheticMVarsAux (mayPostpone := true) : Unit →
 def synthesizeSyntheticMVars (mayPostpone := true) : TermElabM Unit :=
 synthesizeSyntheticMVarsAux mayPostpone ()
 
+/-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
+def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
+s ← get;
+let syntheticMVars := s.syntheticMVars;
+modify $ fun s => { syntheticMVars := [], .. s };
+finally
+  (do
+     v ← elabTerm stx expectedType?;
+     synthesizeSyntheticMVars false;
+     instantiateMVars stx v)
+  (modify $ fun s => { syntheticMVars := s.syntheticMVars ++ syntheticMVars, .. s })
+
 end Term
 end Elab
 end Lean