[Merged by Bors] - chore: change the definition of List.finRange

[kim-em]

François Dorais has been working on upstreaming List.finRange, but wants to change the definition at the same time. That was running into difficulties, which hopefully are resolved here.

[github-actions]

PR summary c25fea8a05

Import changes exceeding 2%

%	File
+2.61%	Mathlib.Data.List.Sublists

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.List.Range	339	287	-52 (-15.34%)
Mathlib.Data.List.Sublists	345	354	+9 (+2.61%)
Mathlib.Data.List.FinRange	351	348	-3 (-0.85%)

Import changes for all files

Files	Import difference
Mathlib.Data.List.Range	-52
Mathlib.Data.List.FinRange	-3
Mathlib.Data.Finset.Powerset	5
Mathlib.Algebra.BigOperators.Ring.Multiset	8
3 files Mathlib.Data.Multiset.Antidiagonal Mathlib.Data.List.Sublists Mathlib.Data.Multiset.Powerset	9

---

Declarations diff

+ finRange_eq_pmap_range

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.01)

Current number	Change	Type
184	1	adaptation notes

Current commit c25fea8a05
Reference commit b96544419e

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Does this apply globally, or just for the current file?

[eric-wieser]

I also worry that this PR might have accumulated a bunch of proof uglification before we discovered this fix; is that the case, or do I have the chronology wrong?

[kim-em]

The uglification seems to still be necessary at the moment, and I'm not really sure why it is happening. It is only at the level of having to redo some simp only blocks, however.

[kim-em]

Does this apply globally, or just for the current file?

This is global.

[jcommelin]

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

[mathlib-bors]

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style