mathlib documentation

tactic.fin_cases

source
meta def tactic.guard_mem_fin (e : expr) :
tactic expr

Checks that the expression looks like x ∈ A for A : finset α, multiset α or A : list α, and returns the type α.

source
meta def tactic.expr_list_to_list_expr (e : expr) :
tactic (list expr)

source
meta def tactic.fin_cases_at_aux (with_list : list expr) (e : expr) :
tactic unit

source
meta def tactic.fin_cases_at (with_list : option pexpr) (e : expr) :
tactic unit

source
meta def tactic.interactive.fin_cases (a : interactive.parse hyp) (a_1 : interactive.parse (lean.parser.tk "with" *> interactive.types.texpr)?) :
tactic unit

fin_cases h performs case analysis on a hypothesis of the form h : A, where [fintype A] is available, or h ∈ A, where A : finset X, A : multiset X or A : list X.

fin_cases * performs case analysis on all suitable hypotheses.

As an example, in

example (f : ℕ → Prop) (p : fin 3) (h0 : f 0) (h1 : f 1) (h2 : f 2) : f p.val :=
begin
  fin_cases *; simp,
  all_goals { assumption }
end

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