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

Similar to simpCore, but uses dsimp.

def Lean.Meta.Grind.preprocess (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.