feat: library suggestion engine for local theorems

[kim-em]

This PR adds a library suggestion engine for local theorems. To be useful, I still need to write more combinators to re-rank and combine suggestions from multiple engines.

This is stacked on top of #11029.

[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 40e1e097c171a6ef1addb607446950e10eedbb9d --onto 705084d9ba258dec704af428d7ce2444525f9ffb. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-31 03:39:45)

[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 40e1e097c171a6ef1addb607446950e10eedbb9d --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-31 03:39:46)