.. _tactic.exact:

exact
=====

The ``exact`` tactic can be used to :ref:`close a goal <glossary.close>`.

Example
-------

If the local context is


.. code-block:: python

   P : Prop,
   HP : P
   ⊢ P

then the tactic ``exact HP`` (note: not ``exact P``) will close the goal.

In this case, because the goal is one of the hypotheses, the ``assumption`` tactic would also work fine. However ``exact`` is more general, because it takes an arbitrary term. For example, the goal here is not precisely one of the assumptions, it is built from two of them.

.. code-block:: lean

   example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
   begin
     /-
     P Q : Prop,
     HP : P,
     HPQ : P → Q
     ⊢ Q
     -/
     exact (HPQ HP)
   end

In fact, for proofs of the form ``begin exact X, end`` there is no point entering tactic mode at all:

.. code-block:: lean

   example (P Q : Prop) (HP : P) (HPQ : P → Q) : Q := HPQ HP