Name an intermediate step
have records a fact you have derived, so later steps can use it by name.
In this course 6 / 10
Every proof so far has worked backwards from the goal, or handed Lean one finished term. Real proofs also work forwards: from what you already hold, derive a fact, give it a name, and carry on with it in the context. have is the tactic for that.
have hq : Q := hpq hp adds hq : Q to the hypotheses, exactly as if the theorem had been stated with it from the start. After := comes a proof of the type you stated — here an implication applied to its premise — and before it comes the name you will use later.
The type can be left out, but writing it is worth the few characters. It records what you believe you have just proved, and when the term does not match, Lean objects at that line instead of at the failure it causes three steps further down.
The proof after := may itself be a tactic block: have hq : Q := by exact hpq hp opens a small proof for that one fact. It is the same tactic either way; by only lets you use tactics inside the gap.
Worked example
example (A B C : Prop) (hab : A → B) (hbc : B → C) (ha : A) : C := by
have hb : B := hab ha
exact hbc hbThe named step is what makes this readable: hb is the halfway point between what you were given and what you had to show. Your exercise derives two facts from the same hypothesis and then builds a conjunction out of them.
have name : Type := proof records a fact you have derived. Forward steps like this are what turn a one-line proof into a readable argument.
Derive Q and R separately with have, then prove the conjunction.
Suggested steps
- Name the proof of Q
- Name the proof of R
- Split the conjunction
- Close both branches with the named facts
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