constructor

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 constructor tactic will turn your goal into these multiple simpler goals.

Examples

Faced with the goal ⊢ P ∧ Q, the constructor tactic will turn it into two goals ⊢ P and ⊢ Q.
Faced with the goal ⊢ P ↔ Q, constructor will turn it into two goals ⊢ P → Q and ⊢ Q → P.
Something which always amuses me – faced with ⊢ True, constructor will solve the goal. This is because True is made up of 0 subproofs, so constructor turns it into 0 goals.

Further notes

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

Historical remark

constructor was called split in Lean 3, but split in Lean 4 now does what Lean 3’s split_ifs tactic does.