ExtTreeMapLemmas dependency

[alexanderlhicks]

Raising this issue to discuss merging lemmas from https://github.com/NethermindEth/ExtTreeMapLemmas that this repository depends on into this repository to make maintenance easier as ExtTreeMapLemmas.DTreeMap currently causes a build error if one tries to update the version of Lean for this repository.

✖ [592/3119] Building ExtTreeMapLemmas.DTreeMap
trace: .> LEAN_PATH=/home/alh/CompPoly/.lake/packages/Cli/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/batteries/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/Qq/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/aesop/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/importGraph/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/plausible/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/mathlib/.lake/build/lib/lean:/home/alh/CompPoly/.lake/packages/ExtTreeMapLemmas/.lake/build/lib/lean:/home/alh/CompPoly/.lake/build/lib/lean /home/alh/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /home/alh/CompPoly/.lake/packages/ExtTreeMapLemmas/ExtTreeMapLemmas/DTreeMap.lean -o /home/alh/CompPoly/.lake/packages/ExtTreeMapLemmas/.lake/build/lib/lean/ExtTreeMapLemmas/DTreeMap.olean -i /home/alh/CompPoly/.lake/packages/ExtTreeMapLemmas/.lake/build/lib/lean/ExtTreeMapLemmas/DTreeMap.ilean -c /home/alh/CompPoly/.lake/packages/ExtTreeMapLemmas/.lake/build/ir/ExtTreeMapLemmas/DTreeMap.c --setup /home/alh/CompPoly/.lake/packages/ExtTreeMapLemmas/.lake/build/ir/ExtTreeMapLemmas/DTreeMap.setup.json --json

cc @Ferinko @Julek

[alexanderlhicks]

Note: intention is to merge ExtTreeMapLemmas into batteries, will just have to be maintained independently in the meantime.
Closing the issue for now as a result.

[dhsorens]

Current status: ExtTreeMapLemmas has some name clashes with new std so won't yet update. See a relevant pull request

I will investigate this in the next day or two, see the extend of the dependency and if we can just use the new lemmas in std that name clash with what's in ExtTreeMapLemmas.

[dhsorens]

The solution (done in #46 ) was to fork this repository and change the lemmas with name clashes. Further TODOs on ExtTreeMapLemmas is to see how much can be upstreamed, and how much can be incorporated elsewhere, hopefully to remove the need for this dependency.

Closing for now as the issue is temporarily resolved.