fix: typo in withSetOptionIn (#3806)

When using `withSetOptionIn` on syntax `set_option ... in <command>`,
recurse into command syntax (`stx[2]`) instead of the syntax `in`
(`stx[1]`).

---

Demonstration of `stx[1]` vs. `stx[2]`:
```lean
import Lean

def stx := (Lean.Unhygienic.run `(set_option trace.debug true in #print foo)).raw

#eval stx[1] -- Lean.Syntax.atom (Lean.SourceInfo.none) "in"
#eval stx[2] -- `#print` command syntax
```

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
 

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