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: δ > 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 : ∃ δ > 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. Note: the syntax is different for ∧ and ∨ because doing cases on an ∨ turns one goal into two (because the inductive type Or has two constructors).

Notes

rcases works up to definitional equality.

Other tactics which use the ⟨hP, hQ, hR⟩ / (hP | hQ | hR) syntax are the rintro tactic (intro + rcases) and the obtain tactic (have + rcases).