fix: do not introduced additional lets that block match generalization

Qq/Match.lean

@@ -257,14 +257,14 @@ macro_rules | `(assert! (_comefrom $n do $b); $body) => `(_comefrom $n do $b in
 scoped macro "comefrom" n:ident "do" b:doSeq : doElem =>
   `(doElem| assert! (_comefrom $n do $b))
 
-def mkLetDoSeqItem [Monad m] [MonadQuotation m] (pat : Term) (rhs : TSyntax `doElem) (alt : TSyntax ``doSeq) : m (List (TSyntax ``doSeqItem)) := do
+def mkLetDoSeqItem [Monad m] [MonadQuotation m] (pat : Term) (rhs : TSyntax `term) (alt : TSyntax ``doSeq) : m (List (TSyntax ``doSeqItem)) := do
   match pat with
     | `(_) => return []
     | _ =>
       if isIrrefutablePattern pat then
-        return [← `(doSeqItem| let $pat:term ← $rhs)]
+        return [← `(doSeqItem| let $pat:term := $rhs)]
       else
-        return [← `(doSeqItem| let $pat:term ← $rhs | $alt)]
+        return [← `(doSeqItem| let $pat:term := $rhs | $alt)]
 
 end Impl
 
@@ -335,11 +335,11 @@ private partial def floatExprAntiquot (depth : Nat) : Term → StateT (Array (TS
       | stx => return stx
 
 macro_rules
-  | `(doElem| let $pat:term ← $_) => do
+  | `(doElem| let $pat:term := $_) => do
     if !hasQMatch pat then Macro.throwUnsupported
     Macro.throwError "let-bindings with ~q(.) require an explicit alternative"
 
-  | `(doElem| let $pat:term ← $rhs:doElem | $alt:doSeq) => do
+  | `(doElem| let $pat:term := $rhs:term | $alt:doSeq) => do
     if !hasQMatch pat then Macro.throwUnsupported
     match pat with
       | `(~q($pat)) =>
@@ -351,7 +351,7 @@ macro_rules
               if id.getId.eraseMacroScopes == `pure then -- TODO: super hacky
                 return ← `(doSeqItem| assert! (_qq_match $pat ← $rhs | $alt))
             | _ => pure ()
-          `(doSeqItem| do let rhs ← $rhs; assert! (_qq_match $pat ← rhs | $alt)))
+          `(doSeqItem| do assert! (_qq_match $pat ← $rhs | $alt)))
 
         `(doElem| do $(lifts.push t):doSeqItem*)