refactor(data/set/finite): reduce imports (#18245)
* Add `eq_or_eq_or_eq_of_forall_not_lt_lt`, `finite.of_forall_not_lt_lt`, `set.finite_of_forall_not_lt_lt` (replacing `set.finite_of_forall_between_eq_endpoints`), and `set.finite_of_forall_not_lt_lt'`.
* Import `data.finset.basic` instead of `data.finset.sort` in `data.set.finite`.
* Forward-ported in leanprover-community/mathlib4#1738
