feat: simp? +suggestions

[kim-em]

This PR implements simp? +suggestions, which uses the configured library suggestion engine to add relevant theorems to the simp call. simp +suggestions without the ? prints a message requiring adding the ?.

[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 0db89d65b27b56ea911add501cf041dfc44976a1 --onto 1ce05b2a179eac8a902995c0caddc609c0169c49. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-03 01:36:22)

[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 0db89d65b27b56ea911add501cf041dfc44976a1 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-03 01:36:23)