have

The have goal can be used to put new hypotheses into the local_context. Writing have H : (some proposition) in Lean is like writing “I now claim that (some proposition) is true” in the middle of a maths proof.

Of course, you now have to prove H before you can continue, so the number of goals goes up by one.

Example

Here is a proof that if P is true, and if P → Q and Q → R, then R is true. In maths the proof might go like this. “First, I claim that Q is true, and the proof is that P is true, and P implies Q. Now I claim that R is true, and that’s because we know that Q implies R and we just proved that Q was true. Here’s what this proof looks like in Lean:

try it!

example (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R) : R :=
begin
  -- one goal, R.
  have HQ : Q, -- now two goals, Q and R.
    apply HPQ,
    exact HP, -- proof of Q finished, now back to R
  apply HQR,
  exact HQ -- we can use the proof of Q because we now have it
end

As well as the have HQ : Q, syntax, there is also the have HQ : Q := ... syntax, where the proof of Q follows immediately after the := like this:

try it!

example (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R) : R :=
begin
  have HQ : Q := HPQ HP,
  exact (HQR HQ),
end

Example (∀)

Here we build terms of type P a and Q a using the have tactic.

try it!

 example (X : Type) (P Q : X → Prop) (a : X) (HP : ∀ x : X, P x) (HQ : ∀ x : X, Q x): P a ∧ Q a :=
 begin
   have HPa : P a := HP a,
   have HQa : Q a := HQ a,
   split,
     -- now two goals P a and Q a
   { exact HPa},
   { exact HQa},
end