Use this file to discover all available pages before exploring further.
Beyond arithmetic and simplification, Mathlib offers a collection of automation tactics that can close whole classes of goals with minimal user input. These range from complete decision procedures for finite computations (decide, native_decide) through propositional logic solvers (tauto) and general proof search (aesop) to domain-specific provers for positivity, continuity, measurability, and other function properties. Knowing which tool fits a given goal can make the difference between a one-line proof and a lengthy manual argument.
decide proves any goal whose type is a Decidable proposition by running the kernel’s evaluator on the decision procedure. It is complete for decidable goals but can be very slow for large computations because the Lean kernel performs each reduction step in the type theory.native_decide works identically but compiles the decision procedure to native code before running it. This makes it orders of magnitude faster for computationally intensive goals, such as primality tests or large finite-set membership checks.
Basic decide
native_decide
example : 2 + 2 = 4 := by decideexample : ¬ (3 = 5) := by decide-- Works on finite types and decidable predicatesexample : ∀ b : Bool, b || true = true := by decideexample : (10 : Fin 100).val < 50 := by decide
-- Much faster for computationally heavy goalsexample : Nat.Prime 1009 := by native_decideexample : Nat.Prime 65537 := by native_decide-- Large list membershipexample : 17 ∈ ([3, 7, 11, 17, 23] : List ℕ) := by native_decide
native_decide generates a proof that invokes compiled native code, which is not re-checked by the Lean kernel at verification time. Unlike sorry, it does produce a genuine certificate — but correctness depends on the native compiler and runtime producing the right answer. The proof is accepted without kernel-level reduction, so it adds a trusted-code dependency to your proof. Use it only when decide is too slow and the goal is clearly decidable.
tauto (also written itauto for the intuitionistic version) proves propositional tautologies in classical logic. It handles goals built from ∧, ∨, →, ¬, ↔, True, and False by exhaustive case analysis.
example (p q : Prop) : p ∧ q → q ∧ p := by tautoexample (p q r : Prop) : (p → q) → (q → r) → p → r := by tautoexample (p : Prop) : p ∨ ¬ p := by tauto-- tauto handles longer tautologies automaticallyexample (a b c d : Prop) : ((a → b) ∧ (c → d)) → (a ∨ c) → (b ∨ d) := by tauto
tauto works on propositional goals only — it does not understand quantifiers or arithmetic. For goals mixing logic and arithmetic, use aesop or a manual decomposition.
aesop is Mathlib’s general-purpose proof search tactic. It combines forward reasoning, backward chaining, and simp-based normalization to explore a search tree of possible proof steps. It is extensible: users and library authors can tag lemmas with @[aesop] to register them as search rules.
-- aesop can close many structural goalsexample (s t : Set α) (h : s ⊆ t) (x : α) (hx : x ∈ s) : x ∈ t := by aesop-- Works well on goals involving membership, subsets, and basic logicexample (p q : Prop) (hp : p) (hq : q) : p ∧ q := by aesop-- aesop? prints the proof it foundexample (h : α → β) (ha : α) : β := by aesop
Customizing aesop with @[aesop]
You can register your own lemmas as aesop rules using the @[aesop] attribute:
-- Register as a forward rule (apply when preconditions are met)@[aesop forward]theorem myLemma (h : P x) : Q x := ...-- Register as a safe rule (always apply without branching)@[aesop safe apply]theorem trivialStep : P → P := id-- Register as a norm rule (used for normalization, like simp)@[aesop norm simp]theorem mySimp : f (g x) = x := ...
See the Mathlib.Tactic.Aesop documentation for the full rule syntax.
aesop is best used when other tactics don’t quite apply and the goal has a structural feel. For purely arithmetic goals, prefer linarith, omega, or norm_num. For goals involving coercions, use norm_cast first.
positivity proves goals of the form 0 ≤ e, 0 < e, or e ≠ 0 by decomposing the expression e and applying positivity/nonnegativity lemmas for each operation. It understands:
Arithmetic: +, *, ^, /, |·| (absolute value)
Special functions: Real.sqrt, n ! (factorial), Nat.choose
Sums and products: ∑, ∏
Conditional expressions: ite, max, min
example (x : ℝ) : 0 ≤ x ^ 2 := by positivityexample (n : ℕ) : 0 < n.factorial := by positivityexample (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 0 < x * y := by positivityexample (x : ℝ) : 0 ≤ |x| := by positivity-- Works on sums and products when each term is nonnegexample (f : ℕ → ℝ) (hf : ∀ i, 0 ≤ f i) (s : Finset ℕ) : 0 ≤ ∑ i ∈ s, f i := by positivity
Positivity extensions
With hypotheses
-- positivity handles Real.sqrtexample (x : ℝ) : 0 ≤ Real.sqrt x := by positivity-- positivity handles NNReal and ENNRealexample (x : ℝ≥0) : (0 : ℝ≥0) ≤ x := by positivity-- positivity handles normsexample (v : EuclideanSpace ℝ (Fin 3)) : 0 ≤ ‖v‖ := by positivity
-- positivity uses local hypotheses for compound expressionsexample (a b : ℝ) (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a * b + a ^ 2 := by positivityexample (n : ℕ) (hn : n > 0) : 0 < (n : ℝ) := by exact_mod_cast hn
positivity is extensible via the @[positivity] attribute. Mathlib uses this to teach it about Real.sqrt, Nat.factorial, abs, and many other functions. You can write your own positivity extensions for custom operations.
continuity proves goals of the form Continuous f, ContinuousAt f x, or ContinuousOn f s by composing continuity lemmas. It works by breaking down the function into primitive components (arithmetic operations, polynomials, standard functions) and applying the corresponding lemmas.
example : Continuous (fun x : ℝ => x ^ 2 + 1) := by continuityexample : Continuous (fun x : ℝ => Real.exp x + Real.sin x) := by continuityexample : ContinuousOn (fun x : ℝ => 1 / x) {x | x ≠ 0} := by apply ContinuousOn.div continuousOn_const continuousOn_id intro x hx exact hx
continuity has largely been superseded by fun_prop in recent Mathlib. For new code, prefer fun_prop, which handles continuity as one of several function properties and is more extensible.
example : Continuous (fun x : ℝ => x ^ 2 + Real.exp x) := by fun_propexample : Measurable (fun x : ℝ => x + 1) := by fun_propexample : Differentiable ℝ (fun x : ℝ => x ^ 3 - 2 * x) := by fun_prop-- fun_prop handles compositions automaticallyexample : Continuous (fun x : ℝ => Real.sin (x ^ 2 + 1)) := by fun_prop
Registering custom function properties with fun_prop
To make fun_prop aware of a new property MyProp, register it with the @[fun_prop] attribute:
-- Mark the property type as a fun_prop targetattribute [fun_prop] MyProp-- Register lemmas for specific operations@[fun_prop]theorem myProp_add (hf : MyProp f) (hg : MyProp g) : MyProp (fun x => f x + g x) := ...@[fun_prop]theorem myProp_comp (hf : MyProp f) (hg : MyProp g) : MyProp (f ∘ g) := ...
When fun_prop fails, it may output a trace showing which subgoal it got stuck on. Enable tracing with set_option trace.Meta.Tactic.fun_prop true to diagnose the issue.
measurability proves Measurable f and MeasurableSet s goals by composing measurability lemmas. Like continuity, it has been largely superseded by fun_prop, but it remains available and still works for many standard goals.
example : Measurable (fun x : ℝ => x + 1) := by measurabilityexample : MeasurableSet {x : ℝ | x > 0} := by measurabilityexample (f g : ℝ → ℝ) (hf : Measurable f) (hg : Measurable g) : Measurable (fun x => f x + g x) := by measurability
For complex measurability goals, especially those involving integrals or advanced measure theory, fun_prop is the preferred tactic in current Mathlib.
