Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt

Use this file to discover all available pages before exploring further.

Tactics in Lean 4 are metaprograms that transform the current proof state — a collection of hypotheses and a goal — into zero or more simpler subgoals. Rather than constructing a complete proof term by hand, you enter tactic mode with the by keyword and issue a sequence of commands that incrementally discharge obligations. Mathlib ships hundreds of tactics covering arithmetic decision procedures, simplification engines, general-purpose proof search, and structural decomposition tools, making it possible to prove substantial mathematical results with concise, readable proof scripts.

​
Importing Tactics

The simplest way to access all of Mathlib’s tactics is a single import at the top of your file: 
import Mathlib
This imports the entire library, including every tactic. For faster compilation in larger projects, you can import only what you need. Each tactic lives in its own module: 
import Mathlib.Tactic.Linarith   -- linarith, nlinarith
import Mathlib.Tactic.Ring       -- ring, ring_nf
import Mathlib.Tactic.NormNum    -- norm_num
import Mathlib.Tactic.Positivity -- positivity
import Mathlib.Tactic.GCongr     -- gcongr
-- Note: omega is a Lean 4 core tactic (from Std/Batteries) and needs no import
When writing a standalone example or experimenting interactively, import Mathlib is the most convenient choice. Switch to granular imports once you know which tactics your project actually uses.

​
Tactic Mode vs Term Mode

Lean 4 supports two styles of proof writing. In term mode, you construct a proof term directly using function application, pattern matching, and anonymous constructors. In tactic mode, opened with by, you describe how to build that term step by step. 
-- Term mode: construct the proof explicitly
theorem add_comm_term (a b : ℕ) : a + b = b + a :=
  Nat.add_comm a b

-- Tactic mode: let tactics fill in the details
theorem add_comm_tactic (a b : ℕ) : a + b = b + a := by
  ring
The two styles can be freely mixed: a tactic block can appear inside a term, and term-mode expressions can appear as arguments to tactics.

​
Experimentation Keywords

Lean 4 provides several commands useful for exploration: 
-- Check the type of an expression or lemma
#check Nat.Prime

-- Evaluate a closed expression
#eval 2 ^ 10

-- Prove a statement without giving it a name
example (n : ℕ) (h : n > 0) : n ≥ 1 := by omega

-- Search for lemmas matching a pattern
#check?  -- (in some Mathlib configurations)
example (x y : ℝ) : |x + y| ≤ |x| + |y| := abs_add x y
The hint tactic (available after import Mathlib) suggests which tactics might close the current goal: 
example (x y : ℝ) (h : x > 0) (h2 : y > 0) : x + y > 0 := by
  hint  -- suggests: linarith, positivity, …

​
Tactic Taxonomy

Mathlib tactics fall into four broad categories. Each has its own documentation page.

Arithmetic

Decision procedures for numeric goals: linarith, nlinarith, omega, norm_num, ring, ring_nf, abel, field_simp.

Simplification

Term rewriting and normalization: simp, simp_rw, simp_all, norm_cast, push_cast, push_neg, gcongr.

Automation

General proof search and property provers: decide, native_decide, tauto, aesop, positivity, fun_prop, continuity, measurability.

Structural

Proof structure and decomposition: ext, use, obtain, rcases, induction, constructor, apply, exact, refine, by_contra, wlog, tfae_have.

​
Quick-Reference Tactic Grid

The table below lists the most-used tactics with a one-line description.
TacticWhat it does
linarithProves linear arithmetic goals over ordered rings
nlinarithExtends linarith to basic nonlinear arithmetic
omegaDecision procedure for ℕ/ℤ linear arithmetic, handles % and /
norm_numNormalizes and proves numeric expressions (primes, fractions, etc.)
ringProves equalities in commutative (semi)rings
abelProves equalities in additive commutative groups/monoids
field_simpClears denominators in field expressions
simpRewrites using @[simp]-tagged lemmas
simp_rwLike simp only but rewrites under binders
norm_castNormalizes numeric coercions (ℕ → ℤ → ℚ → ℝ)
push_negPushes ¬ through quantifiers and connectives
gcongrApplies congruence lemmas for inequality goals
decideEvaluates decidable propositions by kernel reduction
native_decideLike decide but compiles to native code
aesopGeneral proof search via forward/backward chaining + simp
positivityProves 0 ≤ e, 0 < e, or e ≠ 0
fun_propProves function properties (continuity, measurability, etc.)
extApplies extensionality lemmas tagged @[ext]
useProvides witnesses for existential goals
obtain / rcasesDestructures hypotheses by pattern matching
inductionInduction on an inductive type
by_contraIntroduces ¬ goal and switches to proving False
wlogReduces goal to a canonical case

​
The ? Variants

Many Mathlib tactics have a ? variant that, on success, prints a more explicit version of the call it used. This is invaluable for learning and for making proofs more robust: 
example (x y : ℝ) (h1 : x ≥ 1) (h2 : y ≥ 2) : x + y ≥ 3 := by
  linarith?
  -- Prints: Try this: linarith [h1, h2]

example (n : ℕ) : n + 0 = n := by
  simp?
  -- Prints: Try this: simp only [add_zero]
Using linarith? or simp? in finished proofs can slow down compilation. Replace the ? call with the printed suggestion once you are happy with the proof.

​
Further Reading

Build docs developers (and LLMs) love

Get started for freeTalk to us