mathlib

a0504eb3 - refactor(data/*/interval): generalize `finset.Ico` to locally finite orders (#7987)

refactor(data/*/interval): generalize `finset.Ico` to locally finite orders (#7987) `finset.Ico` currently goes `ℕ → ℕ → finset ℕ`. This generalizes it to `α → α → finset α` where `locally_finite_order α`. This also ports all the existing `finset.Ico` lemmas to the new API, which involves renaming and moving them to `data.finset.interval` or `data.nat.interval` depending on whether I could generalize them away from `ℕ` or not. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>