diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 758c25ffaf..cebd8e4c00 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -537,7 +537,7 @@ partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
      stx[0].getKind == ``Lean.Parser.Command.set_option then
       let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
       Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[1]
+        withSetOptionIn cmd stx[2]
   else
     cmd stx
 
diff --git a/tests/lean/withSetOptionIn.lean b/tests/lean/withSetOptionIn.lean
new file mode 100644
index 0000000000..8f34667133
--- /dev/null
+++ b/tests/lean/withSetOptionIn.lean
@@ -0,0 +1,39 @@
+import Lean
+
+/-!
+# `withSetOptionIn`
+
+This test checks that `withSetOptionIn` recurses into the command syntax (`stx[2]`) in
+`set_option ... in <cmd>`.
+
+Prior to #3806, `withSetOptionIn` erroneously recursed into the syntax `in` (`stx[1]`).
+-/
+
+open Lean Elab Command
+
+/-- Trace `foo` when `set_option trace.debug true`. -/
+elab "#trace_debug_foo" : command => do trace[debug] "foo"
+
+/-- Elab `cmd` using `withSetOptionIn`. -/
+elab "#test " cmd:command : command => withSetOptionIn elabCommand cmd
+
+/-! ## Controls
+
+Ensure that `#trace_debug_foo` works as expected.
+-/
+
+#guard_msgs in
+#trace_debug_foo
+
+/-- info: [debug] foo -/
+#guard_msgs in
+set_option trace.debug true in #trace_debug_foo
+
+/-! ## Test
+
+Should trace `[debug] foo`, and not log the error "unexpected command 'in'".
+-/
+
+/-- info: [debug] foo -/
+#guard_msgs in
+#test set_option trace.debug true in #trace_debug_foo
diff --git a/tests/lean/withSetOptionIn.lean.expected.out b/tests/lean/withSetOptionIn.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2