Documentation

Mathlib.Tactic.FinCases

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 : } [inst : ] [inst : ] (e : Lean.Expr) :
m ()

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

Equations
• One or more equations did not get rendered due to their size.

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.

Implementation of the fin_cases tactic.

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 *; simp
all_goals assumption


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

Equations
• One or more equations did not get rendered due to their size.

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.