mathlib

2b35fc7b - refactor(data/set/finite): reorganize and put emphasis on fintype instances (#14136)

refactor(data/set/finite): reorganize and put emphasis on fintype instances (#14136) I went through `data/set/finite` and reorganized it by rough topic (and moved some lemmas to their proper homes; closes #11177). Two important parts of this module are (1) `fintype` instances for various set constructions and (2) ways to create `set.finite` terms. This change puts the module closer to following a design where the `set.finite` terms are created in a formulaic way from the `fintype` instances. One tool for this is a `set.finite_of_fintype` constructor, which lets typeclass inference do most of the work. Included in this commit is changing `set.infinite` to be protected so that it does not conflict with `infinite`.