feat: port fin_cases

[kim-em]

trafficstars

This is a port of fin_cases. It doesn't yet support the with or using clauses from mathlib3.

I could remove the dependence on #433, but would have to (temporarily) remove all the tests to do so.

• depends on: #433

[digama0]

I'm not enthused about this implementation, it has a lot of potential failure modes, but since it's not passing all the tests or implementing all the options we'll need to extend it later anyway, and this is good enough for now.

bors r+

[bors[bot]]

Build failed:

• Build

[kim-em]

The implementation is pretty much isomorphic to the one in mathlib3, so I'll blame the author of that. (Err... sorry.)

After I merge master it is all failing, with metavariables in the declarations, and I'm not immediately seeing why.

[kim-em]

Ugh, voodoo changing a 3 to a 2 fixes the main problem.

Currently, if you call fin_cases h on a bad hypotheses that it can't handle, it just deletes the goal and reports success. Not cool...

[kim-em]

Okay, at least superficially fixed that, now we don't catch the error if cases outright fails.

[kim-em]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style