fin_cases on structure field

Stream: new members

[Li Xuanji]

Is there a way to use fin_cases on a structure field (d.g in this case)?

import Mathlib

structure MyStruct : Type where
  c : ZMod 2
  g : ZMod 3

theorem test1 (g : ZMod 3) : g = 0 ∨ g = 1 ∨ g = 2 := by
  fin_cases g <;> simp

theorem test2 (d : MyStruct) : d.g = 0 ∨ d.g = 1 ∨ d.g = 2 := by
  -- fin_cases d.g
  exact test1 d.g

[Jakub Nowak]

You could do something like this:

import Mathlib

structure MyStruct : Type where
  c : ZMod 2
  g : ZMod 3

theorem test2 (d : MyStruct) : d.g = 0 ∨ d.g = 1 ∨ d.g = 2 := by
  generalize eq : d.g = g
  fin_cases g <;> rw [←eq]

[Jakub Nowak]

It would be nice to support that though. But first, we should investigate why this doesn't work:

import Mathlib

structure MyStruct : Type where
  c : ZMod 2
  g : ZMod 3

/--
error: Tactic `cases` failed with a nested error:
Dependent elimination failed: Failed to solve equation
  ⟨0, ⋯⟩ = d.2
at case `List.Mem.head`
---
error: unsolved goals
d : MyStruct
h : d.g ∈ Fintype.elems
⊢ d.g = 0 ∨ d.g = 1 ∨ d.g = 2
-/
#guard_msgs in
theorem test2 (d : MyStruct) : d.g = 0 ∨ d.g = 1 ∨ d.g = 2 := by
  have h := Fintype.complete d.g
  fin_cases h

[Aaron Liu]

It's because the implementation of fin_cases is kind of stupid