def Lean.Meta.getCtorNumPropFields (ctorInfo : Lean.ConstructorVal) : Lean.MetaM Nat

inductive Lean.Meta.InjectionResultCore : Type

• solved: Lean.Meta.InjectionResultCore
• subgoal: Lean.MVarId → Nat → Lean.Meta.InjectionResultCore

def Lean.Meta.injectionCore (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM Lean.Meta.InjectionResultCore

inductive Lean.Meta.InjectionResult : Type

• solved: Lean.Meta.InjectionResult
• subgoal: Lean.MVarId → Array Lean.FVarId → List Lake.Name → Lean.Meta.InjectionResult

def Lean.Meta.injectionIntro (mvarId : Lean.MVarId) (numEqs : Nat) (newNames : List Lake.Name) (tryToClear : optParam Bool true) : Lean.MetaM Lean.Meta.InjectionResult

def Lean.Meta.injectionIntro.go (tryToClear : optParam Bool true) : Nat → Lean.MVarId → Array Lean.FVarId → List Lake.Name → Lean.MetaM Lean.Meta.InjectionResult

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.injectionIntro.go tryToClear 0 x x x = pure (Lean.Meta.InjectionResult.subgoal x x x)

def Lean.Meta.injection (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (newNames : optParam (List Lake.Name) []) : Lean.MetaM Lean.Meta.InjectionResult

inductive Lean.Meta.InjectionsResult : Type

• solved: Lean.Meta.InjectionsResult
• subgoal: Lean.MVarId → List Lake.Name → Lean.Meta.InjectionsResult

def Lean.Meta.injections (mvarId : Lean.MVarId) (newNames : optParam (List Lake.Name) []) (maxDepth : optParam Nat 5) : Lean.MetaM Lean.Meta.InjectionsResult

partial def Lean.Meta.injections.go (mvarId : Lean.MVarId) : Nat → List Lean.FVarId → Lean.MVarId → List Lake.Name → Lean.MetaM Lean.Meta.InjectionsResult