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:

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

which will leave you with the state

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

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

  1. 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:

ε : ℝ
h : ∃ (δ : ℝ) (H : δ > 0), δ ^ 2 = ε
⊢ ε < 0.1

then rcases h with ⟨δ, hδ, rfl⟩ turns the state into

δ : ℝ
hδ : δ > 0
⊢ δ ^ 2 < 0.1

Here ε has vanished, and all of the other occurrences of ε in the tactic state are now replaced with δ ^ 2.

  1. 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.

  2. 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 definitional equality.

Variants of intro include the intros tactic (intro + rcases) and the obtain tactic (have + rcases).