set_option ... in after decreasing_by with focused · tactic causes parse error

set_option ... in (and presumably other command modifiers) after a decreasing_by block that uses focused · tactics causes a parse error. The parser seems to remain in tactic mode after the focused tactic.

MWE

-- Fails: "unexpected token 'def'; expected '{' or tactic"
def foo : Nat → Nat
  | 0 => 0
  | n + 1 => foo n
termination_by n => n
decreasing_by
· omega

set_option autoImplicit false in
def bar : Nat := 0

Works without ·

-- Works fine
def foo' : Nat → Nat
  | 0 => 0
  | n + 1 => foo' n
termination_by n => n
decreasing_by omega

set_option autoImplicit false in
def bar' : Nat := 0

Notes

• Also fails when the next declaration has a doc comment (/--): error becomes "unexpected token '/--'; expected '{' or tactic"
• Without set_option ... in, the next declaration parses fine (both with and without ·)
• Reproduces on v4.28.0-rc1 and pr-release-12564
• Discovered while adapting Mathlib for https://github.com/leanprover/lean4/pull/12564 (the set_option backward.isDefEq.respectTransparency false in workaround is needed frequently)

Workaround

Use non-focused tactics in the decreasing_by block, or avoid set_option ... in immediately after such blocks.

🤖 Prepared with Claude Code

Start by reproducing the MWE on v4.28.0-rc1 or pr-release-12564, comparing the focused and non-focused decreasing_by forms. Investigate the parser path for tactic blocks followed by set_option ... in, including the doc-comment variant. Done means both declarations parse successfully without requiring the documented workaround.