fix: unknown identifier ranges

[mhuisi]

This PR fixes a bug where the unknown identifier code actions wouldn't work correctly for some unknown identifier error spans and adjusts several unknown identifier spans to actually end on the identifier in question.

The following additional adjustments are made:

• The fallback mechanism of the unknown identifier code actions is removed, since it could produce severely incorrect suggestions for unknown identifier errors on fields.
• A performance bug when using the code action to import all unknown identifiers is fixed.
• A bug that occurs when the elaborator produces multiple overlapping completion infos is fixed.
• A bug in the snapshot selection that could cause it to wait for snapshots in snapshots with non-canonical syntax is fixed.
• Some invariants of the snapshot tree are documented.
• The snapshot tree formatting is adjusted to display the final info tree again.

[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 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto 6ca31baa55e4b29c9667085736863f9ca840b16c. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-15 15:28:16)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto ca9b3eb75f3f794d3d526a7c37da389175b317a2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-16 14:57:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto c8290bd94221f41ae49899f0f7de71b52724ad7e. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-19 10:25:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto efe2ab4c04e81fe2a3edcc0d861449490b4431b2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-20 13:33:33)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto 47a1355fc43b29421cfb02047445888bbb414441. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-22 10:24:51)