Reference material to consult as needed: the alphabetical glossary of
tactics; how a Lean file is organized (imports, namespaces, sections,
and scoping); how to navigate and search Mathlib; common pitfalls; and
a collection of short reference topics -- Lean's different brackets,
the kinds of equality, exploring definitions with #check/#print,
the diagnostic commands, and an alphabetical keyword reference.
This chapter is an alphabetical glossary: look up a tactic by name.
The everyday core. A handful of tactics do most of the work in most
proofs: exact (hand over the goal's proof term
directly), apply (reduce the goal to a lemma's
hypotheses), rw (rewrite with an equation or ↔),
intro (move a hypothesis into context), and
simp (simplify with known lemmas).
When you don't know what to use, ask. The search tactics propose a
step for you -- reach for them constantly: exact?
looks for a library term that closes the goal, apply?
for a lemma to apply, rw? for a rewrite that fits, and
simp? reports which simp lemmas fired (so you can then
switch to a robust simp only [...]).
Holes: _ versus ?_. Where a proof term is expected, you may leave
a hole. A plain _ asks Lean to infer that part -- it turns into a
goal only if inference fails. A ?_always leaves a new goal for you
to prove (and ?name labels it case name). This is exactly the
difference between exact and refine:
refine is exact that also tolerates ?_ holes.
Before the alphabetical list, here is a rough guide to which
automation tactic fits which kind of goal.
Goal type
Tactic
Numerical computation (2 + 3 = 5)
norm_num or decide
Linear arithmetic over ℕ, ℤ
omega
Linear arithmetic over ℝ, ℚ
linarith
Ring equality ((x+y)^2 = ...)
ring
Nonlinear inequality
nlinarith or positivity
Clearing denominators
field_simp then ring
Simplification with known lemmas
simp / simp only [...]
Mixed equality, arithmetic, case splits
grind
Set membership, basic logic
aesop
Monotonicity / congruence
gcongr
Equality from a combination of hypotheses
linear_combination
When in doubt, try simp, then grind or aesop, then a more
specialized tactic. Use simp? to see which simp lemmas apply and
switch to simp only for a robust proof.
Summary:aesop (Automated Extensible Search for Obvious Proofs)
performs a best-first tree search using a configurable set of rules.
In the course of a search it can apply lemmas, split goals, call
simp, and more. It is particularly effective on goals involving
set membership, basic logic, and routine structural reasoning.
You extend aesop by registering your own lemmas as rules with the
@[aesop] attribute, e.g. @[aesop safe apply] (always try this
rule) or @[aesop unsafe 50% apply] (try it with lower priority in
the search).
aesop is a search tactic: it explores many branches, so it can
be slower than a targeted tactic and its failures are less
predictable. It is a good first thing to try on an "obvious" goal.
For goals dominated by equalities, congruence, and arithmetic,
grind is often the better general tool; the two
complement each other.
applye tries to match the current goal against the conclusion of e's type.
If it succeeds, then the tactic returns as many subgoals as the number of premises that
have not been fixed by type inference or type class resolution.
Non-dependent premises are added before dependent ones.
The apply tactic uses higher-order pattern matching, type class resolution,
and first-order unification with dependent types.
Extensions:
apply(config:=cfg)e allows for additional configuration (see Lean.Meta.ApplyConfig):
newGoals controls which new goals are added by apply, in which order.
-synthAssignedInstances will not synthesize instance implicit arguments if they have been
assigned by isDefEq.
+allowSynthFailures will create new goals when instance synthesis fails, rather than erroring.
+approx enables isDefEq approximations (see Lean.Meta.approxDefEq).
Summary: There are already a lot of proven statements in Mathlib. When using apply?, Mathlib is searched for statements whose types correspond to those of the statement to be proved. If this is not successful, Lean reports a timeout. If successful, it also reports which commands were found. If you click on it, this is inserted in place of apply?.
Searches environment for definitions or theorems that can refine the goal using apply
with conditions resolved when possible with solve_by_elim.
The optional using clause provides identifiers in the local context that must be
used when closing the goal.
Use +grind to enable grind as a fallback discharger for subgoals.
Use +try? to enable try? as a fallback discharger for subgoals.
Use -star to disable fallback to star-indexed lemmas.
Use +all to collect all successful lemmas instead of stopping at the first.
assumption tries to solve the main goal using a hypothesis of compatible type, or else fails.
Note also the ‹t› term notation, which is a shorthand for showtbyassumption.
Summary:
If you have a term P : Prop as a hypothesis, by_cases hP : P returns two goals. The first one has hP : P, and the second one hP : ¬P. This tactic is thus identical to have hP : P ∨ ¬ P, exact em P, cases hP,. (The second expression is em : ∀ (p : Prop), p ∨ ¬p.)
Examples
Proof state
Tactic
New proof state
⊢ P
by_cases h : Q
h : Q ⊢ P h : ¬Q⊢ P
x : Bool ⊢ x = True ∨ x = False
by_cases x = True
x: bool h: x = True ⊢ x = True ∨ x = False x: bool h: ¬x = True ⊢ x = True ∨ x = False
The second example case-splits on a variable x : Bool; that type, Bool, is introduced in the chapter on the natural numbers.
Apparently, the by_cases tactic (just like by_contra) assumes that a statement is either true or false. This is also known as the law of excluded middle. In mathematics, proofs that do not use this rule are called constructive.
For terms of type Prop, the tactic tauto (or tauto!) can draw various conclusions from a truth table.
The by_contra tactic provides a proof by contradiction. It is therefore assumed (i.e. transformed into a hypothesis) that the statement (after ⊢) is not true, and this must be made to contradict itself, i.e. a proof of false must be found.
Examples
Proof state
Tactic
New proof state
⊢ P
by_contra h
h : ¬P ⊢ False
h: ¬¬P ⊢ P
by_contra hnegP
h: ¬¬P hnegP: ¬P ⊢ False
Remarks
This tactic is stronger than exfalso. After all, there the goal is only converted to false without adding a new hypothesis. With by_contra, the new goal is also false, but there is still a new hypothesis.
Summary: As the word suggests, calc is about concrete calculations. This is not a tactic, but a lean mode. This means that you can enter this mode (with the word calc) and enter calculation steps and proofs that each individual calculation step is correct.
Examples
Here is a proof of the first binomial formula that only comes about by rewriting of calculating properties from the mathlib.
proves a=z from the given step-wise proofs. = can be replaced with any
relation implementing the typeclass Trans. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with _.
calc
a = b := pab
_ = c := pbc
...
_ = z := pyz
It is also possible to write the first relation as <lhs>\n_=<rhs>:=<proof>. This is useful for aligning relation symbols, especially on longer
identifiers:
Summary: If a hypothesis is composed, i.e. can be expanded into two or more cases, cases' delivers exactly that. This can be used not only used with hypotheses h : P ∨ Q or h : P ∧ Q, but also with structures that consist of several cases, such as ∃... (here there is a variable and a statement) and x : bool or n : ℕ.
The application cases' n for n : ℕ is strictly weaker than complete induction (see induction). After all, cases only converts n : ℕ into the two cases 0 and succ n, but you cannot use the statement for n-1 to prove the statement for n.
A property of, say, the natural numbers, gives rise to Set ℕ by collecting all n : ℕ satisfying the property. In other words, P n and the membership n ∈ {m | P m} are equivalent.
Summary:choose f hf using h turns a hypothesis h : ∀ x, ∃ y, P x y into a functionf together with hf : ∀ x, P x (f x). It is the tactic form of choosing a witness for every input at once -- indispensable when you need to build a sequence or function from a family of existence statements (a constant move in analysis). It handles several ∀/∃ layers and extra conclusions in one call.
In fact, constructor is the same as refine ⟨?_, ?_⟩ (i.e. leaving two new goals). However, refine is more flexible since it is not bound to two variables:
When we have a property of the natural numbers, P : ℕ → Prop, {P // P m} is the subtype which consists of all m for which P m holds. Every (m : {P // P m}) is a pair ⟨m.val, m.prop⟩, where (m.val : ℕ) is its numerical value and m.prop is a proof for P m. So, we can construct a member of the subtype by giving a number n and a proof hn : P n. The constructor subtype_of_mem is the constructor for the subtype {m // P m}. It takes a number n and a proof hn : P n and returns the pair ⟨n, hn⟩.
Summary:contradiction closes the goal if the local context
contains two contradictory hypotheses, or a hypothesis of type
False, or h : a ≠ a, or similar trivially absurd facts.
Examples:
Proof state
Tactic
New proof state
h : False
contradiction
(no goals)
h₁ : P
contradiction
(no goals)
Remarks:
contradiction is usually faster and cleaner than exact absurd h h'
or exfalso; exact h' h.
It also recognises Nat.zero_ne_one-style contradictions and
evaluates numeric literals.
Summary:contrapose applies the contrapositive: given a goal
P → Q, it turns it into ¬Q → ¬P. The variant contrapose!
additionally pushes the negations inward using push_neg.
Examples:
Proof state
Tactic
New proof state
h : P ⊢ Q
contrapose h
h : ¬Q ⊢ ¬P
h : x ≤ y ⊢ f x ≤ f y
contrapose! h
h : f y < f x ⊢ y < x
Remarks:
contrapose (without !) simply inserts ¬. contrapose!
additionally runs push_neg on both the hypothesis and the goal,
so ¬(x ≤ y) becomes y < x and so on.
contrapose operates on a hypothesis by default; to contrapose the
goal only, use contrapose without an argument.
Summary:rw and simp rewrite the first matching subterm (and every copy of it), which is sometimes the wrong place -- and neither can reach under a binder such as ∀, ∃, or ∑. The conv tactic enters conversion mode: you first navigate to the exact subterm you mean, and only then rewrite it. Once focused, rw, simp, and change act only on the focused subterm.
Navigation inside conv => …:
lhs / rhs -- move into the left / right operand of an =, ↔, or binary operation.
enter [i, j, …] -- descend into argument i, then j, … of the focused term.
ext x -- go under a binder, introducing x; this is what lets you rewrite beneath ∀/λ/∑.
conv at h => … operates inside a hypothesis h instead of the goal.
the shorthands conv_lhs => … and conv_rhs => … start already focused on one side of the goal.
Examples:
Goal (with h)
Tactic
Effect
h : a = b ⊢ a + a = b + a
conv_lhs => lhs; rw [h]
rewrites only the firsta
h : ∀ n, f n = 0 ⊢ (fun n => f n) = 0
conv_lhs => ext n; rw [h]
rewrites under the λ
h : a + 0 = b
conv at h => lhs; rw [add_zero]
turns h into a = b
example(ab:ℕ)(h:a=b):a+a=b+a:=a:ℕb:ℕh:a=b⊢ a+a=b+aconv_lhs=>a:ℕb:ℕh:a=b| a;a:ℕb:ℕh:a=b| b
Summary:convert e closes the goal with eup to congruence: it matches the goal against the type of e and leaves the mismatched subterms as new equality goals. Reach for it when you have a proof of something that is almost the goal -- the two differ only in a few places. convert e using n limits how deep the matching descends: stopping after n layers gives fewer but larger leftover goals.
Summary:decide closes a goal whose statement is decidable --
i.e. the typeclass Decidable P finds a proof or refutation of P
by computation. Typical candidates are concrete arithmetic
equalities and inequalities, membership in a finite set, divisibility,
and propositional logic on concrete inputs.
Examples:
Proof state
Tactic
New proof state
⊢ (2 + 2 : ℕ) = 4
decide
(no goals)
⊢ (3 : ℕ) ∣ 12
decide
(no goals)
Remarks:
decide performs reduction: it reduces the decision procedure
on the given inputs. For large inputs it can be slow (or time
out); for general arithmetic, prefer omega or norm_num.
For propositions that depend on a variable (e.g. ∀ n, P n),
decide will not work -- it needs concrete inputs.
decide reduces the Decidable instance in the kernel, so whether
it succeeds depends on how that instance is implemented, not just on
the proposition being decidable. Mathlib's Decidable (IsSquare n),
for instance, uses Nat.sqrt, which the kernel does not reduce, so
decide gets stuck on IsSquare 2 -- even though it is perfectly
decidable. Giving the same proposition a kernel-reducible instance (a
bounded search) makes decide work again (see below). The underlying
class is the Decidable typeclass.
native_decide uses the compiled evaluator instead of kernel
reduction, so it closes goals like ¬ IsSquare 2 that decide
cannot -- at the cost of trusting the compiler (it enlarges the
trusted base).
Whether decide succeeds is a property of the instance, not just of the proposition. Mathlib's Decidable (IsSquare n) uses Nat.sqrt, which the kernel cannot reduce, so decide gets stuck. Supplying a kernel-reducible instance (a bounded search, here made to win by priority) closes the very same goals:
e < π is the opposite situation: a true statement whose only Decidable instance is the classical order on ℝ -- it depends on Classical.choice, so no instance can rescue it, and < on ℝ is not computably decidable at all.
example:Real.exp1<Real.pi:=⊢ Real.exp1<Real.piTactic `decide` failed for propositionReal.exp1<Real.pibecause its `Decidable` instance(Real.exp1).decidableLTReal.pidid not reduce to `isTrue` or `isFalse`.After unfolding the instances`Classical.propDecidable`, `LinearOrder.toDecidableLT`, and `Real.decidableLT`, reduction got stuck at the `Decidable` instanceClassical.choice⋯Hint: Reduction got stuck on `Classical.choice`, which indicates that a `Decidable` instance is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. The `decide` tactic works by evaluating a decision procedure via reduction, and it cannot make progress with such instances. This can occur due to the `open scoped Classical` command, which enables the instance `Classical.propDecidable`.⊢ Real.exp1<Real.pi
Here decide is simply the wrong tool: such a statement is proved, not decided -- for instance by squeezing it between rationals.
Summary: If the goal can be closed with a single command, then it can be closed with the exact tactic. Like many other tactics, exact also works with terms that are definitionally equal.
Examples:
Proof state
Tactic
New proof state
h : P ⊢ P
exact h
no goals
hP: P hQ: Q⊢ P ∧ Q
exact ⟨ hP, hQ ⟩
no goals
Remarks:
The related tactic exact? searches Mathlib for a term which closes the goal (and offers to insert it); it is the term-level counterpart of apply?.
If the proof consists of a single call of exact, it is easy to translate it to term mode; see easy proofs in term mode.
In the third example, note the order in which the two hypotheses hP and hnP are applied. The first hypothesis after exact is always the one whose right side matches the goal. If the goal requires further input, it is appended afterwards.
Summary: The statement false → P is true for all P. If the current goal is ⊢ P, and you would apply this true statement using apply, the new goal would be ⊢ false. This is exactly what the exfalso tactic does.
Examples:
Proof state
Tactic
New proof state
h : P ⊢ Q
exfalso
h : P ⊢ False
hP : P hnP : ¬P ⊢ Q
exfalso
hP : P hnP: ¬P ⊢ false
Remarks:
If you use this tactic, you leave the realm of constructive mathematics. (This dispenses with the rule of the excluded middle.)
exfalso is the same as apply False.elim; see the examples for exact.
Summary: Extensionality is a principle that states that two functions are equal if they give the same result for all arguments. The ext tactic applies this principle to prove the equality of two functions.
Summary:funext is the function extensionality tactic. To
prove a goal of the form f = g, where f g : (x : α) → β x are
two (possibly dependent) functions, funext x introduces a fresh
variable x : α and reduces the goal to f x = g x. This
relies on the funext axiom from Lean's type theory.
Examples:
Proof state
Tactic
New proof state
f g : ℕ → ℕ ⊢ f = g
funext n
f g : ℕ → ℕ
⊢ f n = g n
f g : (x : α) → β x ⊢ f = g
funext x
f g : (x : α) → β x
⊢ f x = g x
Remarks:
funext is a special case of the more general ext tactic. Use
funext when you specifically want to compare two functions
pointwise; use ext when the goal involves more than one layer
of extensionality (e.g. functions returning sets).
You can introduce several variables at once, e.g. funext x y to
reduce (fun x y ↦ f x y) = (fun x y ↦ g x y) to f x y = g x y.
Function extensionality. If two functions return equal results for all possible arguments, then
they are equal.
It is called “extensionality” because it provides a way to prove two objects equal based on the
properties of the underlying mathematical functions, rather than based on the syntax used to denote
them. Function extensionality is a theorem that can be proved using quotient
types.
Summary:field_simp clears denominators in a goal or hypothesis
involving a field (like ℚ, ℝ, ℂ). It rewrites expressions
of the form a / b into a common form, turning an equation between
rational expressions into one without division. Combined with
ring, it closes most identities in fields.
Examples:
Proof state
Tactic
New proof state
a b : ℝ
⊢ a / b + 1 = (a + b) / b
field_simp
a b : ℝ
⊢ a + b = a + b
Remarks:
field_simp typically needs nonzeroness hypotheses for every
denominator. These are taken from the context automatically, or
can be supplied with field_simp [h₁, h₂].
The idiomatic combination is field_simp; ring: field_simp
removes division, ring then finishes the algebraic identity.
It works over any Field, DivisionRing, or GroupWithZero.
Summary:filter_upwards is the workhorse tactic for proving
goals of the form ∀ᶠ x in F, P x. Given a list of Eventually
hypotheses, it intersects them, peels off the ∀ᶠ quantifier, and
leaves you with a pointwise goal in which all of the supplied
hypotheses appear specialized at the point x.
Examples:
Proof state
Tactic
New proof state
F : Filter α
⊢ ∀ᶠ x in F, p x ∧ q x
filter_upwards [h₁, h₂] with x hp hq
F : Filter α
⊢ p x ∧ q x
Remarks:
The list [h₁, h₂, ...] may be empty (filter_upwards []),
in which case the tactic only peels off the ∀ᶠ and leaves the
pointwise goal P x.
The with clause names the bound point and the specialized
hypotheses; if you omit it, fresh names are chosen automatically.
Use filter_upwards whenever you want to combine several
"eventually" facts and finish pointwise -- a very common pattern
in analysis and measure theory (where ∀ᶠ x ∂μ is "almost
everywhere").
It works for any filter, including atTop, nhds x, cofinite,
and μ.ae.
openFilterexample{α:Type*}{F:Filterα}{pq:α→Prop}(hp:∀ᶠxinF,px)(hq:∀ᶠxinF,qx):∀ᶠxinF,px∧qx:=α:Type u_1F:Filterαp:α→Propq:α→Prophp:∀ᶠ(x:α)inF,pxhq:∀ᶠ(x:α)inF,qx⊢ ∀ᶠ(x:α)inF,px∧qxfilter_upwards[hp,hq]withxα:Type u_1F:Filterαp:α→Propq:α→Prophp✝:∀ᶠ(x:α)inF,pxhq:∀ᶠ(x:α)inF,qxx:αhp:px⊢ qx→px∧qxα:Type u_1F:Filterαp:α→Propq:α→Prophp✝:∀ᶠ(x:α)inF,pxhq✝:∀ᶠ(x:α)inF,qxx:αhp:pxhq:qx⊢ px∧qxAll goals completed! 🐙
-- If p holds eventually along F and ∀ x, p x → q x,
-- then q holds eventually along F.
example{α:Type*}{F:Filterα}{pq:α→Prop}(hp:∀ᶠxinF,px)(h:∀x,px→qx):∀ᶠxinF,qx:=α:Type u_1F:Filterαp:α→Propq:α→Prophp:∀ᶠ(x:α)inF,pxh:∀(x:α),px→qx⊢ ∀ᶠ(x:α)inF,qxfilter_upwards[hp]withxα:Type u_1F:Filterαp:α→Propq:α→Prophp✝:∀ᶠ(x:α)inF,pxh:∀(x:α),px→qxx:αhp:px⊢ qxAll goals completed! 🐙
Summary:fun_prop is a general-purpose tactic for closing
function-property goals such as Continuous f, Measurable f,
Differentiable ℝ f, ContDiff ℝ n f, Integrable f, and others.
It works by recursively applying composition, linearity, and other
structural lemmas tagged @[fun_prop] in Mathlib.
Examples:
Proof state
Tactic
New proof state
⊢ Continuous (fun x : ℝ => x^2 + Real.sin x)
fun_prop
no goals 🎉
Remarks:
fun_prop subsumes and replaces the older continuity and
measurability tactics for most purposes.
For arguments it does not know about (e.g. the continuity of a
user-defined function), supply the fact as a hypothesis or add
a @[fun_prop] lemma.
When fun_prop fails, it will often report a helpful subgoal
indicating which atomic fact is missing.
Summary:gcongr ("generalized congruence") reduces a
monotonicity goal by peeling off a common outer context. It turns
a goal like f a + b ≤ f a' + b into a ≤ a' whenever f is
known to be monotone in its argument. It is the standard tool for
proving routine inequalities of compound expressions.
Examples:
Proof state
Tactic
New proof state
a a' b : ℝ
⊢ a + b ≤ a' + b
gcongr
a a' b : ℝ
⊢ a ≤ a'
Remarks:
gcongr relies on lemmas tagged @[gcongr] in Mathlib. Common
operations (+, *, ^, div, sum, ...) are already tagged,
so the tactic works out of the box in most situations.
After gcongr, the remaining goals are usually closed by
assumption, linarith, or positivity.
Summary:grind is a powerful general-purpose automation tactic
introduced into Lean 4 by the Lean FRO team. It is designed to close
goals that mix equational, propositional, and arithmetic
reasoning -- the kind of "obvious" side goals that a human would
consider routine but that no single specialized tactic handles. Its
design is inspired by SMT solvers (think of the engines inside Z3):
it does not search for a proof term by trial and error the way
aesop does, but runs a set of cooperating decision procedures until
they either close the goal or get stuck.
Under the hood grind combines several engines:
Congruence closure -- it maintains equivalence classes of terms
and knows that equal inputs give equal outputs, so from a = b it
derives f a = f b automatically.
Constraint propagation and case splitting -- it propagates the
consequences of hypotheses and splits on disjunctions,
if-conditions, and the constructors of inductive types.
A linear arithmetic procedure over Nat, Int, and ordered
fields, similar in spirit to omega/linarith.
E-matching -- it instantiates quantified lemmas by matching their
left-hand sides against terms present in the goal, using
patterns. This is how you teach grind new facts.
Constructor reasoning -- injectivity and no-confusion, so
some a = some b yields a = b, and some a = none is a
contradiction.
Examples:
example(f:Nat→Nat)(ab:Nat)(h:a=b):fa=fb:=f:ℕ→ℕa:ℕb:ℕh:a=b⊢ fa=fbAll goals completed! 🐙
-- chaining equalities
example(abc:Nat)(h1:a=b)(h2:b=c):a=c:=a:ℕb:ℕc:ℕh1:a=bh2:b=c⊢ a=cAll goals completed! 🐙
-- propositional reasoning with case splits
example(pq:Prop)(h:p∨q)(hp:¬p):q:=p:Propq:Proph:p∨qhp:¬p⊢ qAll goals completed! 🐙
-- injectivity of constructors
example(ab:Nat)(h:somea=someb):a=b:=a:ℕb:ℕh:somea=someb⊢ a=bAll goals completed! 🐙
-- a little linear arithmetic
example(ab:Int)(h1:a≤b)(h2:b≤a):a=b:=a:ℤb:ℤh1:a≤bh2:b≤a⊢ a=bAll goals completed! 🐙
When to reach for it.grind shines on goals that interleave a
handful of hypotheses, some case analysis, equalities, and a bit of
arithmetic -- exactly the situations where you would otherwise
write a tedious chain of rcases, simp, and omega. It is a
finishing tactic: point it at a goal you believe is true "for
obvious reasons".
Extending it. You register facts for grind with the @[grind]
attribute family; the tactic then instantiates them by E-matching
during the search. This is the analogue of @[simp] for the
simplifier, but the lemmas are used as logical facts rather than
rewrite rules.
What it does not do.grind does not perform induction, and
it is not a general nonlinear arithmetic engine. For goals needing
induction use induction; for polynomial identities use ring;
for pure linear arithmetic omega (over ℤ/ℕ) or linarith
(over ℝ/ℚ) are lighter and faster.
Cost. Because it runs several procedures and may split into many
cases, grind can be noticeably slower than a targeted tactic.
Prefer the specialized tactic when you already know which one
applies; keep grind for when the goal genuinely mixes several
kinds of reasoning.
Relation to aesop. Both are general automation, but with
different philosophies: aesop runs a customizable best-first
proof search applying registered rules, while grind runs
decision procedures with congruence closure and E-matching. When
one fails, the other is often worth a try.
Summary:nlinarith is the nonlinear extension of linarith.
Like linarith, it proves goals of the form a ≤ b, a < b,
a = b, or False from linear hypotheses over ordered fields.
Unlike linarith, it additionally multiplies pairs of hypotheses
to produce quadratic witnesses, so it can close many goals
involving products and squares.
Examples:
Proof state
Tactic
New proof state
x : ℝ ⊢ 0 ≤ x ^ 2 + 1
nlinarith [sq_nonneg x]
(no goals)
Remarks:
nlinarith is strictly more powerful than linarith but also
slower; prefer linarith when possible.
You can supply extra lemmas as hints:
nlinarith [sq_nonneg x, mul_self_nonneg y]. Hints of the form
0 ≤ ... are especially useful.
For purely polynomial identities (not inequalities), use ring
or polyrith instead.
Summary:norm_cast moves coercions outward, out of compound
expressions and towards the root of the term. This is the inverse
of push_cast, which moves coercions inward. Together they are
the standard tools for manipulating goals that mix integer, natural,
rational, and real coercions.
Examples:
Proof state
Tactic
New proof state
n : ℕ ⊢ (n : ℝ) + (1 : ℝ) = ((n + 1 : ℕ) : ℝ)
norm_cast
(no goals)
Remarks:
Use norm_cast when casts sit on atoms (e.g. (n : ℝ) + 1) and
you want to pull them outside. Use push_cast for the opposite
direction.
The variant exact_mod_cast h applies norm_cast automatically
before trying to close the goal with h.
Summary:omega is a decision procedure for linear arithmetic
over the integers ℤ and the natural numbers ℕ. It closes goals
involving +, -, * (by a constant), /, %, ≤, <, =,
≠, ∧, ∨, and ¬, provided the goal reduces to a Presburger
arithmetic statement. It is one of the most useful tactics for
closing routine numerical side conditions.
Examples:
Proof state
Tactic
New proof state
a b : ℕ
⊢ a ≤ b + 1
omega
(no goals)
n : ℕ
⊢ 0 < n
omega
(no goals)
Remarks:
omega is complete for linear arithmetic: if the goal is a true
statement in Presburger arithmetic, omega will close it.
It does not handle nonlinear products (use nlinarith) or
real-valued arithmetic (use linarith).
It works equally well on ℤ and ℕ, automatically handling the
fact that natural numbers are nonnegative.
Summary:polyrithfinds a linear combination of the equality
hypotheses that proves an equality goal, by sending the problem to an
external oracle (a Sage server) over the network. On success it
prints a concrete linear_combination
call, which you then paste into your proof.
Usage (not run here, as it needs network access):
example (x y : ℝ) (h1 : x + y = 3) (h2 : x - y = 1) :
x = 2 := by
polyrith
-- Try this: linear_combination (h1 + h2) / 2
Remarks:
polyrith requires network access and a working Python/Sage
backend, so it may be unavailable or fail; it is a discovery aid,
not something to leave in a finished proof.
Once it suggests a combination, replace the polyrith call with the
printed linear_combination so the proof is self-contained and
reproducible offline.
Summary:positivity proves goals of the form 0 < e, 0 ≤ e,
or e ≠ 0, where e is an arithmetic expression built from
literals and variables by operations that preserve positivity
(addition of nonnegatives, multiplication, powers, abs, exp,
square roots, ...).
Examples:
Proof state
Tactic
New proof state
x : ℝ
⊢ 0 < x ^ 2 + 1
positivity
(no goals)
Remarks:
positivity is extensible: any @[positivity]-tagged lemma in
Mathlib becomes available.
When a term depends on a variable whose sign is unknown but you
have a hypothesis 0 < y, positivity will pick it up
automatically.
Summary:push_cast pushes coercions (like Nat.cast,
Int.cast, Rat.cast) towards the leaves of an expression. It
turns ((a + b : ℕ) : ℝ) into (a : ℝ) + (b : ℝ), and similarly
for *, ^, etc. This is the inverse direction of norm_cast,
which moves casts outward.
Examples:
Proof state
Tactic
New proof state
n : ℕ ⊢ ((n + 1 : ℕ) : ℝ) = (n : ℝ) + 1
push_cast
n : ℕ ⊢ (n : ℝ) + 1 = (n : ℝ) + 1
Remarks:
Use push_cast when the cast sits outside a compound
expression and you want to distribute it; use norm_cast when
the casts sit on atoms and you want to pull them out.
The idiomatic combination for closing casting goals is
push_cast; ring (or push_cast; linarith).
Summary:ring_nf is the normal-form variant of ring. While
ringcloses a goal that is an identity in a (semi)commutative
ring, ring_nf instead rewrites both sides of the goal into a
canonical polynomial form. It is useful when ring does not close
the goal because it is not yet an equation (e.g. there are side
hypotheses) or when you want to simplify a hypothesis.
Examples:
Proof state
Tactic
New proof state
a b : ℝ
⊢ ...
ring_nf at h
a b : ℝ
⊢ ...
Remarks:
ring_nf never fails; it just rewrites.
Use ring to close a pure ring identity; use ring_nf to
normalize one side before continuing with another tactic.
You can target a hypothesis with ring_nf at h or normalize
everywhere with ring_nf at *.
Summary: By using have we introduce a new goal, which we have to prove first. Afterwards, it is available as a hypothesis in all further goals. This is identical to first proving a lemma h with the statement after have h : and then reusing it at the appropriate place in the proof (for example with apply or rw).
Examples:
Proof state
Tactic
New proof state
⊢ R
have h : P ↔ Q
⊢ P ↔ Q h : P ↔ Q ⊢ R
⊢ P
have h1 : ∃ (m : ℕ), f 27 m, ... cases h1 with m hm
m : ℕ hm: f 27 m ⊢ P
Remarks:
Assume you want to use have. You could as well formulate a separate lemma and use it afterwards. It is not always clear which is better.
If the proof of the statement is short and is only used once in your proof, you might want to consider replacing its proof in the place where it is needed.
Suppose we have two goals (let's call them ⊢ 1 and ⊢ 2), and we need the statement of ⊢ 1 in the proof of ⊢ 2. We can first introduce a third goal with have h := ⊢ 1 (where ⊢ 1 is to be replaced by the statement). Then ⊢ 1 can be proved with exact, and has the statement ⊢ 1 available in the proof of ⊢ 2.
The instance-cache variant haveI (and its value-keeping siblings letI and let) live in their own entry, let, letI, haveI -- filed under l.
Summary:hint runs a curated list of standard tactics -- among them simp, exact?, omega, linarith, decide, tauto -- on the current goal and reports in the infoview which of them close it. It does not change the proof state; it is a suggestion tool. When you are stuck and unsure what to try, hint is often the fastest way to find a one-line finish.
Example:
example (a b : ℕ) (h : a ≤ b) : a ≤ b + 1 := by
hint -- infoview: "Try these:" omega, linarith, …
omega -- then apply one of the suggestions
Notes
Because hint only reports, you still write the chosen tactic yourself -- unlike apply?/exact?, which offer an exact term to insert.
The list of tactics hint tries is configurable, but the defaults cover the common cases.
Inductive types allow the possibility of proving statements about them by means of induction. This includes, for example, the usual case of complete induction over natural numbers.
If the goal is of the form ⊢ P → Q or ∀ (n : ℕ), P n, you can proceed with intro P or intro n. You can use several intro commands at the same time to summarize a single one. A little more precisely, intro h1 h2 h3, is identical to intro h1; intro h2; intro h3.
If the goal is a disjunction ⊢ P ∨ Q, then left reduces it to ⊢ P -- it is exactly apply Or.inl, so it suffices to prove the left disjunct. Symmetrically, right reduces ⊢ P ∨ Q to ⊢ Q (apply Or.inr). More generally, for any goal whose type is an inductive with two constructors, left picks the first constructor and right the second.
Summary:let and have both introduce a local hypothesis, but they differ in what they remember. let x := e keeps the value: x is definitionally equal to e, so later steps may unfold x back to e. have h : P := e keeps only the typeP and forgets the term e, which becomes opaque. For proofs this is exactly right -- by proof irrelevance the particular term does not matter -- so use have for Props and let for data you will compute with.
The I-suffixed variants haveI and letI do the same for instances: they add the given term to the local instance cache, so that typeclass resolution can find it. haveI adds it opaquely, letI transparently (keeping the definitional value). Reach for them when you must supply a typeclass instance by hand in the middle of a proof.
Examples:
let keeps the value; have forgets it
example:(4:ℕ)=2+2:=⊢ 4=2+2x:ℕ:=2⊢ 4=2+2
-- x : ℕ := 2 (value kept: x unfolds to 2)
x:ℕ:=2⊢ 4=x+xAll goals completed! 🐙example:True:=⊢ Truey:ℕ:=2⊢ True
-- y : ℕ (only the type remains)
All goals completed! 🐙
Summary: This tactic can prove equations and inequalities with the help of hypotheses. It is important that the hypotheses used are also only equations and inequalities. So here we are working mainly with the transitivity of < together with arithmetic rules.
Summary:linear_combination proves an equality goal from
equality hypotheses. You supply an explicit linear (or polynomial)
combination of the hypotheses that equals the goal; the tactic
subtracts it from the goal and discharges the remainder with ring.
It is the tactic to reach for when linarith cannot help because the
goal is an equality that follows by algebraic manipulation.
You provide the coefficients; the tactic verifies them. Here
(h1 + h2) / 2 says "add the two equations and halve", which gives
exactly x = 2.
The leftover after subtracting your combination must be closed by
ring, so any polynomial identity in the coefficients is allowed,
not just linear ones.
If you do not know the combination, polyrith can
often find it for you and print a linear_combination call.
This tactic is related to rw. The difference is that you can specify the occurrence number of the term to be replaced on which rw is to be applied. The exact syntax is nth_rewrite k h, where k is the number (starting with $0$) of the term to be replaced and h is the hypothesis to be replaced. As with rw, this must be in the form h : x=y or h : A↔B.
Examples:
Proof state
Tactic
New proof state
n : ℕ ⊢ 0 + n = 0 + 0 + n
nth_rewrite 0 zero_add
n : ℕ ⊢ n = 0 + 0 + n
n : ℕ ⊢ 0 + n = 0 + 0 + n
nth_rewrite 1 zero_add
n : ℕ ⊢ 0 + n = 0 + n
n : ℕ ⊢ 0 + n = 0 + 0 + n
nth_rewrite 2 zero_add
n : ℕ ⊢ 0 + n = 0 + n
In the above example, Lean sees three terms of the form 0 + ?_: Number 0 is on the left-hand side, for numbers 1 and 2, on the right side (because of the parenthesis 0 + 0 + n = (0 + 0) + n), the second = is checked first. To the left of it is 0 + 0, which is by definition identical to 0. applying rw zero_add here, the term is converted to n. For number 2, you see 0 + 0, determine that it is of the desired form and convert it to 0.
Summary: In many steps of a proof, a negation must be carried out. In order to process the corresponding quantifiers etc. as well and to better reusable, the tactic push_neg is available.
Examples
Proof state
Tactic
New proof state
⊢ ¬(P ∨ Q)
push_neg
⊢ ¬P ∧ ¬Q
h : ¬(P ∨ Q)
push_neg at h
h : ¬P ∧ ¬Q
⊢ ¬(P ∧ Q)
push_neg
⊢ P → ¬Q
P : X → Prop ⊢ ¬∀ (x : X), P x
push_neg
P : X → Prop ⊢ ∃ (x : X), ¬P x
P : X → Prop ⊢ ¬∃ (x : X), P x
push_neg
P : X → Prop ⊢ ∀ (x : X), ¬P x
Notes:
This tactic also works with other objects, such as sets.
Summary:rcases is a more flexible version of cases. Here, it is allowed to use ⟨ hP, hQ ⟩ (or (hP | hQ)) to to split the hypotheses hP and hQ into their cases. As can be seen in the example above, it is also possible to nest ⟨.,.⟩ and (.|.).
Examples:
Proof state
Tactic
New proof state
h : P ∧ Q ⊢ R
rcases h with⟨ hP, hQ ⟩
+ hP : P {br}[]hQ : Q {br}[]⊢ R
* + h : P ∨ Q{br}[]⊢ R
+ rcases h with( hP | hQ )
hP : P ⊢ R hQ : Q ⊢ R
h : ∃ (m : ℕ) (hg : 0 ≤ m), m < n ⊢ P
rcases h with⟨m, h1, h2⟩
n m : ℕ h1 : 0 ≤ m h2 : m < n ⊢ 1 < n
Remarks:
The last example shows how to use rcases to directly resolve a ∃ quantifier in a hypothesis that has more than one constraint (here: 0 ≤ m) and m < n can be resolved directly.
An rcases pattern can be one of the following, in a nested combination:
A name like foo
The special keyword rfl (for pattern matching on equality using subst)
A hyphen -, which clears the active hypothesis and any dependents.
A type ascription like pat:ty (parentheses are optional)
A tuple constructor like ⟨p1,p2,p3⟩
An alternation / variant pattern p1|p2|p3
Parentheses can be used for grouping; alternation is higher precedence than type ascription, so
p1|p2|p3:ty means (p1|p2|p3):ty.
N-ary alternations are treated as a group, so p1|p2|p3 is not the same as p1|(p2|p3),
and similarly for tuples. However, note that an n-ary alternation or tuple can match an n-ary
conjunction or disjunction, because if the number of patterns exceeds the number of constructors in
the type being destructed, the extra patterns will match on the last element, meaning that
p1|p2|p3 will act like p1|(p2|p3) when matching a1∨a2∨a3. If matching against a
type with 3 constructors, p1|(p2|p3) will act like p1|(p2|p3)|_ instead.
Summary:refine is exact with holes: you give the proof term but leave some parts open as ?_, and each comes back as a new goal (for ?_ versus a plain _, see the note at the start of this chapter). This makes refine the tool for building a proof term outside-in -- state its shape now, discharge the pieces as separate goals. A named hole ?h labels its goal case h, which is convenient when several are open.
The most common use is to split a goal by naming the constructor or lemma that produces it and leaving its arguments as holes -- an anonymous constructor ⟨…⟩ for an ∧, ↔, ∃, structure, or subtype, or a lemma such as le_antisymm for an equality.
Summary:revert is the opposite of intro: It takes a hypothesis from the local context and inserts it as a precondition into the goal.
Examples
Proof state
Tactic
New proof state
h : P ⊢ Q
revert hP
⊢ P → Q
Remarks:
revert is rarely needed; actually only when you want to apply an already proven result exactly and first want to establish the correct form of the goal.
This tactic applies to a goal whose target has the form x~x, where ~ is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
The implementation of the rintro tactic. It takes a list of patterns pats and
an optional type ascription ty? and introduces the patterns, resulting in zero or more goals.
Summary:rw stands for rewrite. For rw h to work, h must be an expression of the type h : x=y or h : A↔B. In this case, rw h replaces every term that is syntactically identical to x (or A) is replaced by y (or B). This also works if h is an already proven result (i.e. a lemma or theorem). With rw ← h is applied from right to left. (In the above example, y is replaced by x and B by A.)
Examples
Proof state
Tactic
New proof state
h : P ↔ Q ⊢ P
rw [h]
h : P ↔ Q ⊢ Q
h : P ↔ Q ⊢ Q
rw [← h]
h : P ↔ Q ⊢ P
h : P ↔ Q hP : P
rw [h] at hP
h : P ↔ Q hP : Q
h : P ↔ Q hQ : Q
rw [← h] at hQ
h : P ↔ Q hQ : P
k m: ℕ ⊢ k + m + 0 = m + k + 0
rw [add_comm]
k m : ℕ ⊢ 0 + (k + m) = m + k + 0
k m : ℕ ⊢ k + m + 0 = m + k + 0
rw [add_comm k m]
⊢ m + k + 0 = m + k + 0
k m : ℕ ⊢ k + m + 0 = m + k + 0
rw [← add_comm k m]
⊢ k + m + 0 = k + m + 0
k m : ℕ ⊢ k + m + 0 = m + k + 0
rw [add_zero, add_zero]
k m : ℕ ⊢ k + m = m + k
For the last four examples, you first need to know that addcomm and addzero are the statements
lemma add_comm : ∀ {G : Type} [_inst_1 : add_comm_semigroup G] (a b : G),
a + b = b + a
add_zero : ∀ {M : Type} [_inst_1 : add_zero_class M] (a : M), a + 0 = a
In the first of the four examples, rw applies to the first occurrence of a term of type a + b. Due to the internal bracketing, (k + m) + 0 is on the left side, so that the rw results in a 0 + k + m. If you want to use the commutativity in the term k + m, you need the second (or third) example, where rw add_comm k m leads to the desired progress. In the last example, the two + 0 terms are first eliminated by rw add_zero.
Notes
rw is used very often in practice to apply statements from the mathlib (at least if they are of the type = or ↔).
If you want to combine several rw commands, you can do so in square brackets, for example rw [h1, h2] or rw [h1, ←h2, h3].
rw immediately executes a refl after its application. This leads to the second and third examples of the applications of add_comm and add_zero that the new proof state is not as specified, but no goals.
If you do not want to perform a rw in sequence (as in the double elimination of the +0 above), you can use nth_rewrite to rewrite the second occurrence of a term.
The rw tactic does not work when it comes after a binder, which could be a ∀ ∃ ∑. In this case, simp_rw will hopefully help.
rw?searches for a rewrite that applies to the goal: it lists library equations and ↔-statements whose left- (or, with ←, right-) hand side matches a subterm, and you pick one. Useful when you are sure a rewrite should exist but do not know its name.
Summary:set x := e introduces a local abbreviation x for the
expression e and substitutes every occurrence of e in the goal
(and, with the with clause, in the hypotheses) with x. The
substitution is definitional: x and e are interchangeable, but
the proof state becomes much more readable.
Examples:
Proof state
Tactic
New proof state
a b : ℕ ⊢ a + b + (a + b) = 2 * (a + b)
set s := a + b with hs
a b : ℕ s : ℕ := a + b hs : s = a + b ⊢ s + s = 2 * s
Remarks:
Without with hs, no equation hypothesis is introduced, and x
is still definitionally equal to e.
set is very useful when you want to rw with a complicated
subterm, or when reading the goal becomes difficult.
The dual let x := e introduces a let-binding into the term but
does not fold the expression in the goal.
Summary:show e changes the syntactic form of the current goal
to e, provided e is definitionally equal to the goal. It is
the tactic counterpart of the term-mode (h : T) ascription.
Examples:
Proof state
Tactic
New proof state
⊢ 1 + 1 = 2
show 2 = 2
⊢ 2 = 2
⊢ P ∨ Q
show Q ∨ P
(fails: not def-equal)
Remarks:
show does not prove anything; it only reshapes the goal. It is
useful before rw, apply, or exact when those tactics expect
a specific syntactic shape.
show e fails if e is not definitionally equal to the goal.
For propositional reshaping (which is not definitional) use
change or suffices.
Summary: In mathlib there are many lemmas with = or ↔ statements that can be applied with rw and are marked with @[simp]. These marked lemmas have the property that the right side is a simplified form of the left side. With simp, lean looks for matching lemmas and tries to apply them.
Examples
Proof state
Tactic
New proof state
⊢ n + 0 = n
simp
no goals 🎉
h : n + 0 = m ⊢ P
simp at h
h : n = m ⊢ P
Remarks:
If you want to know which lemmas were used, try simp?. This provides some clues.
Proof state
Tactic
New proof state
⊢ n + 0 = n
simp?
no goals 🎉 Try this: simp only add_zero, eq_self_iff_true
Summary:simp_all simplifies the goal and every hypothesis at once, using the hypotheses as additional simp lemmas and repeating until nothing changes. It is stronger than simp at *: because each simplified hypothesis feeds back in, it often closes goals that need several facts to interact.
Summary:simp_rw [h₁, h₂, ...] rewrites with each lemma in turn,
but -- unlike rw -- can rewrite under binders (∀, ∃, fun,
∑, ...). Unlike simp, it does not apply any extra simp lemmas;
it rewrites with exactly the lemmas you supply.
Examples:
Proof state
Tactic
New proof state
f : ℕ → ℕ
simp_rw [h]
⊢ ∀ n, 0 + 1 = 1
Remarks:
rw refuses to rewrite under binders, giving a "motive is not
type correct" error in those situations. simp_rw is the right
tool there.
If the lemmas you rewrite with are simp lemmas and you are happy
for simp to apply other simp lemmas too, just use simp only.
Summary: In a hypothesis h : ∀ n, ..., ... applies to all n, but for the proof of the goal, you may only need a specific n. If you specify specialize h followed by the value for which h is needed, the hypothesis changes accordingly.
Just as with use, you have to be careful that the goal remains provable.
If you want to use two values of the hypothesis h, then let h' := h first provides a duplication of the hypothesis, so that you can then apply specialize to h and h'.
Summary:symm swaps the two sides of a symmetric relation.
For equality, it turns a goal a = b into b = a. It also works
for ↔, ≃, Dvd.dvd, and any other relation tagged @[symm]
in Mathlib.
Examples:
Proof state
Tactic
New proof state
a b : ℕ ⊢ a = b
symm
a b : ℕ ⊢ b = a
h : a = b ⊢ ...
symm at h
h : b = a ⊢ ...
Remarks:
The term-mode analogue is Eq.symm h (or .symm).
symm is often used just before exact h when you have h : b = a
but a goal a = b.
Summary:tauto solves all goals that can be solved with a truth table.
Examples
Proof state
Tactic
New proof state
⊢ P ∧ Q → P
tauto oder tauto!
No goals
⊢ ((P → Q) → P) → P
tauto!
No goals
The truth tables for ¬P, P ∧ Q and P ∨ Q are as follows; if more terms of type Prop are involved, there are more lines.
P
¬P
true
false
false
true
P
Q
(P ∧ Q)
true
true
true
false
true
false
true
false
false
false
false
false
P
Q
(P ∨ Q)
true
true
true
false
true
true
true
false
true
false
false
false
Notes
The difference between tauto and tauto! is that in the latter tactic, the rule of the excluded middle is allowed. The second example can therefore only be solved with tauto!, but not with tauto.
Summary:trans b proves a transitive goal a R c -- for =, ≤, <, ⊆, ∣, and any relation with a registered Trans instance -- by splitting it into the two goals a R b and b R c for a middle term b you supply. It is the transitivity counterpart of symm.
Summary:trivial tries a short list of simple tactics to close
the goal: rfl, assumption, True.intro, decide, and a few
others. It is a gentle hammer for goals that "should be obvious".
Examples:
Proof state
Tactic
New proof state
⊢ True
trivial
(no goals)
h : P ⊢ P
trivial
(no goals)
Remarks:
Unlike triv, trivial also closes goals that are true by
decidability (like 2 + 2 = 4).
When trivial does not close a goal, it prints no specific
reason -- if you want a more informative automated tactic, try
exact? or simp.
Summary:unfold f replaces the constant f by its definition in the goal (unfold f at h in a hypothesis). It works on defs by rewriting with their equation lemmas, so it also unfolds functions defined by pattern matching.
Example:
defmyDbl(n:ℕ):ℕ:=2*n
-- `ring` cannot see through `myDbl`; unfold it first
example(n:ℕ):myDbln=n+n:=n:ℕ⊢ myDbln=n+nn:ℕ⊢ 2*n=n+nAll goals completed! 🐙
If the two sides are already definitionally equal after unfolding, rfl alone often suffices -- unfold just makes the step explicit.
simp only [myDbl] unfolds via the same equation lemmas and is frequently more robust; show or change can also replace the goal with an unfolded, definitionally-equal form.
Summary: The use tactic is used for goals that begin with ∃. Here, parameters are used to indicate which object quantified by ∃ is to be reused in the proof.
Examples
Proof state
Tactic
New proof state
⊢ ∃ (k : ℕ), k * k = 16
use 4
⊢ 4 * 4 = 16
⊢ ∃ (k l : ℕ), k * l = 16
use 8, 2
⊢ 8 * 2 = 16
In this example, Lean knows that 4 * 4 = 16 by rfl, so we need not type it.
Summary:wlog h : P with H formalizes "without loss of generality, assume P". It produces two goals:
a reduction goal, where you are handed H -- the full statement, generalized over the relevant variables -- and must prove the goal in general, typically by applying H to a swapped/symmetric instance to cover the case ¬P;
the main goal, where you may now assume h : P.
Example: commutativity of +, reduced to the case a ≤ b:
A Lean file is a sequence of commands -- def, theorem,
structure, #check, and so on -- processed top to bottom. It opens
with its imports, which pull in other files, and then a handful of
keywords organize the rest and control where the names they
introduce are visible: namespace, open, section, variable, and
the scope modifiers private, local, and scoped. This appendix
collects them in one place.
Every Lean file begins with its imports. Writing import Foo.Bar
makes the contents of the module Foo/Bar.lean available in the
current file, and imports are transitive -- importing a module also
brings in everything that module itself imports. All import lines
must come first, before any other command; an import after the
first def or #check is a syntax error.
The module name mirrors the file path: import Mathlib.Order.Basic
refers to Mathlib/Order/Basic.lean. Importing the umbrella module
Mathlib pulls in the entire library at once -- convenient for
exploration, though slower to load -- whereas a targeted import brings
in only what you need:
import Mathlib.Order.Basic -- just one module
import Mathlib -- the whole library
Every chapter file in this course opens with import Mathlib (plus a
few Verso modules), which is why any Mathlib lemma is available in the
examples without further ceremony.
A namespace groups related declarations under a common prefix.
Inside namespace Foo ... end Foo, every declaration bar is really
named Foo.bar. Every structure and inductive type also opens a
namespace of its own name automatically.
namespaceGeostructurePointwherex:Floaty:Float
-- written inside `namespace Geo`, so its full name is
-- `Geo.translate`
deftranslate(p:Point)(dxdy:Float):Point:={x:=p.x+dx,y:=p.y+dy}endGeo
-- outside the namespace we use the qualified names
Geo.Point:Type#checkGeo.Point11.000000#eval(Geo.translate⟨1.0,2.0⟩10.020.0).x -- 11.0
Because the first explicit argument of translate has type
Geo.Point, dot notation works: for p : Geo.Point, writing
p.translate 10.0 20.0 resolves to Geo.translate p 10.0 20.0.
Namespaces are the reason dot notation is so pervasive in Mathlib.
A section groups commands and, crucially, delimits the scope of
variable declarations. A variable introduces a parameter that
several declarations share, without repeating it in each signature;
Lean adds it only to the declarations that actually use it.
sectionvariable(n:ℕ)defaddN(m:ℕ):ℕ:=m+ndefmulN(m:ℕ):ℕ:=m*nend
-- outside the section `n` is gone; it became an argument
addN : ℕ→ℕ→ℕ#check@addN -- addN : ℕ → ℕ → ℕ
Sections may be named (section Foo ... end Foo) and nested; the name
is only a readability aid that must match the closing end. A file
also has an implicit top-level section, so variables written outside
any explicit section last until the end of the file.
3.2.5. Scope of definitions: private, local, scoped🔗
By default a def is visible in every file that imports it (using its
qualified name, or unqualified after open). Three modifiers narrow
that reach:
private def f ... -- visible only within the current file.
local notation ... / local instance ... -- visible only until the
end of the current section or file.
scoped notation ... / scoped instance ... -- visible only when the
enclosing namespace is opened (with open or open scoped).
The scoped modifier is how Mathlib ships heavy notation -- ∑, ∏,
the ℝ≥0 shorthand -- without polluting global scope: you get the
notation exactly when you ask for it by opening the relevant namespace.
namespace BigOps
scoped notation "⟦" x "⟧" => (x, x)
end BigOps
-- `⟦·⟧` is unavailable here until we opt in:
open scoped BigOps
#check (⟦3⟧ : ℕ × ℕ) -- (3, 3)
Together, these keywords let a Lean file stay organized and keep each
name visible exactly where it is wanted -- no more and no less.
Mathlib is the community-maintained mathematical library for Lean 4. It contains hundreds of thousands of lines of formalized mathematics, covering algebra, analysis, topology, measure theory, number theory, combinatorics, and more. Learning to navigate Mathlib effectively is essential for writing proofs that build on existing results rather than reinventing the wheel.
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.
3.3.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 its hypotheses as new subgoals.
-- Goal `a ≤ b`, with `h : a < b` in context. Try:
example (a b : ℝ) (h : a < b) : a ≤ b := by apply?
-- suggests: exact le_of_lt h
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.
3.3.3. Searching by type shape or in natural language🔗
When you cannot guess a lemma's name, several search services help. (For the #check/#print/inferInstance commands that inspect a known definition, see Exploring definitions earlier in this appendix.) All of the services below are available both as web pages and, more conveniently, as commands inside Lean via the LeanSearchClient package (a Mathlib dependency).
Loogle (loogle.lean-lang.org) searches by type shape. You write a pattern (using _ for holes) and Loogle returns every lemma whose statement unifies with it. Inside Lean:
#loogle (?a + ?b) * ?c = _
It also accepts a comma-separated list of constants that must appear, e.g. #loogle Real.exp, Real.log, or a target conclusion #loogle |- tsum _ = _.
LeanSearch (leansearch.net) searches by natural language. From inside Lean:
#leansearch "the derivative of a product of functions"
Moogle (moogle.ai) is another natural-language search with a different ranking model:
#moogle "bolzano-weierstrass"
The two often surface different lemmas, so it is worth trying both.
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.
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:
Full name
Abbreviation
addition
add
multiplication
mul
subtraction
sub
division
div
negation
neg
inverse
inv
commutativity
comm
associativity
assoc
left
left
right
right
if and only if
iff
less than
lt
less or equal
le
greater than
gt
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:
mul_comm.{u_1}{G:Type u_1}[CommMagmaG](ab:G):a*b=b*a#checkmul_comm -- a * b = b * a
add_assoc.{u_1}{G:Type u_1}[AddSemigroupG](abc:G):a+b+c=a+(b+c)#checkadd_assoc -- (a + b) + c = a + (b + c)
MulZeroClass.mul_zero.{u}{M₀:Type u}[self:MulZeroClassM₀](a:M₀):a*0=0#checkmul_zero -- a * 0 = 0
sub_self.{u_1}{G:Type u_1}[AddGroupG](a:G):a-a=0#checksub_self -- a - a = 0
le_of_lt.{u_1}{α:Type u_1}[Preorderα]{ab:α}(hab:a<b):a≤b#checkle_of_lt -- a < b → a ≤ b
lt_of_le_of_lt.{u_1}{α:Type u_1}[Preorderα]{abc:α}(hab:a≤b)(hbc:b<c):a<c#checklt_of_le_of_lt -- a ≤ b → b < c → a < c
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.
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:
Use F12 in VS Code to jump to the definition.
Read the type signature carefully. Implicit arguments (in {...}) are inferred by Lean. Instance arguments (in [...]) are resolved by typeclass search.
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.
Check the imports. The file header tells you what dependencies the file has.
For example, consider:
Set.Finite.union.{u}{α:Type u}{st:Setα}(hs:s.Finite)(ht:t.Finite):(s∪t).Finite#checkSet.Finite.union
-- Set.Finite.union : Set.Finite s → Set.Finite t → Set.Finite (s ∪ t)
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.
3.3.7. 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 @:
add_comm35 : 3+5=5+3#check@add_commℕ_35 -- explicitly providing the type and the arguments
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.
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.
3.3.10. Getting more help: Zulip and AI assistants🔗
Beyond automated search, two more resources are worth knowing.
Zulip (leanprover.zulipchat.com, the #new members and #Mathlib4 streams) is the community chat. For questions that no search answers, posting a minimal example together with the goal you are stuck on almost always gets a helpful reply within hours.
AI assistants (ChatGPT, Claude, Gemini, Copilot, and the Lean-focused tools built on them) have become surprisingly effective at suggesting lemma names, explaining why a tactic fails, and translating informal arguments into Lean. They are fallible -- they will cheerfully invent lemmas that do not exist or quote outdated Mathlib 3 syntax -- so use them critically: paste your goal state and the surrounding example, ask for a couple of candidate approaches, and verify each suggestion in Lean (via exact?, #loogle, or by compiling it). Treat AI output like a confident but occasionally wrong colleague.
As a rule of thumb: try exact? / apply? first (they know your exact proof state), then #loogle (precise, fast), then #leansearch / #moogle or an AI assistant (when you do not know the vocabulary Mathlib uses), and finally the docs or Zulip for open-ended questions.
Even experienced Lean users regularly run into frustrating situations where a proof that "should" work simply does not. This section catalogs the most common pitfalls and gives practical advice for diagnosing and fixing them.
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.
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.
norm_cast normalizes cast expressions (moving coercions outward and simplifying) 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.
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:
example:2+3=5:=⊢ 2+3=5All goals completed! 🐙 -- Lean computes this
example(n:ℕ):n+0=n:=n:ℕ⊢ n+0=nAll goals completed! 🐙 -- by definition of Nat.add
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:
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.
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.
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.
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:
Rewrite earlier so that types match before you build dependent terms.
Use convert instead of exact when the goal is almost right.
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
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:
mul_le_mul_of_nonneg_left.{u_1}{α:Type u_1}[Mulα][Zeroα][Preorderα]{abc:α}[PosMulMonoα](hbc:b≤c)(ha:0≤a):a*b≤a*c#checkmul_le_mul_of_nonneg_left
-- ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b c : α},
-- a ≤ b → 0 ≤ c → c * a ≤ c * b
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:
There are (essentially) three different types of parentheses in Lean statements. The simplest is (...), which, as in normal use, indicates parentheses in the sense of what belongs together. However, you have to learn how Lean brackets internally when no '()' are given. Operators like and (∧), or (∨), are right-associative, so e.g. P ∧ Q ∧ R := P ∧ (Q ∧ R). The application of functions in sequence, such as f : ℕ → ℝ and g : ℝ → ℝ , applied to n : ℕ is g (f n), because g expects an input of type ℝ, and this is what f n provides. You cannot omit (...), i.e. in this case the parenthesis is left-associative.
Beyond grouping, Lean uses four kinds of binder brackets in a declaration's signature; they differ in who supplies the argument, and how:
Bracket
Kind
Who fills it in
(x : α)
explicit
you, at every call
{x : α}
implicit
Lean, by unification (from the other arguments), eagerly
⦃x : α⦄ (or {{x : α}})
strict implicit
Lean, by unification -- but only once a following explicit argument is supplied
α sits in {} because Lean infers it from the type of the explicit x; Add α sits in [] because it is found by instance search; only x must be given at the call. Real Mathlib lemmas read the same way:
@gt_iff_lt : ∀{α:Type u_1}[inst:LTα]{xy:α},x>y↔y<x#check@gt_iff_lt
-- @gt_iff_lt : ∀ {α : Type u_1} [inst : LT α] {x y : α}, x > y ↔ y < x
Here {α}, [inst : LT α] and {x y} are all supplied automatically, so you write just gt_iff_lt (or apply it to concrete x, y).
Both {} and ⦃⦄ are implicit -- Lean fills them in -- but they differ in when. A regular implicit {x} is solved eagerly, the moment the function is mentioned. A strict implicit ⦃x⦄ (also written {{x}}) is solved only when a following explicit argument is actually supplied; until then the binder stays put.
In ordinary use the difference is invisible (idImp 5 and idStrict 5 both give 5). It matters when a function is used without its explicit argument -- exactly the situation for ⊆. Mathlib defines s ⊆ t as ∀ ⦃a⦄, a ∈ s → a ∈ t with a strict implicit a, so that from h : s ⊆ t you may apply h directly to a membership proof:
example(st:Setℕ)(h:s⊆t)(a:ℕ)(ha:a∈s):a∈t:=hha
Had a been an ordinary implicit, mentioning h alone would have eagerly forced a metavariable for a, making h ha more awkward. Strict implicits keep such "apply me later" arguments out of the way until a real argument pins them down.
Due to the multitude of types in Lean, we have to be careful about equality. In Lean, there are three types of equality:
Syntactic equality: If two terms are letter-for-letter equal, then they are syntactically equal. However, there are a few more situations in which two terms are syntactically equal. Namely, if one term is just an abbreviation for the other (for example, x = y is an abbreviation for Eq x y, where Eq is a function which takes two terms of the same type, and assigns True if they are the same and False otherwise), then these both terms are syntactically equal. Also equal are terms in which globally quantified variables have different letters. For example, ∀ x, ∃ y, f x y and ∀ y, ∃ x, f y x are syntactically equal.
Definitional equality: Some terms are equal by computation -- Lean reduces both to a common form. For example, for x : ℕ, x + 0 reduces to x, whereas 0 + x does not (an asymmetry that comes from how Nat addition is defined). This notion, the reduction rules that generate it, and the cases where rfl gets stuck, are developed in full in the reduction-rules section of the chapter on the natural numbers.
Propositional equality: If there is a proof of x = y, then x and y are said to be propositionally equal; likewise P and Q are propositionally equal when you can prove P ↔ Q. This is the equality you state and rewrite with in everyday mathematics.
The distinction matters because tactics differ in which equality they respect -- some see through it, some do not. rfl, exact, and apply accept a term whenever it is merely definitionally equal to what is expected (they run the reductions for you), whereas rw matches syntactically and will not fire unless the subterm literally appears. Many otherwise-puzzling tactic failures come down to exactly this.
There is a special kind of equality to be observed with sets and functions. For example, two functions are exactly the same if they return the same value for all values in the domain. This behavior is called extensionality in the theory of programming languages. (If extensionality applies, then, for example, two sorting algorithms are the same if they always produce the same result).
3.5.3. Exploring definitions with #check, #print and inferInstance🔗
Lean provides a handful of commands that are invaluable for exploring
a library like Mathlib. They all start with # and only print
information -- they do not contribute to a proof.
#check e prints the type of the term or expression e. This is
the fastest way to learn what a lemma says, or what type a definition
has.
#check @lemma (with a leading @) prints the type of the lemma
without hiding implicit and instance arguments. Use @ when you
want to see every argument.
#print name prints the definition of the constant name. For a
typeclass, this shows you the list of fields; for a def, the body;
for a structure, the constructor and fields.
#eval e evaluates the term e (when it is computable) and prints
the result. It works on concrete ℕ, List, etc., but not on
abstract propositions.
The term inferInstance asks Lean to synthesize an instance of a
stated type -- a quick way to ask "does this type have that
structure?". If no such instance exists the command fails with a
readable error. See the Typeclass chapter
for the details and an example.
Two tactics complement these commands during an interactive proof:
exact? searches Mathlib for a single lemma that closes the current
goal and prints a exact <lemma> line you can copy.
apply? is the same, but it suggests lemmas whose conclusion
matches the goal, leaving side conditions as new subgoals.
Together, #check, #print, inferInstance, exact? and apply?
are the main tools for navigating an unfamiliar part of Mathlib; for
searching the library by content or name, see
Navigating Mathlib.
These commands inspect your work without changing it: they report a
theorem's logical dependencies, suggest where a definition should
live, and run the library's quality checks. Unlike the #-commands
in the Lean basics chapter (#check, #eval, #print), these are
mostly about engineering a clean, well-placed, axiom-honest
development.
#print axioms name traces a declaration back to the axioms it
ultimately depends on. Recall (see Lean's three
axioms) that Lean has exactly three: propext, Quot.sound, and
Classical.choice.
theoremmy_classical(p:Prop):¬¬p→p:=funh=>Classical.byContradiction(funhn=>hhn)theoremmy_constructive(n:ℕ):n+0=n:=rfl'my_classical' depends on axioms: [propext,Classical.choice,Quot.sound]#printaxiomsmy_classical
-- 'my_classical' depends on axioms:
-- [propext, Classical.choice, Quot.sound]
'my_constructive' does not depend on any axioms#printaxiomsmy_constructive
-- 'my_constructive' does not depend on any axioms
The main use is a constructivity check: if Classical.choice does
not appear, the proof is constructive. Two caveats are worth
stating:
It is a constructivity detector, not an excluded-middle
detector. Because the law of excluded middle is a
theorem derived from Classical.choice (and not
an axiom in its own right), using it leaves no separate token: a
proof
that uses Classical.em and one that uses Classical.choice
directly are indistinguishable -- both simply show
Classical.choice.
If a proof contains a sorry (even indirectly, through a lemma it
calls), the marker sorryAx appears. This makes #print axioms a
reliable way to detect unfinished proofs hiding in a development.
There is no #used_axioms command; #print axioms is the tool.
#find_home name (from the ImportGraph library) suggests the files
highest in the import hierarchy where a declaration could live,
based on which files its own dependencies come from. It is the tool
for upstreaming a lemma to the right place -- e.g. when contributing
to Mathlib. #find_home! additionally refuses to suggest the
current file.
-- best used in a file with `import Mathlib`
#find_home my_lemma
-- ⇒ a list of candidate modules where `my_lemma` could go, e.g.
-- [Mathlib.Order.Basic, Mathlib.Data.Nat.Defs]
#find_home! my_lemma -- same, but never suggests THIS file
Two points to keep in mind: it works best with import Mathlib, and
it may legitimately return only the current file (if the lemma's
dependencies are spread across incomparable files). A related
command, #min_imports, computes the minimal set of imports a
declaration needs and additionally accounts for notation and tactics.
#lint runs Mathlib's environment linters over declarations,
flagging quality problems such as undocumented definitions
(docBlame), unused arguments (unusedArguments), non-confluent simp
lemmas (simpNF), and uses of deprecated names.
#lint -- lint the current file's declarations
#lint in all -- the whole environment (slow)
#lint only docBlame -- run a single named linter
#lint+ in Batteries -- verbose: report each linter's result
#list_linters -- print every available linter
You can also append * to skip slow tests (#lint*), - for a
silent run that fails on any problem (handy in CI), or extra linter
names to add to the default set.
These are not the same as the build-time linters that produce the
warnings you see when this manual compiles (the *-emphasis and
60-column warnings): those check the Verso markup source, whereas
#lint checks the Lean environment.
This appendix collects Lean's keywords in one place, grouped by role,
with a one-line meaning and a minimal example for each. It is meant
as a lookup table, not a tutorial -- the relevant chapters explain the
constructs in context.
Two things are not keywords and are listed elsewhere:
Commands beginning with # (#check, #eval, #print, ...) are
commands, covered in the Lean basics chapter and the "Getting
help" section.
Symbols such as ∀, ∃, λ, →, ↔, ∧, ∨ are notation,
not keywords.
