diff --git a/Qq/Match.lean b/Qq/Match.lean
index 8ae3267..78c871e 100644
--- a/Qq/Match.lean
+++ b/Qq/Match.lean
@@ -248,8 +248,8 @@ partial def isIrrefutablePattern : Term → Bool
 
 scoped elab "_comefrom" n:ident "do" b:doSeq " in " body:term : term <= expectedType => do
   let _ ← extractBind expectedType
-  (← elabTerm (← `(?m)).1.stripPos none).mvarId!.assign expectedType
-  elabTerm (← `(have $n:ident : ?m := (do $b:doSeq); $body)) expectedType
+  let ty ← exprToSyntax expectedType
+  elabTerm (← `(have $n:ident : $ty := (do $b:doSeq); $body)) expectedType
 
 scoped syntax "_comefrom" ident "do" doSeq : term
 macro_rules | `(assert! (_comefrom $n do $b); $body) => `(_comefrom $n do $b in $body)
diff --git a/lean-toolchain b/lean-toolchain
index f0a6d66..ccc4160 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4-pr-releases:pr-release-2973