feat: Std.HashMap

[TwoFX]

Preliminary PRs:

• [x] #4597
• [x] #4599
• [x] #4600
• [x] #4602
• [x] #4603
• [x] #4604
• [x] #4605
• [ ] #4607
• [ ] #4627
• [x] #4629

Quick overview over API/naming changes compared to Lean.HashMap and Batteries.HashMap:

Lean

• find? -> get?/getElem?
• find! -> get!/gtetElem!
• findD -> getD
• findEntry? -> not implemented for now
• insert' -> containsThenInsert (order reversed in result)
• insertIfNew -> getThenInsertIfNew? (order reversed in result)
• numBuckets -> Internal.numBuckets
• ofListWith -> not implemented for now
• Array.groupByKey -> not implemented for now
• merge -> not implemented for now

Batteries

• modify -> not implemented for now
• mergeWith/mergeWithM -> not implemented for now

[kim-em]

Some functions don't have any theorems (e.g. toList, insertMany, ofList). This is of course fine, but we should document this somewhere. Perhaps I would suggest collecting their definitions together and putting them under a /-! ... -/ comment explaining that they don't have theorems at this point.

[leanprover-community-mathlib4-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 d4e141e233f2e54e731a2b763fbf74acf6c5d4dc --onto 62c5bc5d0dd0538731ddc172b75da51b7f645547. (2024-07-04 06:54:39)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-05 07:47:21)

[TwoFX]

@david-christiansen Thank you very much for the detailed review! I'll give you a chance to confirm that all of your comments have been addressed and then I think it's time to get this merged.

[david-christiansen]

This is great, thanks!