.. _tactic.left:

.. _tactic.left.or:

``left`` and ``right``
======================

If the goal is of the form ``P ∨ Q``, then the ``left`` tactic changes the goal to ``P`` and the ``right`` tactic changes it to ``Q``. Here is an example.

.. code-block:: lean

   example (P Q : Prop) (HP : P) : P ∨ Q :=
   begin
     -- goal is P ∨ Q
     left,
     -- goal now P
     exact HP
   end
   
More generally if the goal is any inductive type with two constructors, then the ``left`` tactic changes the goal to the types needed for the first constructor, and the ``right`` tactic changes the goal to the types needed for the second constructor.