feat: add HashMap.get*_filter* lemmas specialized for LawfulBEq

[kim-em]

This PR adds variants of HashMap.getElem?_filter that assume LawfulBEq and have a simpler right-hand-side. simp can already achieve these, via rewriting with getKey_eq under the lambda. However grind can not, and these lemmas help grind work with HashMap goals. There are variants for all variants of HashMap, getElem?/getElem/getElem!/getD, and for filter and filterMap.

[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 e7b8df0c0e1e2104c9f65057348c21ad7e240889 --onto c8290bd94221f41ae49899f0f7de71b52724ad7e. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-19 03:00:05)