.. _tactic.change:

change
======

Like :ref:`show <tactic.show>` but for hypotheses. Changes a hypothesis or goal to a :ref:`definitionally equivalent <glossary.definitional_equivalence>` one.

Example
-------

..  code-block:: lean
		 
    example (a b : ℕ) (H : a + 0 = b + 0) :
    a + 3 = b + 3 :=
    begin
      -- a + 0 is definitially equivalent to a, and same for b
      change a = b at H,
      rw H
    end