feat: verify toList for hash maps

[jt0202]

This PR verifies the toListfunction for hash maps and dependent hash maps.

[jt0202]

This is currently WIP. If you think further lemmas are useful let me know. One lemma is currently unproven, because there are some problems with casting. As with previous PRs I will first only work in Internal/RawLemmas.lean.

[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 6d63f6305eee006f1acaddff2f36654c98ce5b5e --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-05 12:00:25)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6d63f6305eee006f1acaddff2f36654c98ce5b5e --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 11:50:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6d63f6305eee006f1acaddff2f36654c98ce5b5e --onto d61f506da254b919f93e571a84247319de78f526. (2025-02-10 20:03:26)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 80c8837f49ac95c03af15abdf2b350ad669d7d18 --onto ae9d12aeaa075578c7ee3a5a585d0f9fb89cedd2. (2025-02-13 18:30:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47548aa171f02cf0b61fc1eb6bcaee82bb50d060 --onto ae9d12aeaa075578c7ee3a5a585d0f9fb89cedd2. (2025-02-14 08:51:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47548aa171f02cf0b61fc1eb6bcaee82bb50d060 --onto f50b863868a3625dfbca4fd2ad777d187632b1d4. (2025-02-17 07:26:22)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47548aa171f02cf0b61fc1eb6bcaee82bb50d060 --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-17 18:43:42)

[TwoFX]

RawLemmas statements look good to me. Will take a look at the proofs in a bit.

[jt0202]

I am sorry, I wanted to rebase my PR to get rid of the merge conflict, but this somehow created all the extra review requests. How to fix this?

Shall I close this and open a new one and readd my contributions?

[TwoFX]

Since the PR is still a draft the review requests should go away again once you fix your branch to only contain the correct commits.

[TwoFX]

It's difficult to review while the GitHub diff view is confused so I'll wait until you repaired your git history, but I have one remark: the new results in AssoList/Lemmas.lean are not required, the required results are all there in WF.lean, see c605c16.

[jt0202]

It's difficult to review while the GitHub diff view is confused so I'll wait until you repaired your git history, but I have one remark: the new results in AssoList/Lemmas.lean are not required, the required results are all there in WF.lean, see c605c16.

Ok, I have repaired it and used your changes. Additionally, I dropped lemmas in WF.lean that are no longer necessary. Now I only have to try again to get rid of the merge conflict.

[jt0202]

changelog-library

[jt0202]

Interesting that "CI / Linux release (pull_request)" works again. Not sure what went wrong last time, seemed to be unconnected with my PR.

[TwoFX]

The List/Associative proofs can be shortened, see 9182483 for how to get started.

[jt0202]

awaiting-review

[TwoFX]

Could you add 5a21fa9 to your PR? It's a quick test that simp applies the right lemmas in lawful and non-lawful contexts.

[jt0202]

awaiting-review

[TwoFX]

Great work as always, thanks!