6.1.1. The simp tactic🔗

The simp tactic is the workhorse of Lean automation. It applies a set of rewriting rules (called simp lemmas) repeatedly until no more rules apply. A lemma is marked as a simp lemma by adding the @[simp] attribute to it. Mathlib contains thousands of such lemmas.

Basic usage:

The variant simp only [...] restricts simp to use only the listed lemmas. This is preferred in Mathlib contributions because it makes proofs more robust against changes in the simp set.

The variant simp_all applies simp to all hypotheses and the goal simultaneously. This is more powerful than calling simp at * because simplifications in one hypothesis can unlock simplifications elsewhere.

Performance warning: The global simp call (without only) searches through all simp lemmas, which can be slow. In library code, prefer simp only. In interactive exploration, plain simp is fine. You can use simp? to find out which lemmas simp uses, and then replace simp by simp only [...].

6.1.2. The aesop tactic🔗

The aesop tactic (Automated Extensible Search for Obvious Proofs) performs a best-first tree search using a configurable set of rules. It can apply lemmas, split goals, use simp, and more. It is particularly good for goals involving set membership, basic logic, and algebraic structures.

You can register your own lemmas as aesop rules using the @[aesop] attribute:

@[aesop safe apply]   -- always try applying this lemma
@[aesop unsafe 50% apply]  -- try with 50% priority

6.1.3. The omega tactic🔗

The omega tactic decides linear arithmetic over ℕ and ℤ. It handles equalities, inequalities, divisibility, and modular arithmetic involving linear expressions. It cannot handle multiplication of variables (that is nonlinear).

Note that omega works on ℕ and ℤ but not on ℚ or ℝ. For those, use linarith.

6.1.4. The decide tactic🔗

The decide tactic works on decidable propositions -- propositions for which there is a computable decision procedure. This includes Boolean expressions, finite quantifiers, and computations on finite types.

Warning: decide runs a computation at kernel level. For large numbers, it can be extremely slow or time out. For example, Nat.Prime 104729 will take very long. In such cases, use norm_num instead.

6.1.5. The norm_num tactic🔗

The norm_num tactic normalizes numerical expressions. It can prove equalities and inequalities involving concrete numbers, and it has extensions for primality, divisibility, and more.

Unlike decide, norm_num uses verified computation and is much more efficient for numerical goals. It also works in types like ℝ and ℚ where decide does not apply.

6.1.6. The ring tactic🔗

The ring tactic proves equalities in commutative (semi)rings. It works with ℕ, ℤ, ℚ, ℝ, polynomial rings, and any type that has a CommRing or CommSemiring instance. It does not use hypotheses -- it only uses the ring axioms.

6.1.7. polyrith and linear_combination🔗

The linear_combination tactic proves an equality goal by providing a linear (or polynomial) combination of hypotheses. You supply the combination, and the tactic verifies it (usually via ring).

The polyrith tactic tries to find such a combination automatically by calling an external oracle. It then suggests a linear_combination call. This requires network access and may not always succeed.

6.1.8. The linarith tactic🔗

The linarith tactic proves linear arithmetic goals over ordered fields and rings. Unlike omega, it works over ℝ and ℚ, but it only handles linear expressions (no multiplication of variables).

For nonlinear goals, you can sometimes help linarith by providing auxiliary facts:

The variant nlinarith can sometimes handle nonlinear goals by trying to multiply hypotheses together.

6.1.9. The positivity tactic🔗

The positivity tactic proves goals of the form 0 ≤ e or 0 < e. It understands sums, products, powers, absolute values, norms, and more.

6.1.10. The gcongr tactic🔗

The gcongr (generalized congruence) tactic proves inequalities by matching the structure of both sides and reducing to component-wise inequalities. It is very useful for goals like "if a ≤ b and c ≤ d, then a + c ≤ b + d".

6.1.11. The field_simp tactic🔗

The field_simp tactic clears denominators and simplifies expressions involving division in a field. It is typically followed by ring to finish the proof.

Note that field_simp needs hypotheses that denominators are nonzero. It will look for these in the context.

6.1.12. Choosing the right tactic🔗

Here is a rough guide for choosing the right automation tactic:

When in doubt, try simp, then aesop, then more specialized tactics. Use simp? to discover which simp lemmas apply, and then switch to simp only for a more maintainable proof.

6.2.1. How Mathlib is organized🔗

The Mathlib source code lives in the Mathlib/ directory and is organized by mathematical area. Here are some of the main subdirectories:

