# Documentation

Lean.Meta.Tactic.Cases

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.generalizeTargetsEq (mvarId : Lean.MVarId) (motiveType : Lean.Expr) (targets : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For

Similar to generalizeTargets but customized for the casesOn motive. Given a metavariable mvarId representing the

Ctx, h : I A j, D |- T


where fvarId is hs id, and the type I A j is an inductive datatype where A are parameters, and j the indices. Generate the goal

Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T


Remark: (j == j' -> h == h') is a "telescopic" equality. Remark: j is sequence of terms, and j' a sequence of free variables. The result contains the fields

• mvarId: the new goal
• indicesFVarIds: j' ids
• fvarId: h' id
• numEqs: number of equations in the target
Equations
• One or more equations did not get rendered due to their size.
structure Lean.Meta.CasesSubgoalextends :
Instances For
Instances For
partial def Lean.Meta.Cases.unifyEqs? (numEqs : Nat) (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (caseName? : optParam () none) :
def Lean.Meta.Cases.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : ) :

Apply casesOn using the free variable majorFVarId as the major premise (aka discriminant). givenNames contains user-facing names for each alternative.

Equations
def Lean.Meta.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : ) :
Equations
def Lean.MVarId.casesRec (mvarId : Lean.MVarId) (p : ) :

Keep applying cases on any hypothesis that satisfies p.

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

Applies cases (recursively) to any hypothesis of the form h : p ∧ q.

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

Applies cases to any hypothesis of the form h : r = s.

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

Auxiliary structure for storing byCases tactic result.

Instances For
def Lean.MVarId.byCases (mvarId : Lean.MVarId) (p : Lean.Expr) (hName : ) :

Split the goal in two subgoals: one containing the hypothesis h : p and another containing h : ¬ p.

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