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

[leanprover-community-mathlib4-bot]

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!