• Mathlib.Algebra: groups, rings, fields, modules, linear algebra

• Mathlib.Analysis: real analysis, normed spaces, calculus, measure theory

• Mathlib.Topology: topological spaces, continuous maps, filters

• Mathlib.Order: partial orders, lattices, well-founded relations

• Mathlib.Data: concrete data types (Nat, Int, Rat, Real, Fin, List, Set, ...)

• Mathlib.Logic: basic logic, classical reasoning, choice

• Mathlib.SetTheory: ordinals, cardinals

• Mathlib.NumberTheory: primes, arithmetic functions, quadratic reciprocity

• Mathlib.MeasureTheory: measures, integration, probability

• Mathlib.CategoryTheory: categories, functors, natural transformations

• Mathlib.Combinatorics: graph theory, combinatorial identities

• Mathlib.Tactic: custom tactics (ring, norm_num, positivity, ...)

Within each directory, files are further organized by specificity. For example, Mathlib.Topology.Basic contains the definition of topological spaces, while Mathlib.Topology.MetricSpace.Basic specializes to metric spaces.

6.2.2. Searching for results: exact?, apply?, rw?🔗

Lean provides several tactics that search Mathlib for applicable lemmas. These are invaluable when you know what you need but do not know its name.

exact? searches for a single lemma (possibly with arguments) that closes the current goal. It will print a suggestion that you can copy into your proof.

apply? searches for a lemma whose conclusion matches the goal, possibly leaving subgoals.

rw? searches for a lemma that can rewrite part of the goal.

These tactics can be slow because they search through a large library. Use them during exploration, but replace them with the concrete result they find for your final proof.

6.2.3. Using #check, #print, and #search🔗

The commands #check and #print are fundamental for exploring the library interactively.

#check shows the type of a term or lemma:

#print shows the full definition of a term, including its proof:

If you are in VS Code, you can also use F12 (Go to Definition) to jump to the source code of any definition or lemma. This is one of the fastest ways to understand how something is defined.

6.2.4. External search tools: Moogle and Loogle🔗

When you cannot guess the name of a lemma, external search tools can help.

Loogle (loogle.lean-lang.org) lets you search Mathlib by type signature. For example:

• Searching for List.map shows all lemmas involving List.map

• Searching for _ + _ = _ + _ finds commutativity and related lemmas

• Searching for Continuous, Real.exp finds lemmas about continuity of exp

Moogle (moogle.ai) uses natural language search powered by AI. You can type queries like:

• "continuous function on compact set is bounded"

• "sum of convergent series"

• "every finite group is a quotient of a free group"

Both tools link directly to the Mathlib documentation and source code.

6.2.5. The Mathlib documentation website🔗

The official Mathlib documentation is available at the Mathlib docs site. It provides:

• A searchable index of all declarations

• Rendered source code with clickable cross-references

• Type signatures and docstrings

When browsing the docs, pay attention to the namespace. For example, Set.union_comm lives in the Set namespace, so you can use it as Set.union_comm or open Set and use union_comm.

6.2.6. Naming conventions in Mathlib🔗

Mathlib follows systematic naming conventions that make lemma names predictable once you know the pattern. The general rule is:

The conclusion is described first, then hypotheses are listed after _of_.

For example:

• continuous_add : continuity of addition (goal: Continuous ...)

• isOpen_of_isOpen_inter : a set is open given that some intersection is open

• le_of_lt : a ≤ b follows from a < b

Common abbreviations:

Common patterns:

• X_comm : commutativity (a * b = b * a)

• X_assoc : associativity ((a * b) * c = a * (b * c))

• X_zero / zero_X : interaction with zero (a * 0 = 0)

• X_one / one_X : interaction with one (a * 1 = a)

• X_self : applied to itself (a - a = 0)

• X_left / X_right : left/right variants

Examples:

Knowing these conventions lets you guess lemma names. For instance, if you need a + b - b = a, try add_sub_cancel. If you need the reverse direction of some iff, try appending .mpr or .mp.

6.2.7. Reading Mathlib source code🔗

When using a Mathlib lemma, it is often helpful to look at its source code to understand exactly what it says. Here are some tips:

1. Use F12 in VS Code to jump to the definition.

2. Read the type signature carefully. Implicit arguments (in {...}) are inferred by Lean. Instance arguments (in [...]) are resolved by typeclass search.

3. Look at the namespace. If a lemma is in namespace Foo, it can be used on terms of type Foo with dot notation: h.foo instead of Foo.foo h.

4. Check the imports. The file header tells you what dependencies the file has.

