feat: hint alternatives when field-projecting from an unknown type

[robsimmons]

This PR gives suggestions based on the currently-available constants when projecting from an unknown type.

Example: single suggestion in namespace

This was the originally motivating example, as the string refactor led to a number of anonymous-lambda-expressions with Char functions that were no longer recognized as such.

example := (·.isWhitespace)

Before:

Invalid field notation: Type of
  x✝
is not known; cannot resolve field `isWhitespace`

The message is unchanged, but this PR adds a hint:

Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.

Example: single suggestion in namespace

example := fun n => n.succ

Before:

Invalid field notation: Type of
  n
is not known; cannot resolve field `succ`

The message is unchanged, but this PR adds a hint:

Hint: Consider replacing the field projection with a call to one of the following:
  • `Fin.succ`
  • `Nat.succ`
  • `Std.PRange.succ`

[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 edcef51434804e6432c02f42ef364cb13f9149b2 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-02 19:52:57)

[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 edcef51434804e6432c02f42ef364cb13f9149b2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-02 19:52:58)