perf: eliminate cases with all branches unreachable

[hargoniX]

This PR makes the LCNF simplifier eliminate cases where all alts are .unreach to just an .unreach.
an .unreach

We considered dropping a cases in a situation like this but decided against it because it might hinder reuse.

def test x : Bool :=
  cases x : Bool
  | Except.error a.1 =>
    ⊥
  | Except.ok a.2 =>
    let _x.3 := true;
    return _x.3

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 234a789 against 76f32e2 are in! @hargoniX

Minor changes (1)

• 🟥 big_do//instructions: +245.6M (+0.8%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 76f32e22734d99e81cc1a6f5380bdb5c7d34e689 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 17:45:49)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 76f32e22734d99e81cc1a6f5380bdb5c7d34e689 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-05 17:45:50)