fix: some goal state issues

[mhuisi]

This PR resolves the following issues related to goal state display:

1. In a new line after a case tactic with a completed proof, the state of the proof in the case would be displayed, not the proof state after the case
2. In the range of next => / case' ... =>, the state of the proof in the corresponding case would not be displayed, whereas this is true for case
3. In the suffices ... by tactic, the tactic state of the by block was not displayed after the by and before the first tactic

The incorrect goal state after case was caused by evalCase adding a TacticInfo with the full block proof state for the full range of the case block that the goal state selection has no means of distinguishing from the TacticInfo with the same range that contains the state after the whole case block. Narrowing the range of this TacticInfo to case ... => fixed this issue.

The lack of a case proof state on next => was caused by the case syntax that next expands to receiving noncanonical synthetic SourceInfo, which is usually ignored by the language server. Adding a token antiquotation for next fixed this issue.

The lack of a case proof state on case' ... => was caused by evalCase' not adding a TacticInfo with the full block state to the range of case' ... =>. Adding this TacticInfo fixed this issue.

The tactic state of the block not being displayed after the by was caused by the macro expansion of suffices to have not transferring the trailing whitespace of the by. Ensuring that this trailing whitespace information is transferred fixed this issue.

Fixes #2881.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3930100b67d2dd14a62412432f8822b29a9900af --onto d10d41bc07942ca6d8f3081a637045321db15c5a. (2024-10-11 15:11:41)
• ✅ Mathlib branch lean-pr-testing-5677 has successfully built against this PR. (2024-10-11 16:39:41) View Log