Zulip Chat Archive

Stream: new members

Topic: multiple split etc.


view this post on Zulip Michael Beeson (Jul 01 2020 at 07:44):

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.)

view this post on Zulip Scott Morrison (Jul 01 2020 at 07:57):

refine ⟨_,_,_⟩

view this post on Zulip Scott Morrison (Jul 01 2020 at 07:57):

repeat { split }?

view this post on Zulip Shing Tak Lam (Jul 01 2020 at 07:58):

For the splitting a hypotheis, you can use rcases.

view this post on Zulip Scott Morrison (Jul 01 2020 at 07:58):

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

view this post on Zulip Scott Morrison (Jul 01 2020 at 07:58):

(it is what does the case splitting for tidy)


Last updated: May 09 2021 at 18:17 UTC