.. _tac_exfalso:

exfalso
=======

Summary
-------

The ``exfalso`` tactic changes your goal to ``false``. Why might you want to do that? Usually because at this point you can deduce a contradiction from your hypotheses (for example because you are in the middle of a proof by contradiction).

Examples
--------

If your tactic state is like this:

.. code-block::

   hP : P
   h : P → false
   ⊢ Q

then this might initially look problematic, because we don't have any facts about ``Q`` to hand. However, ``false → Q`` regardless of whether ``Q`` is true or false, so and ``hP`` and ``h`` between them are enough to prove ``false``. So you can solve the goal with

.. code-block::

   exfalso,
   apply h,
   exact hP

.. warning::

   Don't use this tactic unless you can deduce a contradiction from your hypotheses! If your hypotheses are not contradictory then ``exfalso`` will leave you with an unsolvable goal.

Details
-------

What is actually happening here is that there's a theorem in Lean called ``false.elim`` which says that for all propositions ``P``, ``false → P``. Under the hood this tactic is just doing ``apply false.elim``, but ``exfalso`` is a bit shorter.