chore(Data/Set): split the CoeSort instance to its own file

[Vierkantor]

Although Data.Set.Operations is somewhat light-weight, it still pulls in a few imports. In particular, if we want to move the definition of Set.Finite to Data.Finite.Defs, then Algebra.Group.Int will complain that it's not allowed to import Set.range from Data.Set.Operations; this split will allow us to do the move without removing an assert_not_exists.

See also this discussion on GitHub: #18619 (comment)
Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Splitting.20docs.23Set.2EinstCoeSortType.20to.20its.20own.20file.3F

---

[github-actions]

PR summary 1ba6b9979c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Types	303	299	-4 (-1.32%)

Import changes for all files

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

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

---

No changes to technical debt.

You can run this locally as

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

[YaelDillies]

I would to know other people's opinions on this. Can you start a discussion on Zulip?

[Vierkantor]

When #18619 gets merged, we can readd the assert_not_exists Set.range to Algebra/Group/Int.lean.