Nested pattern matching in cases

Stream: new members

[Rudy Peterson]

In Lean 4, I am trying to do nested pattern matching in case analysis, however I am running into errors.

namespace nested.examples
section andor
variable (p q r : Prop)

theorem ex1 : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intro
  | Or.inl hp =>
    exact ⟨.inl hp, .inl hp⟩
  | Or.inr ⟨hq, hr⟩ =>
    exact ⟨.inr hq, .inr hr⟩

theorem ex2 : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intros hpqr
  cases hpqr
  case Or.inl hp =>
    exact ⟨.inl hp, .inl hp⟩
  case Or.inr ⟨hq, hr⟩ =>
    exact ⟨.inr hq, .inr hr⟩

theorem ex3 : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intros hpqr
  cases hpqr with
  | Or.inl hp =>
    exact ⟨.inl hp, .inl hp⟩
  | Or.inr ⟨hq, hr⟩ =>
    exact ⟨.inr hq, .inr hr⟩
end andor
end nested.examples

ex works fine, but ex2 and ex3 both get the same error when I try to do the nested pattern matching in the Or.inr case:

Messages below:
17:13:
unexpected token '⟨'; expected '=>'
25:10:
unexpected token '⟨'; expected '=>'

Is there a way to do nested pattern matching in cases?

Thanks!

[Kevin Buzzard]

You can use mathlib's rcases (I know this doesn't answer the question)

import Mathlib

variable (p q r : Prop)

theorem ex2 : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intro hpqr
  rcases hpqr with hp | ⟨hq, hr⟩
  · exact ⟨.inl hp, .inl hp⟩
  · exact ⟨.inr hq, .inr hr⟩

[Kyle Miller]

cases looks like it would be similar to intro's pattern matching, but it uses a different system. (You have to label cases with inl and inr rather than Or.inl and Or.inr too, though that doesn't help with the further pattern matching.)

Instead, there's match for the equivalent to what intro can do:

theorem ex3 : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intros hpqr
  match hpqr with
  | Or.inl hp =>
    exact ⟨.inl hp, .inl hp⟩
  | Or.inr ⟨hq, hr⟩ =>
    exact ⟨.inr hq, .inr hr⟩