feat: extrinsic finiteness proofs for toList, toListRev and toArray on iterators

[datokrat]

This PR removes the Finite hypothesis on the toList, toListRev and toArray functions on iterators. The new default implementation uses a fixpoint combinator that is semantically equal to a well-founded recursive function or an opaque function depending on whether the functional is well-founded recursive w.r.t. any well-founded relation. The PR also adds it.ensureTermination.toList and other variants that require a Finite instance and always terminate, in case that one wants intrinsic guarantees that it terminates.

[datokrat]

!bench

[leanprover-radar]

Benchmark results for 840c675 against 746206c are in! @datokrat

[leanprover-bot]

Here are the benchmark results for commit 840c675.
The entire run failed.
Found no significant differences.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-10-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-15 10:45:18)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-10-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-21 10:44:26)
• 🟡 Mathlib branch lean-pr-testing-10785 build this PR didn't complete normally. (2025-10-22 21:18:12) View Log
• ✅ Mathlib branch lean-pr-testing-10785 has successfully built against this PR. (2025-10-23 14:59:06) View Log
• ✅ Mathlib branch lean-pr-testing-10785 has successfully built against this PR. (2025-10-31 16:16:39) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-15 10:45:19)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-21 10:44:27)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-31 15:12:58)

[datokrat]

!radar

[leanprover-radar]

Benchmark results for c3fe021 against 65315a6 are in! @datokrat

[datokrat]

!bench

[leanprover-radar]

Benchmark results for 7fd052b against 65315a6 are in! @datokrat

[leanprover-bot]

Here are the benchmark results for commit 7fd052b.Found no runs to compare against.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 6854540 against 65315a6 are in! @datokrat

[TwoFX]

I'm not really qualified to review this file, but you have discussed it a lot, so I'll trust your judgement that it's good.

[datokrat]

Closing in favor of #10863.