Make `aesop` utilize `fin_cases`

[madvorak]

I suggest that aesop could call fin_cases in a similar way it currently calls cases (maybe with lower priority or priority depending on how many values there are).

import Mathlib.Tactic

example (i : Fin 2) : i = i * i := by
  fin_cases i <;> aesop

It would be great if the example above were proved by aesop alone.

[JLimperg]

I'm not convinced that this should be in the default rule set because it's a very explosive rule. But if there is a variant of fin_cases that applies it everywhere (fin_cases *), this could be registered in Aesop rulesets as desired. If there's no such variant yet, hopefully Mathlib would be willing to add it.

[JLimperg]

(The built-in cases rule is already borderline too explosive, but it's also quite important in practice, so I've left it enabled by default.)