refactor: Lighten finiteness dependencies

[YaelDillies]

---

• depends on: [Merged by Bors] - chore: Make Finset.preimage not depend on Finset.sum #11601
• depends on: [Merged by Bors] - chore(Data/List/GetD): Use Std lemmas #11653
• depends on: [Merged by Bors] - feat(Polynomial): When the trailing degree is zero #11655
• depends on: [Merged by Bors] - chore(Data/Nat): Use Std lemmas #11661
• depends on: [Merged by Bors] - chore(Data/List/Join): Delete deprecated lemmas #11665
• depends on: [Merged by Bors] - chore(Data/List): Use Std lemmas #11711
• depends on: [Merged by Bors] - chore(Data/Nat/Factorial): Use Std lemmas #11715
• depends on: [Merged by Bors] - chore: Reduce scope of LinearOrderedCommGroupWithZero #11716
• depends on: [Merged by Bors] - chore(Algebra/BigOperators/List): Use Std lemmas #11725
• depends on: [Merged by Bors] - move(Data/List/BigOperators): Move to Algebra.BigOperators.List #11729
• depends on: [Merged by Bors] - chore(Data/Finset/Basic): Depend on less order theory #11732
• depends on: [Merged by Bors] - chore(Data/List): Depend less on big operators #11741
• depends on: [Merged by Bors] - chore: Sort big operator order lemmas #11750
• depends on: [Merged by Bors] - chore(Data/List): Do not depend on algebra #11845
• depends on: [Merged by Bors] - chore(Data/Nat/Defs): Integrate Nat.sqrt material #11866
• depends on: [Merged by Bors] - chore: Split Data.{Nat,Int}{.Order}.Basic in group vs ring instances #11924

[ghost]

This PR/issue depends on:

• [Merged by Bors] - chore: Make Finset.preimage not depend on Finset.sum #11601
• [Merged by Bors] - chore(Data/List/GetD): Use Std lemmas #11653
• [Merged by Bors] - feat(Polynomial): When the trailing degree is zero #11655
• [Merged by Bors] - chore(Data/Nat): Use Std lemmas #11661
• [Merged by Bors] - chore(Data/List/Join): Delete deprecated lemmas #11665
• [Merged by Bors] - chore(Data/List): Use Std lemmas #11711
• [Merged by Bors] - chore(Data/Nat/Factorial): Use Std lemmas #11715
• [Merged by Bors] - chore: Reduce scope of LinearOrderedCommGroupWithZero #11716
• [Merged by Bors] - chore(Algebra/BigOperators/List): Use Std lemmas #11725
• [Merged by Bors] - move(Data/List/BigOperators): Move to Algebra.BigOperators.List #11729
• [Merged by Bors] - chore(Data/Finset/Basic): Depend on less order theory #11732
• [Merged by Bors] - chore(Data/List): Depend less on big operators #11741
• [Merged by Bors] - chore: Sort big operator order lemmas #11750
• [Merged by Bors] - chore(Data/List): Do not depend on algebra #11845
• [Merged by Bors] - chore(Data/Nat/Defs): Integrate Nat.sqrt material #11866
• [Merged by Bors] - chore: Split Data.{Nat,Int}{.Order}.Basic in group vs ring instances #11924
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary 2e421d64e7

Import changes exceeding 2%

