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
If
ε : ℝ
is in your tactic state, and also a hypothesish : ∃ δ > 0, δ^2 = ε
then you can takeh
apart with thecases'
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⟩
.
In fact you can do a little better. The hypothesis
h2
can be used as a definition ofε
, or a formula forε
, and thercases
tactic has an extra trick which enables you to completely removeε
from the tactic state, replacing it everywhere withδ ^ 2
. Instead of calling the hypothesish2
you can instead typerfl
. 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
.
If
h : P ∧ Q ∧ R
thenrcases h with ⟨hP, hQ, hR⟩
directly decomposesh
intohP : P
,hQ : Q
andhR : R
. Again this would take two moves withcases'
.If
h : P ∨ Q ∨ R
thenrcases h with (hP | hQ | hR)
will replace the goal with three goals, one containinghP : P
, one containinghQ : Q
and the otherhR : R
. Againcases'
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 typeOr
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
).