split with named hypotheses

Stream: lean4

[Freddie Nash]

Is standard lib variant of the split tactic that allows you name the per-branch hypothesis all at once in the same manner as rcases ... with ...? (currently I would use rename_i on each branch as necessary, but I'd much prefer juxtaposing the hypotheses at the top)

[Jannis Limperg]

You can use

split
next h1 =>
  ...
next h2 =>
  ...

as a slightly less ugly workaround.

[Freddie Nash]

Thanks, not seen next before

[Freddie Nash]

Patterned decomposition is another nice feature of rcases

[Freddie Nash]

next naturally doesn't allow the neat juxtaposition, and seems it doesn't seem to have quite the same behaviour with e.g. the else part of an if, but still good to know and I'll keep playing around with it

[Jannis Limperg]

Related issue: lean4#2745