feat: suggestions for ambiguous dotted identifiers

[robsimmons]

This PR scans the environment for viable replacements for a dotted identifier (like .zero) and suggests concrete alternatives as replacements.

Example

#example .zero

Error message:

Invalid dotted identifier notation: The expected type of `.cons` could not be determined

Additional hint added by this PR:

Hint: Using one of these would be unambiguous:
  [apply] `BitVec.cons`
  [apply] `List.cons`
  [apply] `List.Lex.cons`
  [apply] `List.Pairwise.cons`
  [apply] `List.Perm.cons`
  [apply] `List.Sublist.cons`
  [apply] `List.Lex.below.cons`
  [apply] `List.Pairwise.below.cons`
  [apply] `List.Perm.below.cons`
  [apply] `List.Sublist.below.cons`
  [apply] `Lean.Grind.AC.Seq.cons`

Additional changes

This PR also brings several related error message descriptions and code actions more in line with each other, changing several "Suggested replacement: " code actions to the more common "Change to " wording, and sorts suggestions obtained from searching the context by the default sort for Names (which prefers names with fewer segments).

[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 3c100ada2a8bb3fb207232effa37099502b393d8 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 21:34:08)

[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 3c100ada2a8bb3fb207232effa37099502b393d8 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-08 21:34:10)