def Lean.Meta.Grind.cases (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM (List Lean.MVarId)

The grind tactic includes an auxiliary cases tactic that is not intended for direct use by users. This method implements it. This tactic is automatically applied when introducing local declarations with a type tagged with [grind_cases]. It differs from the user-facing Lean cases tactic in the following ways:

• It avoids unnecessary revert and intro operations.

• It does not introduce new local declarations for each minor premise. Instead, the grind tactic preprocessor is responsible for introducing them.

• It assumes that the major premise (i.e., the parameter fvarId) is the latest local declaration in the current goal.

• If the major premise type is an indexed family, auxiliary declarations and (heterogeneous) equalities are introduced. However, these equalities are not resolved using unifyEqs. Instead, the grind tactic employs union-find and congruence closure to process these auxiliary equalities. This approach avoids applying substitution to propositions that have already been internalized by grind.

Equations

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

def Lean.Meta.Grind.cases.throwInductiveExpected (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) {α : Type} (type : Lean.Expr) : Lean.MetaM α

Equations

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