feat: HashMap.toList_map_fst

[kim-em]

This PR adds the lemma toList_map_fst : m.toList.map Sigma.fst = m.keys for m a (raw or standard) DHashMap, and the same theorem but with Prod.fst for (raw or standard) HashMap.

I'm not satisfied with how I've done this: in particular the proofs:

• toList_map_fst in DHashMap/Internal/RawLemmas should presumable be using simp_to_model, but I don't understand how to make that work
• toList_inner in HashMap/RawLemmas and HashMap/Lemmas is brute force. How can I avoid proving this twice? How am I meant to structure this?

[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 321e148f51eb507acd9bf870ba1a7d469d4ed3b1 --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-27 03:57:43)

[jt0202]

From my understanding you would have to do the following based on what is written in Internal.Defs

* `toList_map_fst` in `DHashMap/Internal/RawLemmas` should presumable be using `simp_to_model`, but I don't understand how to make that work

simp_to_model needs to know how m.1.keys and m.1.toList look on lists like length_keys_eq_length_keys in Internal.WF.
Probably like: m.keys = List.Keys (toListModel m)and m.toList = toListModel m
After proving that you would need to add them to queryNames in Internal.Raw and add (h: m.1.WF) to your theorem. Then you should be able to use simp_to_model.

* `toList_inner` in `HashMap/RawLemmas` and `HashMap/Lemmas` is brute force. How can I avoid proving this twice? How am I meant to structure this?

You have to prove the result for toList and const.toList in Raw0 and afterwards you use these results directly in all other classes.