def Lean.Meta.Grind.simpCore (e : Expr) : GrindM Simp.Result

Simplifies the given expression using the grind simprocs and normalization theorems.

def Lean.Meta.Grind.dsimpCore (e : Expr) : GrindM Expr

Similar to simpCore, but uses dsimp.

@[export lean_grind_preprocess]

def Lean.Meta.Grind.preprocessImpl (e : Expr) : GoalM Simp.Result

Preprocesses e using grind normalization theorems and simprocs, and then applies several other preprocessing steps.

def Lean.Meta.Grind.pushNewFact' (prop proof : Expr) (generation : Nat := 0) : GoalM Unit

def Lean.Meta.Grind.pushNewFact (proof : Expr) (generation : Nat := 0) : GoalM Unit

Infers the type of the proof, preprocess it, and adds it to todo list.

def Lean.Meta.Grind.preprocessLight (e : Expr) : GoalM Expr

A lighter version of preprocess which produces a definitionally equal term, but ensures assumptions made by grind are satisfied.