For example, consider:

This tells you: if s and t are finite sets, then s ∪ t is finite. Because it is in the Set.Finite namespace, you can also write hs.union ht if hs : Set.Finite s and ht : Set.Finite t.

6.2.8. Understanding implicit arguments and typeclass resolution🔗

Lean uses several kinds of argument brackets:

• (x : α) — explicit: you must provide this argument

• {x : α} — implicit: Lean infers this from context

• [inst : SomeClass α] — instance: resolved by typeclass search

• ⦃x : α⦄ — strict implicit: like {} but slightly different unification behavior

When applying a lemma, you usually only provide explicit arguments. If Lean cannot infer an implicit argument, you can provide it with @:

Typeclass resolution is the mechanism by which Lean automatically finds, for example, that ℝ is a CommRing or that ℕ has a LinearOrder. This works through a chain of instances registered with the instance command.

6.2.9. Managing dependencies with lake🔗

Lean projects use lake (Lean's build system and package manager) to manage dependencies. If you need Mathlib in your project, your lakefile.lean will contain something like:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "main"

Useful lake commands:

• lake build — build the project

• lake update — update dependencies

• lake exe cache get — download precompiled Mathlib .olean files (saves hours of compilation)

Always run lake exe cache get after updating Mathlib to avoid recompiling the entire library.

6.2.10. Common patterns in Mathlib proofs🔗

Here are some patterns you will see frequently in Mathlib and should adopt:

Pattern 1: Dot notation for structure projections and namespace lemmas.

Pattern 2: Anonymous constructor notation.

Pattern 3: calc blocks for chains of equalities or inequalities.

Pattern 4: suffices to restructure a proof by stating an intermediate goal.

Pattern 5: have for local forward reasoning, obtain for destructuring.

6.3.1. Universe issues🔗

Every type in Lean lives in a universe. The hierarchy is:

• Prop (also called Sort 0) — the universe of propositions

• Type 0 (also called Type) — the universe of "ordinary" types like ℕ, ℝ

• Type 1, Type 2, ... — higher universes

Most of the time, you do not need to think about universes. Problems arise when you write definitions that are universe-polymorphic and Lean cannot unify the universe levels.

Symptom: An error message mentioning universe level or Sort u_1.

Fix: Add explicit universe annotations. For example:

universe u v
variable {α : Type u} {β : Type v}

In practice, if you are working with concrete types (ℕ, ℝ, etc.) and Mathlib structures, universe issues are rare. They mostly appear when defining very general abstractions.

6.3.2. Coercion headaches🔗

In mathematics, we freely treat a natural number as an integer, a rational as a real, and so on. In Lean, these are different types, and moving between them requires coercions, written ↑ (or Nat.cast, Int.cast, etc.).

Lean inserts coercions automatically in many cases, but sometimes the coercion chain gets confused, especially when mixing several numeric types.

The standard coercion chain:

ℕ → ℤ → ℚ → ℝ → ℂ

Common problem: Your goal looks right, but it involves a mismatch between, say, (n : ℕ) and (↑n : ℤ), and tactics like ring or linarith fail because the types do not match.

Tactics for coercion issues:

• push_cast pushes coercions inward: it rewrites ↑(a + b) to ↑a + ↑b, ↑(a * b) to ↑a * ↑b, etc.

• pull_cast pulls coercions outward (the reverse direction).

• norm_cast normalizes cast expressions and can close goals involving casts.

• exact_mod_cast and apply_mod_cast are versions of exact and apply that handle casts automatically.

Tip: When working with mixed types, try to state everything in the "largest" type from the start. For example, if you are working with both ℕ and ℝ, cast to ℝ as early as possible and use push_cast and norm_cast to manage the casts.

6.3.3. Definitional equality surprises🔗

In Lean, some equalities hold by definition (definitional equality), while others require a proof (propositional equality). The distinction can be surprising.

When rfl works: rfl closes a goal a = b when a and b are definitionally equal. For example:

When rfl fails:

-- This does NOT work:
-- example (n : ℕ) : 0 + n = n := by rfl
-- Because Nat.add is defined by recursion on the first argument,
-- 0 + n is not definitionally equal to n.

The change tactic lets you replace the goal with a definitionally equal one:

The show tactic does the same thing but is more readable when used at the start of a proof:

Tip: If a tactic unexpectedly fails, try using change to rewrite the goal into an equivalent form. Sometimes the goal looks right in the Infoview but contains hidden definitional mismatches.

6.3.4. Typeclass diamonds🔗

A typeclass diamond occurs when there are two different paths to derive the same typeclass instance for a type, and these paths produce instances that are not definitionally equal.

For example, suppose ℤ gets a Monoid instance both directly and through CommRing → Ring → Monoid. If these produce different Monoid structures, Lean may complain about type mismatches.

Symptom: An error like "type mismatch" where the types look identical in the Infoview, or rfl fails on something that "obviously" should work.

How Mathlib avoids diamonds: Mathlib carefully designs its typeclass hierarchy so that diamonds are definitionally equal. This is one reason why the hierarchy is so carefully structured with extends and forgetful inheritance. When defining your own instances, follow the same patterns.

Practical advice: If you encounter a diamond, check whether you have defined a typeclass instance that conflicts with one from Mathlib. The fix is usually to ensure your instance agrees definitionally with the existing one, or to remove it and use the one from Mathlib.

6.3.5. Simp loop issues🔗

A simp loop occurs when two simp lemmas rewrite back and forth indefinitely. For example, if both a = b and b = a were simp lemmas, simp would loop forever.

Symptom: simp takes very long or times out.

How to diagnose: Use set_option trace.Meta.Tactic.simp true in before your tactic call to see which lemmas simp is applying. If you see the same lemma applied repeatedly, you have a loop.

-- Diagnose simp behavior:
-- set_option trace.Meta.Tactic.simp true in
-- example : ... := by simp

Prevention: When marking a lemma @[simp], ensure it rewrites toward a "simpler" or "canonical" form. The left-hand side should be more complex than the right-hand side. Never add both a = b and b = a as simp lemmas.

6.3.6. Dependent type complications🔗

Lean's type system is very expressive, but dependent types can cause headaches when types that "should" be equal are not definitionally equal.

The classic problem: You have h : a = b and want to rewrite in a type that depends on a. But after rewriting, the type of some term changes, and Lean complains about a type mismatch.

Tools for dealing with this:

• subst h : if h : a = b and a is a variable, this substitutes b for a everywhere.

• congr / congr 1 : tries to reduce an equality goal to equalities of the components.

• convert e : like exact e but allows the types to differ, generating subgoals for the mismatches.

• Eq.mpr and cast : explicitly transport a term along an equality of types (rarely needed in tactic mode).

HEq (Heterogeneous equality): Sometimes two terms have different types but you want to say they are "equal." This is what HEq provides. It should be avoided when possible, as it is harder to work with than Eq.

Practical advice: If you get stuck with dependent type issues, try:

1. Rewrite earlier so that types match before you build dependent terms.

2. Use convert instead of exact when the goal is almost right.

3. Use simp or congr to reduce the problem.

6.3.7. Timeout issues🔗

Lean has a computational budget measured in heartbeats. When a tactic or elaboration exceeds this budget, you get a timeout error.

Common causes:

• simp with too many lemmas or a simp loop

• decide on a large computation

• Typeclass search going through too many instances

• Deeply nested term elaboration

How to increase the budget (for debugging only):

set_option maxHeartbeats 400000 in
example : ... := by sorry

The default is 200000. Increasing it is a band-aid, not a solution. Find the root cause.

How to diagnose:

-- See what simp is doing:
set_option trace.Meta.Tactic.simp true in

-- See typeclass search:
set_option trace.Meta.synthInstance true in

-- Profile a tactic:
set_option profiler true in

6.3.8. Practical debugging tips🔗

Here is a collection of debugging techniques that every Lean user should know.

1. Use the Infoview. Always keep the Lean Infoview panel open in VS Code. Place your cursor after each tactic to see the current goal state. This is the single most important debugging tool.

2. Type annotations. When Lean gives a confusing error, add explicit type annotations to help it (and yourself) understand what is going on:

-- Instead of:
-- let x := f a
-- Write:
-- let x : ℝ := f a

3. #check everything. If you are not sure what type a lemma expects, #check it:

4. Binary search for errors. If a long proof breaks, comment out the bottom half and see if the top half is OK. Then narrow down. You can also replace a tactic with sorry to skip it temporarily.

5. trace options. Lean has many trace options for understanding what is happening:

6. Minimize the example. If you are stuck, try to create a minimal example that reproduces the issue. Remove all unnecessary hypotheses, imports, and context. This often reveals the problem.

7. Check Zulip. The Lean Zulip chat is an active community where you can ask questions. Search the archive first -- your question has likely been asked before.

8. Use conv for surgical rewriting. When rw rewrites in the wrong place, use conv to target a specific subexpression: