Splitting docs#Set.instCoeSortType to its own file?

Stream: mathlib4

[Anne Baanen]

I opened PR #19031 which moves docs#Set.instCoeSortType to its own file from Data.Set.Operations. This was needed in #18619 because there are a few files that import docs#Finite but have an assert_not_exists against importing docs#Set.range. For example, file#Mathlib/Algebra/Group/Int. @Yaël Dillies rightfully pointed out that Data.Set.Operations is already quite minimal, so it shouldn't need further splitting unless really well motivated.

What do we think? Should we split that file further, or remove the assert_not_exists

[Yuyang Zhao]

Is there any reason not to put it in Mathlib.Data.Set.Defs?