refactor: replace PRange shape α with Rcc α and eight other types

[datokrat]

This PR "monomorphizes" the structure Std.PRange shape α, replacing it with nine distinct structures Std.Rcc, Std.Rco, Std.Rci etc., one for each possible shape of a range's bounds. This change was necessary because the shape polymorphism is detrimental to attempts of automation.

BREAKING CHANGE: While range/slice notation itself is unchanged, this essentially breaks the entire remaining (polymorphic) range and slice API except for the dot-notation(toList, iter, ...). It is not possible to deprecate old declarations that were formulated in a shape-polymorphic way that is not available anymore.

[datokrat]

!bench

[leanprover-bot]

Here are the benchmark results for commit f4372ef.
There were significant changes against commit d0d5d4c:

  Benchmark                            Metric                      Change
  ==================================================================================
- Init size                            bytes .olean                  2.3%
- Init size                            bytes .olean.private          2.3%
- Init size                            bytes .olean.server           1.9%
- Init.Data.BitVec.Lemmas re-elab      maxrss                        1.1%   (47.2 σ)
- Init.Data.List.Sublist re-elab -j4   maxrss                        1.4%   (36.3 σ)
+ bv_decide_inequality.lean            wall-clock                   -3.5%  (-83.9 σ)
+ iterators (compiled)                 branches                     -8.7% (-774.9 σ)
+ iterators (compiled)                 instructions                 -9.1% (-597.1 σ)
+ iterators (elab)                     branch-misses                -3.1%  (-28.0 σ)
+ iterators (elab)                     branches                     -4.1% (-242.6 σ)
+ iterators (elab)                     instructions                 -4.1% (-199.9 σ)
+ iterators (interpreted)              branches                     -1.8% (-649.2 σ)
+ iterators (interpreted)              instructions                 -1.8% (-727.2 σ)
- lake build clean                     maxrss                        1.3%   (22.9 σ)
+ lake config elab                     instructions                 -1.9%  (-79.3 σ)
+ stdlib                               grind dsimp                  -7.6%  (-32.1 σ)
- stdlib                               number of imported bytes      1.2%
- stdlib                               number of imported consts     1.5%
- stdlib size                          lines                         1.1%
+ treemap.lean                         eraseInsert                  -4.0%  (-39.2 σ)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-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-09-23 16:18:09)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-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-01 13:08:15)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-10319 built against this PR, but testing failed. (2025-09-23 17:18:48) View Log
• 🟡 Mathlib branch lean-pr-testing-10319 build this PR didn't complete normally. (2025-09-24 08:37:13) View Log
• ❌ Mathlib branch lean-pr-testing-10319 built against this PR, but testing failed. (2025-09-24 08:49:55) View Log
• ❌ Mathlib branch lean-pr-testing-10319 built against this PR, but testing failed. (2025-09-24 10:16:32) View Log
• ✅ Mathlib branch lean-pr-testing-10319 has successfully built against this PR. (2025-09-24 12:44:19) View Log
• ✅ Mathlib branch lean-pr-testing-10319 has successfully built against this PR. (2025-09-24 17:47:07) View Log
• ✅ Mathlib branch lean-pr-testing-10319 has successfully built against this PR. (2025-09-24 20:54:16) View Log
• ✅ Mathlib branch lean-pr-testing-10319 has successfully built against this PR. (2025-10-01 14:05:31) View Log