refactor: remove IteratorCollect

[datokrat]

This PR removes the IteratorCollect type class and hereby simplifies the iterator API. Its limited advantages did not justify the complexity cost.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 1783806 against e261790 are in! @datokrat

Minor changes (3)

• ✅ iterators (elab)//instructions: -20.8M (-0.5%)
• ✅ size/init/.olean.private//bytes: -521kiB (-0.2%)
• ✅ size/init/.olean//bytes: -224kiB (-0.2%)

[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 e2617903f81f2f9ffc6c0b7a06cc91678c546305 --onto 95a7c769d8d1565fdafd32553bb44d7d53edf5c3. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-17 08:15:24)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f21f8d96f97989d3a34148329a158e94b220314b --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-17 23:12: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 e2617903f81f2f9ffc6c0b7a06cc91678c546305 --onto 95a7c769d8d1565fdafd32553bb44d7d53edf5c3. You can force reference manual CI using the force-manual-ci label. (2025-12-17 08:15:26)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f21f8d96f97989d3a34148329a158e94b220314b --onto 0708024c4649f11da1276d8b6d4345972a9dc57c. You can force reference manual CI using the force-manual-ci label. (2025-12-17 23:12:25)

[robsimmons]

@datokrat can you spot check leanprover/reference-manual#715 when you get a chance in light of this?

[datokrat]

@robsimmons Looking good! Sorry for not leaving more breadcrumbs for how to solve the errors in the manual.