feat: verify partition for hashmaps

[jt0202]

This PR verifies the partition function for hashmaps.

[jt0202]

The approach here is to reuse the lemmas of the filter results as shown here for two example. This hinges on two lemmas I cant prove right now, but I am pretty sure they should hold. Please ignore the style violations for now; I will fix the unsqueezed simps and long lines later. Suggestions for name are appreciated though.

[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 51b67385cc0cd2613764ee4607957fef1f06128b --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-25 23:27:26)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 54fbe931ab77351ccba28aa7c03f22c717ba0681 --onto 0173444d24df9253d7947cfe82519e4a6caffd3a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 08:27:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 54fbe931ab77351ccba28aa7c03f22c717ba0681 --onto dd28f005889dd2fcca6fe0638133de561a655ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 22:05:37)

[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 51b67385cc0cd2613764ee4607957fef1f06128b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-25 23:27:28)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 54fbe931ab77351ccba28aa7c03f22c717ba0681 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-04 08:27:59)

[jt0202]

Open question: Do we want to provide all lemmas for both results of partitions as seen here or just provide the equiv results and let the user build it themselves?

[jt0202]

awaiting-review

[jt0202]

changelog-library