Is there a way to split conjunction automatically?

isabelle

Solution

Use the `intro` method: `proof (intro conjI)`

Problem

I want to prove `A /\ B /\ C /\ D /\ E /\ F` in Isabelle. How can I split the subgoal to 6 separate subgoals automatically in `proof(rule ...)`, so then I can prove them separately afterwards? Of course, I can write `proof(rule conjI)` 5 times, but maybe there is a more elegant way to do splitting in one step?

Original source