diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 85392b5d38..a81dd14afb 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1368,7 +1368,7 @@ mutual
     else
       pure doElems.toArray
     let contSeq := mkDoSeq contSeq
-    let auxDo ← `(do let __discr := $val; match __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+    let auxDo ← `(do match $val:term with | $pattern:term => $contSeq | _ => $elseSeq)
     doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
 
   /-- Generate `CodeBlock` for `doReassignArrow; doElems`
diff --git a/tests/lean/run/doLetElse.lean b/tests/lean/run/doLetElse.lean
index 24435474c1..e65b084f99 100644
--- a/tests/lean/run/doLetElse.lean
+++ b/tests/lean/run/doLetElse.lean
@@ -3,10 +3,22 @@ def foo (x? : Option Nat) : IO Nat := do
   IO.println s!"x: {x}"
   return x
 
-def test (input : Option Nat) (expected : Nat) : IO Unit := do
+def testFoo (input : Option Nat) (expected : Nat) : IO Unit := do
   assert! (← foo input) == expected
 
+#eval testFoo (some 10) 10
+#eval testFoo none 0
+#eval testFoo (some 1) 1
 
-#eval test (some 10) 10
-#eval test none 0
-#eval test (some 1) 1
+def bar (x : Nat) : IO (Fin (x + 1)) := do
+  let 2 := x | return 0
+  -- the pattern match performed a substitution
+  let y : Fin 3 := ⟨1, by decide⟩
+  return y
+
+def testBar (x : Nat) (expected : Fin (x + 1)) : IO Unit := do
+  assert! (← bar x) == expected
+
+#eval testBar 1 0
+#eval testBar 2 1
+#eval testBar 3 0