multiple split etc.

Stream: new members

[Michael Beeson]

If my goal is a conjunction of three or more conjuncts how can I split it all at once into several subgoals, one for each conjunct?
And similarly, if one of my hypotheses is a conjunct with several conjuncts, and I want to break it up completely,
making each conjunct a separate hypothesis, how do I do that with one command? (I have written some very ugly proofs splitting off one conjunct at a time, it is time I learned the right way.)

[Scott Morrison]

refine ⟨_,_,_⟩

[Scott Morrison]

repeat { split }?

[Shing Tak Lam]

For the splitting a hypotheis, you can use rcases.

[Scott Morrison]

there's also auto_cases which may be helpful, although is not typically used interactively

[Scott Morrison]

(it is what does the case splitting for tidy)