.. _tactic.show:

show
====

A tactic which can be used to change a goal to a :ref:`definitionally equivalent <glossary.definitional_equivalence>` goal. Note also :ref:`change <tactic.change>`, which works both with goals and hypotheses.

Example
-------

If `n : ℕ` then `n + 0` is definitionally equivalent to `n`, so the following proof works:

.. code-block:: lean

   example (a b : ℕ) : (a + 0) + b = b + a :=
   begin
     change a + b = b + a,
     rw add_comm
   end