feat: elaboration with empty tactic sequences

[kmill]

This PR changes the parsing of empty tactic sequences so that they report a parse error but still elaborate. For example, in

example (as bs : List Nat) : (as.append bs).length = as.length + bs.length := by
  induction as
  case nil =>
  case cons b bs ih =>

there are parse errors after each => for not having complete tactic sequences, but both show the tactic state for that particular case. The syntaxes for many tactics have also been changed to require that the tactic sequence be strictly indented. The motivation for this is that, without strict indentation, the above example would parse with the second case nested under the first one. The induction and cases tactics were modified in #7830 in anticipation of this change; one can write induction p with | _ x y without the => if the succeeding tactics stay at the same indentation level.

Implementation note: The orelse parser needed some additional logic to handle error recovery. Recall that in p <|> q, if p parses an antiquotation, then q is tentatively parsed as well to see if it parses a longer antiquotation. Now, if q does error recovery and p parses an antiquotation, p is preferred.

Todo: add else if to the if tactic.

This works toward issue #3555. This PR is an experiment to see if having parse errors is more useful than distracting, given that they do not keep the tactic proof from elaborating.

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bdd1918cd81c9a09e1b2005af5f3d934e812b8d5 --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-27 14:45:02)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bdd1918cd81c9a09e1b2005af5f3d934e812b8d5 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-27 14:45:04)