chore(data/list/range): split & reduce imports (#17887)
This PR splits most of the lemmas about `list.fin_range` into a new file.
`list.fin_range` is much less useful than `list.range`, but we need to import `data.list.of_fn` for `list.fin_range`, and then `data.list.of_fn` imports `data.fin.tuple.basic` and `data.fin.tuple.basic` imports many things.
