.. _tactic.have:

have
====

The ``have`` goal can be used to put new hypotheses into the :ref:`local_context <glossary.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.

.. _tactic.have.implies:
   
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:

.. code-block:: lean

   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:

.. code-block:: lean

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

.. _tactic.have.forall:

Example (∀)
------------

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

.. code-block:: lean
		
   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