# Documentation

Mathlib.Tactic.CasesM

# casesm, cases_type, constructorm tactics #

These tactics implement repeated cases / constructor on anything satisfying a predicate.

def Mathlib.Tactic.casesMatching (g : Lean.MVarId) (matcher : ) (recursive : ) (allowSplit : ) (throwOnNoMatch : optParam Bool !recursive) :

Core tactic for casesm and cases_type. Calls cases on all fvars in g for which matcher ldecl.type returns true.

• recursive: if true, it calls itself repeatedly on the resulting subgoals
• allowSplit: if false, it will skip any hypotheses where cases returns more than one subgoal.
• throwOnNoMatch: if true, then throws an error if no match is found
Equations
• One or more equations did not get rendered due to their size.
partial def Mathlib.Tactic.casesMatching.go (matcher : ) (recursive : ) (allowSplit : ) (g : Lean.MVarId) (acc : optParam () #[]) :

Auxiliary for casesMatching. Accumulates generated subgoals in acc.

Elaborate a list of terms with holes into a list of patterns.

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

Returns true if any of the patterns match the expression.

Equations
• One or more equations did not get rendered due to their size.
• casesm p applies the cases tactic to a hypothesis h : type if type matches the pattern p.
• casesm p_1, ..., p_n applies the cases tactic to a hypothesis h : type if type matches one of the given patterns.
• casesm* p is a more efficient and compact version of · repeat casesm p. It is more efficient because the pattern is compiled once.

Example: The following tactic destructs all conjunctions and disjunctions in the current context.

casesm* _ ∨ _, _ ∧ _

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.elabCasesType (heads : ) (recursive : ) (allowSplit : ) :

Common implementation of cases_type and cases_type!.

Equations
• One or more equations did not get rendered due to their size.
• cases_type I applies the cases tactic to a hypothesis h : (I ...)
• cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)
• cases_type* I is shorthand for · repeat cases_type I
• cases_type! I only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current goal.

cases_type* Or And

Equations
• One or more equations did not get rendered due to their size.
• cases_type I applies the cases tactic to a hypothesis h : (I ...)
• cases_type I_1 ... I_n applies the cases tactic to a hypothesis h : (I_1 ...) or ... or h : (I_n ...)
• cases_type* I is shorthand for · repeat cases_type I
• cases_type! I only applies cases if the number of resulting subgoals is <= 1.

Example: The following tactic destructs all conjunctions and disjunctions in the current goal.

cases_type* Or And

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.constructorMatching (g : Lean.MVarId) (matcher : ) (recursive : ) (throwOnNoMatch : optParam Bool !recursive) :

Core tactic for constructorm. Calls constructor on all subgoals for which matcher ldecl.type returns true.

• recursive: if true, it calls itself repeatedly on the resulting subgoals
• throwOnNoMatch: if true, throws an error if no match is found
Equations
• One or more equations did not get rendered due to their size.
partial def Mathlib.Tactic.constructorMatching.go (matcher : ) (g : Lean.MVarId) (acc : optParam () #[]) :

Auxiliary for constructorMatching. Accumulates generated subgoals in acc.

• constructorm p_1, ..., p_n applies the constructor tactic to the main goal if type matches one of the given patterns.
• constructorm* p is a more efficient and compact version of · repeat constructorm p. It is more efficient because the pattern is compiled once.

Example: The following tactic proves any theorem like True ∧ (True ∨ True) consisting of and/or/true:

constructorm* _ ∨ _, _ ∧ _, True

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