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).

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 α := @Lean.Meta.Monotonicity.defaultFailK✝) (goal : MVarId) : MetaM (List MVarId)

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

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