fix: add mem_eraseDups lemma for List deduplication

[NicolasRouquette]

This PR proves that membership is preserved by eraseDups: an element exists in the deduplicated list iff it was in the original.

Includes a helper lemma for the loop invariant of eraseDupsBy.loop to establish the relationship between membership in the result, remaining list, and accumulator.

The proof changed compared to the proposal discussed on Zulip: https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Where.20should.20List.2Emem_eraseDup.20and.20List.2Emem_eraseDups.20l.2E.2E.2E

Specifically, I could not apply @Rob23oba 's short proof suggestion because it is located in src/Init/Data, a context where the grind strategy is not yet available.

In the Zulip thread, there is a discussion about the similarities/differences between Lean's List.eraseDups and Batteries' List.eraseDup; whether it makes sense to keep both (perhaps with a suitable renaming of Batterie's definition) or deprecate one (if any, it would be Batteries' since it is currently unused whereas Lean's is used across the board in Lean, Batteries, and Mathlib). See the Batteries PR: leanprover-community/batteries#1580

changelog-library

Closes #11786

[NicolasRouquette]

@digama0 Could you please add an appropriate changelog label (e.g., changelog-feature or changelog-fix) to this PR? The CI is failing because the PR title starts with "fix:" but no changelog label is present.

[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 f483c6c10f6122657fe6ca5ca79708567b0d6686 --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-27 06:53:24)

[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 f483c6c10f6122657fe6ca5ca79708567b0d6686 --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force reference manual CI using the force-manual-ci label. (2025-12-27 06:53:25)

[Rob23oba]

@NicolasRouquette you can add the label by posting a comment that only contains the name of the label you want to add (changelog-library in this case).

[NicolasRouquette]

changelog-library

[Rob23oba]

The "Check PR body..." check is also a bit bugged so you'll have to update it by e.g. editing the PR description back and forth.