parser interprets unindented list literal as part of indented tactic block

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

This example fails to parse:

example : List Nat :=
  have : 1 = 1 := by
    simp
  [] -- unexpected end of input; expected ';' or line break

Lean seems to interpret the list literal as belonging to simp (also works with grind).

Symptomatics:

• When using simp [], the error disappears.
• The error message is not captured by #guard_msgs in, but perhaps that is because the parser isn't able to recover and doesn't even return a partial parsing result.

Expected behavior:

No error. [] should be interpreted as a list literal.

Actual behavior:

Error as shown.

Versions

Lean 4.30.0-nightly-2026-03-04
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the minimal example in the issue with the Lean nightly environment at live.lean-lang.org, then inspect the parser behavior around the indented tactic block and following [] literal. Done means the example parses without an error and [] is treated as the list literal rather than as part of simp or grind.