Commit 2025-01-10 09:20 593e78d7

chore(Data/Set): split the CoeSort instance to its own file (#19031) 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: https://github.com/leanprover-community/mathlib4/pull/18619#discussion_r1841131715 Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Splitting.20docs.23Set.2EinstCoeSortType.20to.20its.20own.20file.3F