only relevant cases over a match

Stream: general

[Andrés Goens]

I have a pattern where I'm doing a proof by cases on an inductive with a bunch of arms for a match expression, and most pairs of them are the same, but I kind of still have to go over the product of all combinations nominally and Lean gets pretty slow when doing this. Here's an MWE:

inductive ManyArms
  | arm1
  | arm2
  | arm3
  | arm4
  | arm5
  | arm6
  | arm7
  | arm8
  | arm9
  | arm10
  | arm11
  | arm12
  | arm13
  | arm14
  | arm15
  | arm16
  | arm17
  | arm18
  | arm19
  | arm20
  | arm21
  | arm22
  | arm23
  | arm24
  | arm25
  | arm26
  | arm27
  | arm28
  | arm29
  | arm30


def someFun : ManyArms → ManyArms → Bool
 | .arm2, .arm3 => true
 | _, _ => false

theorem only23 {x y} : someFun x y = true → x = .arm2 ∧ y = .arm3 := by
  simp [someFun]
  cases x <;> cases y <;> simp

After the simp [someFun], my goal becomes:

⊢ (match x, y with
    | ManyArms.arm2, ManyArms.arm3 => true
    | x, x_1 => false) =
    true →
  x = ManyArms.arm2 ∧ y = ManyArms.arm3

So essentially it should only be two cases, from the match, but in this case it's 30^2 instead because it has to go over the cases of the inductive manyArms. (this does take some time even for this simple MWE). Is there any simple way to just go over these two cases instead?

[Aaron Liu]

Did you try split?

[Aaron Liu]

theorem only23 {x y} : someFun x y = true → x = .arm2 ∧ y = .arm3 := by
  simp [someFun]
  split <;> simp

[Aaron Liu]

This only produces two cases

[Andrés Goens]

awesome, that's exactly what I was looking for, thanks!