%	File
+7.74%	Mathlib.Computability.Primrec
+6.34%	Mathlib.Data.Fintype.Card
+2.06%	Mathlib.Data.Nat.Factorial.DoubleFactorial
+8.46%	Mathlib.Dynamics.BirkhoffSum.Basic
+15.18%	Mathlib.Logic.Denumerable
+3.26%	Mathlib.Order.PartialSups
+3.31%	Mathlib.Order.RelSeries
+2.99%	Mathlib.Order.SupIndep
+22.36%	Mathlib.Tactic.NormNum.BigOperators

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.NormNum.BigOperators	550	673	+123 (+22.36%)
Mathlib.Algebra.BigOperators.Intervals	674	557	-117 (-17.36%)
Mathlib.Logic.Denumerable	448	516	+68 (+15.18%)
Mathlib.Dynamics.BirkhoffSum.Basic	520	564	+44 (+8.46%)
Mathlib.Order.SuccPred.LinearLocallyFinite	567	520	-47 (-8.29%)
Mathlib.Computability.Primrec	530	571	+41 (+7.74%)
Mathlib.Data.Fintype.Card	426	453	+27 (+6.34%)
Mathlib.Order.RelSeries	513	530	+17 (+3.31%)
Mathlib.Order.PartialSups	491	507	+16 (+3.26%)
Mathlib.Order.SupIndep	469	483	+14 (+2.99%)
Mathlib.Data.Int.Interval	557	542	-15 (-2.69%)
Mathlib.Data.Nat.Factorial.DoubleFactorial	630	643	+13 (+2.06%)
Mathlib.Data.Finset.NatAntidiagonal	501	511	+10 (+2.00%)
Mathlib.Combinatorics.Young.YoungDiagram	501	510	+9 (+1.80%)
Mathlib.Analysis.Normed.Group.Basic	948	931	-17 (-1.79%)
Mathlib.Data.List.ToFinsupp	509	517	+8 (+1.57%)
Mathlib.Data.Multiset.Fintype	514	520	+6 (+1.17%)
Mathlib.Data.Holor	566	572	+6 (+1.06%)
Mathlib.Data.Nat.Factorial.BigOperators	656	662	+6 (+0.91%)
Mathlib.Combinatorics.Derangements.Finite	675	681	+6 (+0.89%)
Mathlib.Data.Sign	590	595	+5 (+0.85%)
Mathlib.Data.Rat.Denumerable	632	637	+5 (+0.79%)
Mathlib.RingTheory.Coprime.Lemmas	635	640	+5 (+0.79%)
Mathlib.GroupTheory.Perm.Sign	650	655	+5 (+0.77%)
Mathlib.Data.Matrix.Basic	806	800	-6 (-0.74%)
Mathlib.Topology.Algebra.InfiniteSum.NatInt	960	967	+7 (+0.73%)
Mathlib.Order.Interval.Finset.Basic	501	503	+2 (+0.40%)
Mathlib.Order.Interval.Finset.Nat	503	505	+2 (+0.40%)
Mathlib.Algebra.BigOperators.Fin	565	567	+2 (+0.35%)
Mathlib.Combinatorics.SetFamily.LYM	664	666	+2 (+0.30%)
Mathlib.Combinatorics.Enumerative.Catalan	709	711	+2 (+0.28%)
Mathlib.Data.Finset.Image	410	409	-1 (-0.24%)
Mathlib.Data.Finset.Card	411	410	-1 (-0.24%)
Mathlib.Data.Sym.Sym2	441	440	-1 (-0.23%)
Mathlib.Data.Finset.Lattice	443	442	-1 (-0.23%)
Mathlib.Data.Finset.Powerset	449	448	-1 (-0.22%)
Mathlib.Data.Set.Finite	488	487	-1 (-0.20%)
Mathlib.LinearAlgebra.Matrix.Transvection	978	980	+2 (+0.20%)
Mathlib.Order.Interval.Set.Infinite	489	488	-1 (-0.20%)
Mathlib.Algebra.BigOperators.Group.Finset	513	512	-1 (-0.19%)
Mathlib.Data.Fintype.BigOperators	517	516	-1 (-0.19%)
Mathlib.RingTheory.Prime	536	537	+1 (+0.19%)
Mathlib.Algebra.BigOperators.Ring	550	549	-1 (-0.18%)
Mathlib.Order.Category.NonemptyFinLinOrd	626	625	-1 (-0.16%)
Mathlib.Data.Finite.Card	727	728	+1 (+0.14%)
Mathlib.Algebra.Polynomial.Degree.TrailingDegree	864	863	-1 (-0.12%)
Mathlib.Topology.Algebra.Order.LiminfLimsup	906	905	-1 (-0.11%)
Mathlib.Algebra.MvPolynomial.Degrees	936	935	-1 (-0.11%)
Mathlib.AlgebraicTopology.AlternatingFaceMapComplex	978	979	+1 (+0.10%)
Mathlib.RingTheory.ChainOfDivisors	1065	1064	-1 (-0.09%)

Import changes for all files

Files	Import difference
There are 3377 files with changed transitive imports taking up over 145670 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ List.toFinset_range
+ Multiset.sup_powersetCard
+ Multiset.toFinset_range
+ Nat.instInfinite
+ eventually_constant_prod
+ piFinsetUnion
+ prod_fin_eq_prod_range
+ prod_range_add
+ prod_range_add_div_prod_range
+ prod_range_one
+ prod_range_succ
+ prod_range_succ'
+ prod_range_succ_comm
+ prod_range_zero
+ sum_range_succ_mul_sum_range_succ
+ union
+ union_symm_inl
+ union_symm_inr
- Finset.prod_fin_eq_prod_range
- instance : Infinite ℕ
- ⟨_,

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.

[YaelDillies]

The main goal of this PR, namely to rid basic Finset API of algebra imports, has been achieved. There are stil some interesting ideas in this PR that could be worth exploring in a new unrotted PR:

• Delaying defining Finset.range/merge it with Finset.Iio.
• Strategically relocating lemmas about Fin-indexed big operators