.. _tactic.apply:

apply
=====

You can use ``apply H`` if you have a hypothesis ``H : P → Q`` and your goal is ``Q``. It changes the goal to ``P``.

.. code-block:: python

   ...
   H : P → Q,
   ...		
   ⊢ Q

becomes

.. code-block:: python

   ...
   H : P → Q,
   ...		
   ⊢ P

after ``apply H``.
   
In maths, what is happening is that if you know that ``P`` implies ``Q`` then to prove ``Q`` it suffices to prove ``P``.

.. _tactic.apply.not:

Example (``¬``)
---------------

.. code-block:: lean

   theorem contrapositive (P Q : Prop) (HPQ : P → Q) : ¬ Q → ¬ P :=
   begin
   /-
     P Q : Prop,
     HPQ : P → Q
     ⊢ ¬Q → ¬P
   -/
     intro HnQ,
     intro HP,
   /-
     P Q : Prop,
     HPQ : P → Q,
     HnQ : ¬Q,
     HP : P
     ⊢ false
   -/
     apply HnQ, -- !
   /-
     P Q : Prop,
     HPQ : P → Q,
     HnQ : ¬Q,
     HP : P
     ⊢ Q
   -/
     apply HPQ,
     assumption
   end

		
Above is a proof of the fact that if :math:`P\implies Q` then :math:`\lnot Q\implies \lnot P` in Lean. A mathematician might say "Let's prove this by contradiction", and then might feel bound to the idea that the *last* line of their proof must be "...but this is a contradiction, and hence we are done". But mathematics is more flexible than this. After assuming :math:`P\implies Q` and :math:`\lnot Q` and :math:`P` our goal is now to prove `false`, which in practice means that we need to derive a contradiction from our assumptions. However our hypothesis :math:`\lnot Q` can be interpreted as `Q → false`, and using the `apply` tactic reduces the goal from `false` to `Q`, reducing our problem to proving `Q` from `P` and `P → Q`; all of a sudden we are not proving something by contradiction any more.