mathlib3

665c13a4 - chore(*): clean up/golf proofs with unneeded or case splits (#10569)

chore(*): clean up/golf proofs with unneeded or case splits (#10569) Golf/simplify/clean up some more proofs with unnecessary case splits, this time found by linting for `or.dcases_on` with branches proving the more general fact.