feat: lemmas about iterator collectors

[datokrat]

This PR provides simple lemmas about toArray, toList and toListRev for the iterator library.

It also changes the definition of Iter and IterM so that they aren't equal anymore and in particular not definitionally equal. While it was very convenient to have them be definitionally equal when working with dependent code, it was also confusing and annoying that one would sometimes end up with something like it.toList = IterM.toList it, where it : Iter β.

[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 60ea92fdb0594065072ed843724d98cd15b76fba --onto ca9b3eb75f3f794d3d526a7c37da389175b317a2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-16 14:30:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60ea92fdb0594065072ed843724d98cd15b76fba --onto efe2ab4c04e81fe2a3edcc0d861449490b4431b2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-20 07:51:08)
• ✅ Mathlib branch lean-pr-testing-8380 has successfully built against this PR. (2025-05-20 14:27:51) View Log