refactor: use Shrink stub in the iterator framework

[datokrat]

This PR introduces a no-op version of Shrink, a type that should allow shrinking small types into smaller universes given a proof that the type is small enough, and uses it in the iterator library. Because this type would require special compiler support, the current version is just a wrapper around the inner type so that the wrapper is equivalent, but not definitionally equivalent.

While Shrink is unable to shrink universes right now, but introducing it now will allow us to generalize the universes in the iterator library with fewer breaking changes as soon as an actual Shrink is possible.

[datokrat]

!bench

[leanprover-radar]

Benchmark results for 1d641f2 against 71ddf22 are in! @datokrat

[leanprover-bot]

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

[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 71ddf227d2effc7725bf20e655a806a461e26cfe --onto c32a57e5806476ed6bac4c9cf1bb11cea2b02ea2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-09 14:35:46)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 71ddf227d2effc7725bf20e655a806a461e26cfe --onto 705dac4f77aa60d749ee2b37d102518d772d6e53. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-10 19:19:05)
• 💥 Mathlib branch lean-pr-testing-10725 build failed against this PR. (2025-10-13 08:58:15) View Log
• ✅ Mathlib branch lean-pr-testing-10725 has successfully built against this PR. (2025-10-13 16:08:13) View Log

[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 71ddf227d2effc7725bf20e655a806a461e26cfe --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-09 14:35:48)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-12 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-13 08:30:37)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-13 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-13 15:01:34)

[datokrat]

!bench

[leanprover-radar]

Benchmark results for 96c2e15 against 71ddf22 are in! @datokrat

[leanprover-bot]

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

[datokrat]

!bench

[leanprover-radar]

Benchmark results for 96c2e15 against 71ddf22 are in! @datokrat

[leanprover-bot]

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

[datokrat]

!radar

[leanprover-radar]

Benchmark results for a10cbef against 71ddf22 are in! @datokrat

[datokrat]

!radar

[leanprover-radar]

Benchmark results for df636df against 71ddf22 are in! @datokrat