structure Lean.Meta.InductionSubgoal : Type

• mvarId : Lean.MVarId
• fields : Array Lean.Expr
• subst : Lean.Meta.FVarSubst

instance Lean.Meta.instInhabitedInductionSubgoal : Inhabited Lean.Meta.InductionSubgoal

structure Lean.Meta.AltVarNames : Type

• explicit : Bool
• varNames : List Lake.Name

instance Lean.Meta.instInhabitedAltVarNames : Inhabited Lean.Meta.AltVarNames

def Lean.MVarId.induction (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (recursorName : Lake.Name) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) : Lean.MetaM (Array Lean.Meta.InductionSubgoal)

@[deprecated Lean.MVarId.induction]

def Lean.Meta.induction (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (recursorName : Lake.Name) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) : Lean.MetaM (Array Lean.Meta.InductionSubgoal)