diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index d851971323..c76db8e9dc 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1451,6 +1451,9 @@ partial def doSeqToCode : List Syntax → M CodeBlock
       mkSeq doElem <$> doSeqToCode doElems
     else if k == `Lean.Parser.Term.doAssert then
       mkSeq doElem <$> doSeqToCode doElems
+    else if k == `Lean.Parser.Term.doNested then
+      let nestedDoSeq := doElem[1]
+      doSeqToCode (getDoSeqElems nestedDoSeq ++ doElems)
     else if k == `Lean.Parser.Term.doExpr then
       let term := doElem[0]
       if doElems.isEmpty then
diff --git a/tests/lean/run/nestedDo.lean b/tests/lean/run/nestedDo.lean
new file mode 100644
index 0000000000..e4a2b66949
--- /dev/null
+++ b/tests/lean/run/nestedDo.lean
@@ -0,0 +1,11 @@
+#lang lean4
+
+def f (x : Nat) : StateM Nat Nat := do
+let y ← do
+  modify (·+1)
+  let s ← get
+  pure $ s + x
+pure $ y + 1
+
+theorem ex1 : (f 5).run' 2 = 9 :=
+rfl