.. _tac_rcases:

rcases
======

Summary
-------

The ``rcases`` tactic can be used to do multiple ``cases`` tactics all in one line. It can also be used to do certain variable substitutions with a ``rfl`` trick.

Examples
--------

1) If ``ε : ℝ`` is in your tactic state, and also a hypothesis ``h : ∃ δ > 0, δ^2 = ε`` then you can take ``h`` apart with the ``cases`` tactic. For example you can do this:

.. code-block::

   cases h with δ h1, -- h1 : ∃ (H : δ > 0), δ ^ 2 = ε 
   cases h1 with hδ h2,

which will leave you with the state

.. code-block::

    ε δ : ℝ
    hδ : δ > 0
    h2 : δ ^ 2 = ε

However, you can get there in one line with ``rcases h with ⟨δ, hδ, h2⟩``.

2) In fact you can do a little better. The hypothesis ``h2`` can be used as a *definition* of ``ε``, or a *formula* for ``ε``, and the ``rcases`` tactic has an extra trick which enables you to completely remove ``ε`` from the tactic state, replacing it everywhere with ``δ ^ 2``. Instead of calling the hypothesis ``h2`` you can instead type ``rfl``. This has the effect of rewriting ``← h2`` everywhere and thus replacing all the ``ε`` s with ``δ ^ 2``. If your tactic state contains this:

.. code-block::

   ε : ℝ
   h : ∃ (δ : ℝ) (H : δ > 0), δ ^ 2 = ε
   ⊢ ε < 0.1
   
then ``rcases h with ⟨δ, hδ, rfl⟩`` turns the state into

.. code-block::

   δ : ℝ
   hδ : δ > 0
   ⊢ δ ^ 2 < 0.1
   
Here ``ε`` has vanished, and all of the other occurrences of ``ε`` in the tactic state are now replaced with ``δ ^ 2``.

3) If ``h : P ∧ Q ∧ R`` then ``rcases h with ⟨hP, hQ, hR⟩`` directly decomposes ``h`` into ``hP : P``, ``hQ : Q`` and ``hR : R``. Again this would take two moves with ``cases``.

4) If ``h : P ∨ Q ∨ R`` then ``rcases h with (hP | hQ | hR)`` will replace the goal with three goals, one containing ``hP : P``, one containing ``hQ : Q`` and the other ``hR : R``. Again ``cases`` would take two steps to do this.

Details
-------

Note that ``rcases`` works up to :ref:`definitional equality <defeq>`.

Variants of ``intro`` include the :ref:`intros <tac_intros>` tactic (``intro`` + ``rcases``) and the :ref:`obtain <tac_obtain>` tactic (``have`` + ``rcases``).