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  h2

which will leave you with the state

ε δ : 
 : δ > 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

δ : 
 : δ > 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).