The bound attribute

Any lemma tagged with @[bound] is registered as an apply rule for the bound tactic, by converting it to either norm apply or safe apply <priority>. The classification is based on the number and types of the lemma's hypotheses.

def Mathlib.Tactic.Bound.isZero {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : Lean.MetaM Bool

Check if an expression is zero

def Mathlib.Tactic.Bound.ineqPriority {u : Lean.Level} {α : Q(Type u)} (a b : Q(«$α»)) : Lean.MetaM Nat

Map the arguments of an inequality expression to a score

partial def Mathlib.Tactic.Bound.hypPriority (hyp : Q(Prop)) : Lean.MetaM Nat

Map a hypothesis type to a score

def Mathlib.Tactic.Bound.typePriority (decl : Lean.Name) (type : Lean.Expr) : Lean.MetaM Nat

Map a type to a score

def Mathlib.Tactic.Bound.typePriority.argPriority (x : Lean.Expr) : Lean.MetaM Nat

Score the type of argument x

def Mathlib.Tactic.Bound.typePriority.checkResult (decl : Lean.Name) (type : Lean.Expr) (t : Q(Prop)) : Lean.MetaM Unit

Insist that our conclusion is an inequality

def Mathlib.Tactic.Bound.declPriority (decl : Lean.Name) : Lean.MetaM Nat

Map a theorem decl to a score (0 means norm apply, 0 < means safe apply)

def Mathlib.Tactic.Bound.scoreToConfig (decl : Lean.Name) (score : Nat) : Aesop.Frontend.RuleConfig

Map a score to either norm apply or safe apply <priority>

def Mathlib.Tactic.Bound.attrBound_forward : Lean.ParserDescr

Attribute for forward rules for the bound tactic.

@[bound_forward] lemmas should produce inequalities given other hypotheses that might be in the context. A typical example is exposing an inequality field of a structure, such as HasPowerSeriesOnBall.r_pos.