fix: hovers on binders with metavariables

[nomeata]

this fixes #4078

[nomeata]

Mostly as a learning experience, I wanted to be see if I can fix a bug this part of the code based. I wonder if this is really the right fix, because I don’t see much withSaveInfoContext in this module, so happy to be educated! @kmill maybe?

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4137 has successfully built against this PR. (2024-05-11 17:47:57) View Log
• ✅ Mathlib branch lean-pr-testing-4137 has successfully built against this PR. (2024-05-11 18:56:12) View Log