def Lean.Meta.Split.getSimpMatchContext : MetaM Simp.Context

def Lean.Meta.Split.simpMatch (e : Expr) : MetaM Simp.Result

def Lean.Meta.Split.simpMatch.pre (e : Expr) : SimpM Simp.Step

def Lean.Meta.Split.simpMatchTarget (mvarId : MVarId) : MetaM MVarId

opaque Lean.Meta.Split.discrGenExId : InternalExceptionId

Internal exception for discriminant generalization failures due to type errors.

def Lean.Meta.Split.isDiscrGenException (ex : Exception) : Bool

def Lean.Meta.Split.applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params discrs : Array Expr) : MetaM (List MVarId)

def Lean.Meta.Split.mkDiscrGenErrorMsg (e : Expr) : MessageData

def Lean.Meta.Split.throwDiscrGenError {α : Type} (e : Expr) : MetaM α

def Lean.Meta.Split.splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

def Lean.Meta.splitTarget? (mvarId : MVarId) (splitIte : Bool := true) : MetaM (Option (List MVarId))

partial def Lean.Meta.splitTarget?.go (mvarId : MVarId) (splitIte : Bool := true) (target : Expr) (badCases : ExprSet) : MetaM (Option (List MVarId))

def Lean.Meta.splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId))