.. _tactic.existsi:

existsi
=======

The ``existsi`` tactic makes progress with goals of the form ``∃ x : X, P x``. With this as the goal, and with ``t : X`` in the :ref:`local context <glossary.local_context>`, the tactic ``existsi t`` will change the goal to ``P t``.

Example
-------

.. code-block:: lean

   example : ∃ n : ℕ, 2 + 2 = n :=
   begin
     existsi 4,
     -- goal now 2 + 2 = 4
   refl
   end

Note that ``existsi`` can be quite dense about types -- you might have to explicitly tell it the type of the term you are trying to use. if you have mathlib installed, then the ``use`` tactic is slightly more user-friendly.

.. code-block:: lean

   import tactic.interactive -- for use tactic
   import data.real.basic -- for real numbers

   example : ∃ n : ℝ, n + 3 = 3 + 7 :=
   begin
     -- existsi 7, -- fails
     -- existsi (7 : ℝ), -- works
     use 7, -- works
     -- goal now 7 + 3 = 3 + 7
     apply add_comm, -- commutativity of addition closes the goal
   end