def Lean.Meta.getInductiveUniverseAndParams (type : Expr) : MetaM (List Level × Array Expr)

def Lean.Meta.withNewEqs {α : Type} (targets targetsNew : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α

def Lean.Meta.generalizeTargetsEq (mvarId : MVarId) (motiveType : Expr) (targets : Array Expr) : MetaM MVarId

structure Lean.Meta.GeneralizeIndicesSubgoal : Type

• mvarId : MVarId
• indicesFVarIds : Array FVarId
• fvarId : FVarId
• numEqs : Nat

def Lean.Meta.generalizeIndices' (mvarId : MVarId) (e : Expr) (varName? : Option Name := none) : MetaM GeneralizeIndicesSubgoal

Given a metavariable mvarId representing the goal

Ctx |- T

and an expression e : I A j, where I A j is an inductive datatype where A are parameters, and j the indices. Generate the goal

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

Remark: (j == j' -> e == 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

If varName? is not none, it is used to name h'.

def Lean.Meta.generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndicesSubgoal

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

structure Lean.Meta.CasesSubgoalextends Lean.Meta.InductionSubgoal : Type

• mvarId : MVarId
• fields : Array Expr
• subst : FVarSubst
• ctorName : Option Name

  The constructor of this subgoal. Is none in the catch-all of a sparse case match

structure Lean.Meta.Cases.Context : Type

• inductiveVal : InductiveVal
• nminors : Nat
• majorDecl : LocalDecl
• majorTypeFn : Expr
• majorTypeArgs : Array Expr
• majorTypeIndices : Array Expr

partial def Lean.Meta.Cases.unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none) : MetaM (Option (MVarId × FVarSubst))

def Lean.Meta.Cases.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) (interestingCtors? : Option (Array Name) := none) : MetaM (Array CasesSubgoal)

def Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array Meta.AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) (interestingCtors? : Option (Array Name) := none) : MetaM (Array Meta.CasesSubgoal)

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

• useNatCasesAuxOn is a temporary hack for the rcases family of tactics. Do not use it, as it is subject to removal. It enables using Nat.casesAuxOn instead of Nat.casesOn, which causes case splits on n : Nat to be represented as 0 and n' + 1 rather than as Nat.zero and Nat.succ n'.

def Lean.MVarId.casesRec (mvarId : MVarId) (p : LocalDecl → MetaM Bool) : MetaM (List MVarId)

Keep applying cases on any hypothesis that satisfies p.

def Lean.MVarId.casesAnd (mvarId : MVarId) : MetaM MVarId

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

def Lean.MVarId.substEqs (mvarId : MVarId) : MetaM (Option MVarId)

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

structure Lean.Meta.ByCasesSubgoal : Type

Auxiliary structure for storing byCases tactic result.

• mvarId : MVarId
• fvarId : FVarId

def Lean.MVarId.byCases (mvarId : MVarId) (p : Expr) (hName : Name := `h) : MetaM (Meta.ByCasesSubgoal × Meta.ByCasesSubgoal)

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

def Lean.MVarId.byCasesDec (mvarId : MVarId) (p dec : Expr) (hName : Name := `h) : MetaM (Meta.ByCasesSubgoal × Meta.ByCasesSubgoal)

Given dec : Decidable p, split the goal in two subgoals: one containing the hypothesis h : p and another containing h : ¬ p.