refactor(data/finset/fin): Delete `finset.fin_range`

[YaelDillies]

finset.fin_range n is just finset.univ, so we inline its definition in the fintype (fin n) instance to avoid people trying to use it.

---

[eric-wieser]

I think list.fin_range should refer to finset.univ in the docstring.

[Vierkantor]

I think we will need to add a new case to tactic.norm_num.eval_finset to handle univ : finset (fin n). Let me know if you're having trouble with that.

[YaelDillies]

There already is a case to handle univ : finset α. Is that not enough?

[Vierkantor]

I don't think so, the case for univ just opens up the fintype instance and goes in recursion on the expression it finds in the fintype.elems field.

[YaelDillies]

Then I have no idea what to do! 😅

[Vierkantor]

I've pushed a commit that should work, but we'll have to wait for all the dependencies of the test to build to find out.

[YaelDillies]

Doesn't seem to have worked 😢

[Vierkantor]

Sorry, this dropped off my radar. Now it works! (for the one test file, on my machine...)

[eric-wieser]

It's quite hard to parse the norm_num diff here.

Could you spin out a PR that just reorders finset/mutliset/list to list/multiset/finset first, since I think that reorder is what's making the diff painful.

[Vierkantor]

Okay: #15840.

[b-mehta]

@YaelDillies bump on this - it seems sensible enough to me but it needs a merge of master

[eric-wieser]

Thanks for splitting out the reorder, the norm_num diff is now much easier to follow!

[bors[bot]]

:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests