Extending `fin_cases` to work on Nats < a literal?

Stream: mathlib4

[David Sampson]

Right now you can get this to work by introducing an x' : Fin n, adding an equality hypothesis showing x = x'.val, doing some rewrites, and then calling fin_cases x', but it's kind of clunky.

Would folks consider enhancing the tactic to handle this case automatically a useful addition?

If so, it's something I would be interested in working on though I haven't contributed to mathlib before.

If not, is there a straightforward (1 lineish) way to do what I'm proposing using existing machinery?

[Kenny Lau]

import Mathlib

example (n : ℕ) (hn : n < 10) : True := by
  interval_cases n

Also this probably should be in #Is there code for X?

And next time you can receive a faster response if you include code such as above.

[David Sampson]

Thanks! This is perfect, don't know how I missed it.