Build a two-part proof
constructor splits P ∧ Q, bullets keep the branches tidy.
In this course 4 / 13
A proof of P ∧ Q is a proof of P together with a proof of Q. constructor splits such a goal into those two parts. From that point your proof has two goals open, and the Goal panel numbers them so you can see which one you are working on.
A bullet · focuses the first open goal and requires it to be closed before you move on. Bulleted proofs read like an outline, and when a branch fails Lean points at that bullet rather than at the end of the proof. Type \. followed by a space, or click · in the symbol bar under the editor.
The branches are independent and often need different tactics. In the worked example the first is closed with a hypothesis and the second by computation. Treat each bullet as its own small proof with its own goal. Bullets nest: a branch that splits again gets bullets of its own, indented one step further.
One shortcut in this editor: press Enter at the end of a constructor line and both bullets are inserted for you, already indented.
Worked example
example (A : Prop) (ha : A) : A ∧ (2 + 2 = 4) := by
constructor
· exact ha
· rflThe two branches are closed by different tactics, because the two halves of the conjunction are different kinds of claim. In your exercise both halves are hypotheses, but check which name belongs to which side.
constructor splits P ∧ Q into two goals. Bullets keep the branches separate and the errors local.
Combine hp and hq into a proof of P ∧ Q.
Suggested steps
- Split the conjunction into two goals
- Prove the left half
- Prove the right half
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct