Examples of proofs which use extensive case splitting?

Stream: Is there code for X?

[Markus de Medeiros]

In SampCert we have a file containing a bunch of proofs involving conversions between different extended real number types. The proofs themselves are basically all just by cases, and I found that I could avoid doing a ton of redundant work by judiciously applying a few case splits at the start, and then using simp_all to discharge all but a handful of the goals.

The change to lean 4.9 broke a couple of these proofs, so now I'm trying to simplify this part of our codebase and make it more robust. I'm wondering if there are any examples out there for automating these case/simp-heavy proofs I could read for inspiration?

[Martin Dvořák]

I've been doing a lot of similar things recently:
https://github.com/madvorak/vcsp/blob/ef4b96946118c6c8b71ea73ee85b61805d6af3d8/VCSP/LinearProgrammingE.lean#L299
The readability can get slightly improved using the match tactic, but I don't have any tips on how to automate the case analyses.

[Markus de Medeiros]

Thanks for the link!

[Eric Wieser]

Your approach is a little strange in places; rather than building Or/Exists lemmas then using rcases, you can use cases directly

[Eric Wieser]

(this changed quite recently, previously you had to write cases x using EReal.rec instead of just cases x)

[Markus de Medeiros]

This would definitely simplify some of them. Thanks!