split

Summary

If your goal is a proof which is “made up of subproofs” (for example a goal like ⊢ P ∧ Q; to prove this you have to prove P and Q) then the split tactic will turn your goal into these multiple simpler goals.

Examples

1. Faced with the goal ⊢ P ∧ Q, the split tactic will turn it into two goals ⊢ P and ⊢ Q.

2. Faced with the goal ⊢ P ↔ Q, split will turn it into two goals ⊢ P → Q and ⊢ Q → P.

3. Something which always amuses me – faced with ⊢ true, split will solve the goal. This is because true is made up of 0 subproofs, so split turns it into 0 goals.

Further notes

The refine tactic is a more refined version of split; faced with a goal of ⊢ P ∧ Q, split does the same as refine ⟨_, _⟩,. In fact refine is more powerful than split; faced with ⊢ P ∧ Q ∧ R you would have to use split twice to break it into three goals, whereas refine ⟨_, _, _⟩ does the job in one go.