Module 6 · Lesson 1

rcases & obtain

Powerful pattern matching tactics for destructuring hypotheses.rcases and obtain extend the core cases tactic with recursive patterns.

❗

rcases and obtain require Mathlib. Add import Mathlib.Tactic.Cases orimport Mathlib.Tactic.

Basic rcases

The rcases tactic ("recursive cases") extends the corecases tactic with a powerful pattern syntax. Instead of nested case splits, you write one pattern that destructures multiple layers at once.

lean

1import Mathlib.Tactic.Cases
2
3-- rcases destructs with angle bracket patterns
4example (h : ∃ n : Nat, n > 0) : True := by
5  rcases h with ⟨n, hn⟩
6  -- Now have n : Nat and hn : n > 0
7  trivial
8
9-- Compare to cases:
10example (h : ∃ n : Nat, n > 0) : True := by
11  cases h with
12  | intro n hn => trivial

Key Takeaway

rcases h with ⟨x, y, z⟩ recursively destructsh, naming the parts x,y, z.

Nested Patterns

The real power of rcases appears with nested structures. You can unpack existentials, conjunctions, and pairs all in a single pattern, avoiding multiple cases calls.

lean

1import Mathlib.Tactic.Cases
2
3-- rcases handles nested structures in one step
4example (h : ∃ n m : Nat, n < m ∧ m < 10) : True := by
5  rcases h with ⟨n, m, hnm, hm10⟩
6  -- n : Nat, m : Nat, hnm : n < m, hm10 : m < 10
7  trivial
8
9-- Even deeper nesting
10example (h : ∃ p : Nat × Nat, p.1 < p.2) : True := by
11  rcases h with ⟨⟨a, b⟩, hab⟩
12  -- a : Nat, b : Nat, hab : a < b
13  trivial

Disjunctions with |

lean

1import Mathlib.Tactic.Cases
2
3-- Use | to split disjunctions
4example (h : P ∨ Q) : Q ∨ P := by
5  rcases h with hp | hq
6  · right; exact hp
7  · left; exact hq
8
9-- Combined with existentials
10example (h : (∃ n : Nat, n = 0) ∨ (∃ n : Nat, n > 0)) : True := by
11  rcases h with ⟨n, hn⟩ | ⟨n, hn⟩
12  all_goals trivial

The obtain Tactic

lean

1import Mathlib.Tactic.Obtain
2
3-- obtain is like rcases but with a goal-style syntax
4example (h : ∃ n : Nat, n > 0 ∧ n < 10) : True := by
5  obtain ⟨n, hn_pos, hn_lt⟩ := h
6  trivial
7
8-- obtain can also introduce with a proof
9example : ∃ n : Nat, n > 0 := by
10  obtain ⟨n, hn⟩ : ∃ n : Nat, n > 0 := ⟨1, by norm_num⟩
11  exact ⟨n, hn⟩

💡

Use obtain when you want to destructure and name parts in one step. Use rcases for pattern matching on existing hypotheses.

Wildcard Patterns

lean

1import Mathlib.Tactic.Cases
2
3-- Use _ to discard parts you don't need
4example (h : ∃ n m : Nat, n < m) : ∃ n : Nat, True := by
5  rcases h with ⟨n, _, _⟩
6  exact ⟨n, trivial⟩
7
8-- Use rfl pattern to substitute immediately
9example (h : ∃ n : Nat, n = 5) : 5 = 5 := by
10  rcases h with ⟨_, rfl⟩
11  rfl

Deep Dive: rcases Patterns

The rcases pattern language:

⟨p₁, p₂, ...⟩ — destruct products/exists
p₁ | p₂ — split on disjunctions
rfl — substitute equalities
_ — discard (anonymous)
- — clear hypothesis after use
@name — name for the whole match

The rfl Pattern

lean

1import Mathlib.Tactic.Cases
2
3-- rfl immediately substitutes equalities
4example (h : ∃ n : Nat, n = 3 ∧ n > 0) : 3 > 0 := by
5  rcases h with ⟨_, rfl, h3⟩
6  -- n is replaced by 3 everywhere
7  exact h3
8
9-- Super useful for existentials with equations
10example (h : ∃ x : Nat, x = 10 ∧ x * 2 = 20) : 10 * 2 = 20 := by
11  rcases h with ⟨_, rfl, heq⟩
12  exact heq

Real-World Examples

Unpacking Complex Structures

lean

1import Mathlib.Tactic.Cases
2
3-- Nested existentials with conditions
4theorem unpack_bounds (h : ∃ ε > 0, ∀ x, |x| < ε → P x) : 
5    ∃ δ : ℝ, δ > 0 := by
6  rcases h with ⟨ε, hε_pos, _⟩
7  exact ⟨ε, hε_pos⟩

Case Analysis on Sum Types

lean

1import Mathlib.Tactic.Cases
2
3-- Handling Either-like types
4example (x : Sum Nat Bool) : Nat ∨ Bool := by
5  rcases x with n | b
6  · left; exact n
7  · right; exact b

With obtain for Existence

lean

1import Mathlib.Tactic.Obtain
2
3-- Proving existence by obtaining a witness
4example : ∃ n : Nat, n^2 = 4 := by
5  obtain ⟨n, hn⟩ : ∃ n : Nat, n = 2 := ⟨2, rfl⟩
6  use n
7  simp [hn]

rcases vs cases vs match

lean

1import Mathlib.Tactic.Cases
2
3-- Core Lean cases
4example (h : P ∧ Q) : P := by
5  cases h with
6  | intro left right => exact left
7
8-- rcases (Mathlib) - more concise
9example (h : P ∧ Q) : P := by
10  rcases h with ⟨hp, _⟩
11  exact hp
12
13-- match in term mode
14example (h : P ∧ Q) : P :=
15  match h with
16  | ⟨hp, _⟩ => hp

Exercise: Destruct an Existential

Use rcases to unpack an existential and use the witness.

lean

1import Mathlib.Tactic.Cases
2
3example (h : ∃ n : Nat, n > 5) : ∃ m : Nat, m > 0 := by
4  rcases h with ⟨n, hn⟩
5  exact ⟨n, by omega⟩

polyrith Next: push_neg