Bounds And Inequalities

Use this path when the goal is a concrete inequality over an interval or box.

Typical goals:

∀ x ∈ I, f x ≤ c
∀ x ∈ I, c ≤ f x
∀ x ∈ I, f x ≤ g x

Main tactics and commands:

certify_bound
certify_kernel
certify_kernel_fallback
multivariate_bound

certify_kernel is strict and only succeeds when the kernel-verified dyadic path can close the goal. Use certify_kernel_fallback when an explicit compiler/runtime fallback is acceptable.

For ergonomic raw Lean goals, start with certify_bound or interval_bound. The stricter kernel path is best for reflected Expr.eval goals or for goals whose raw expression bridge is known to be supported. When you want to try that kernel path first but still allow the normal raw-expression automation, use certify_kernel_fallback explicitly.

Minimal example:

import LeanCert.Tactic.IntervalAuto

example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 3 := by
  certify_bound

Discovery commands can help find a candidate bound before formalizing it. See Optimization and Discovery.

For the full tactic reference, see Reference → Tactics.

For troubleshooting failed interval proofs, see Troubleshooting.