def Lean.MVarId.constructorCore (mvarId : MVarId) (cfg : Meta.ApplyConfig := { }) (findAll : Bool := true) : MetaM (List MVarId × Array Name)

When the goal mvarId type is an inductive datatype, constructorCore calls apply with the first matching constructor.

Along with the resulting goals, it returns the constructors that apply succeeds with, in declaration order. When findAll is false, the search stops at the first match, so at most one constructor is reported.

def Lean.MVarId.constructor (mvarId : MVarId) (cfg : Meta.ApplyConfig := { }) : MetaM (List MVarId)

When the goal mvarId type is an inductive datatype, constructor calls apply with the first matching constructor.

def Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId