feat(Mathlib/Tactic/finCases): Port `fin_cases`

[winston-h-zhang]

trafficstars

This PR implements fin_cases from mathlib3. It largely follows the original idea behind Scott's code. There are a few notable details for this PR

• To have fin_casess full functionality, we must port Fintype/Finset/Multiset. I've tried my best to only use the minimal number of dependencies, but right now it feels very messy. Is there a standard way of organizing this?
• cases_core doesn't exist and I don't know how to recreate the API. There's an extremely hacky section that needs to be fixed.

[digama0]

Please separate out the porting parts of this PR into its own PR.

[digama0]

For porting, you should be using https://github.com/leanprover-community/mathlib3port, not https://github.com/leanprover-community/mathlib directly. This will save you a lot of trouble fixing lean 3 syntax stuff, and will save us trouble when we later have to diff these files against the automatically ported files when new theorems are added to mathlib and/or we get around to porting these files for real.

[kim-em]

@winston-h-zhang, would it be okay if I started some work on this port? My plan would be

1. Port a minimal version of fin_cases that only deals with List A hypotheses. This will get most of the logic of the tactic sorted out, but not need any material on Finset and Multiset ported.
2. In parallel, port as little as possible of Finset and Multiset from mathlib3port.
3. Once those are both done, make fin_cases do everything.

I would probably just start a new branch, but make use of some of your code from here (appropriately credited, of course :-).

[kim-em]

Made redundant by #437.