fix: lemma selection improvements to to rw? and lazy discriminator tree

[joehendrix]

This makes several changes to rw? and lazy discrimination trees based on test failures in rewrite search.

Changes include:

1. Reverting to Mathlib function for candidate lemma priority in rw?
2. Introducing additional filters for auto-generated named in lazy discriminator tree.
3. Refactoring lazy discriminator values to clarify what is stored.
4. Including star keys in calculation of match closeness in prioritization.
5. Using more fields in current core context when initializing lazy discriminator tree and avoiding max heartbeat issues.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-26 09:22:36) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-26 10:16:14) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-26 10:36:57) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-26 11:02:17) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-26 18:54:04) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but linting failed. (2024-03-26 20:29:13) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-26 22:20:58) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-27 00:32:28) View Log
• ❌ Mathlib branch lean-pr-testing-3769 built against this PR, but testing failed. (2024-03-27 01:06:16) View Log