def Lean.Meta.Monotonicity.headBetaUnderLambda (f : Expr) : Expr

opaque Lean.Meta.Monotonicity.monotoneExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name)

Environment extensions for monotonicity lemmas

def Lean.Meta.Monotonicity.findMonoThms (e : Expr) : MetaM (Array Name)

Finds tagged monotonicity theorems of the form monotone (fun x => e).

def Lean.Meta.Monotonicity.defaultFailK {α : Type} (f : Expr) (monoThms : Array Name) : MetaM α

partial def Lean.Meta.Monotonicity.solveMonoCall (α inst_α e : Expr) : MetaM (Option Expr)

Base case for solveMonoStep: Handles goals of the form

monotone (fun f => f.1.2 x y)

It's tricky to solve them compositionally from the outside in, so here we construct the proof from the inside out.

def Lean.Meta.Monotonicity.solveMonoStep (failK : {α : Type} → Expr → Array Name → MetaM α := @defaultFailK) (goal : MVarId) : MetaM (List MVarId)

partial def Lean.Meta.Monotonicity.solveMono (failK : {α : Type} → Expr → Array Name → MetaM α := fun {α : Type} => defaultFailK) (goal : MVarId) : MetaM Unit

def Lean.Meta.Monotonicity.evalMonotonicity : Elab.Tactic.Tactic