The fin_cases tactic.

Given a hypothesis of the form h : x ∈ (A : List α), x ∈ (A : Finset α), or x ∈ (A : Multiset α), or a hypothesis of the form h : A, where [Fintype A] is available, fin_cases h will repeatedly call cases to split the goal into separate cases for each possible value.

def Lean.Elab.Tactic.getMemType {m : Type → Type} [Monad m] [MonadError m] (e : Expr) : m (Option Expr)

If e is of the form x ∈ (A : List α), x ∈ (A : Finset α), or x ∈ (A : Multiset α), return some α, otherwise none.

partial def Lean.Elab.Tactic.unfoldCases (g : MVarId) (h : FVarId) (userNamePre : Name := Name.anonymous) (counter : ℕ := 0) : MetaM (List MVarId)

Recursively runs the cases tactic on a hypothesis h. As long as two goals are produced, cases is called recursively on the second goal, and we return a list of the first goals which appeared.

This is useful for hypotheses of the form h : a ∈ [l₁, l₂, ...], which will be transformed into a sequence of goals with hypotheses h : a = l₁, h : a = l₂, and so on. Cases are named according to the order in which they are generated as tracked by counter and prefixed with userNamePre.

partial def Lean.Elab.Tactic.finCasesAt (g : MVarId) (hyp : FVarId) : MetaM (List MVarId)

Implementation of the fin_cases tactic.

def Lean.Elab.Tactic.finCases : ParserDescr

fin_cases h performs case analysis on a hypothesis of the form h : A, where [Fintype A] is available, or h : a ∈ A, where A : Finset X, A : Multiset X or A : List X.

As an example, in

example (f : ℕ → Prop) (p : Fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val := by
  fin_cases p; simp
  all_goals assumption

after fin_cases p; simp, there are three goals, f 0, f 1, and f 2.

fin_cases used to also have two modifiers, fin_cases ... with ... and fin_cases ... using .... With neither actually used in mathlib, they haven't been re-implemented here.

In case someone finds a need for them, and wants to re-implement, the relevant sections of the doc-string are preserved here:

---

fin_cases h with l takes a list of descriptions for the cases of h. These should be definitionally equal to and in the same order as the default enumeration of the cases.

For example,

example (x y : ℕ) (h : x ∈ [1, 2]) : x = y := by
  fin_cases h with 1, 1+1

produces two cases: 1 = y and 1 + 1 = y.

When using fin_cases a on data a defined with let, the tactic will not be able to clear the variable a, and will instead produce hypotheses this : a = .... These hypotheses can be given a name using fin_cases a using ha.

For example,

example (f : ℕ → Fin 3) : True := by
  let a := f 3
  fin_cases a using ha

produces three goals with hypotheses ha : a = 0, ha : a = 1, and ha : a = 2.