Index of Lean tactics
Tactics marked * are specific to this book, so you will not be able to get help with them by googling/consulting internet forums/etc. Reread the indicated part of the book or ask your instructor!
* addarith
(first use: Section 1.5)
Attempts to solve an equality or inequality by moving terms from the left-hand side to the right-hand side, or vice versa.
apply
(first use: Section 2.2; for
Invokes a specified lemma or hypothesis to modify the goal.
by_cases
(first use: Section 5.2)
Case-splits on whether a given statement is true or false.
* cancel
(first use: Section 2.1)
Cancels a common factor from LHS/RHS of equality/inequality, cancels an exponentiation common to both sides, etc.
constructor
(first use: Section 2.4; for ↔
goals: Section 4.2)
Splits an “and” goal (
contradiction
(first use: Section 4.4)
If there are two contradictory hypotheses available, this concludes the proof.
dsimp
(first use: Section 3.1)
Unfolds a definition. Typically used while working on a proof rather than in the final version; it
is useful for inspecting a goal or hypothesis more carefully, but in most cases the proof will still
work after a dsimp
line is deleted.
* extra
(first use: Section 1.4; for congruences: Section 3.4)
A comparison tactic for inequalities, or other relations such as congruences: checks an inequality whose two sides differ by the addition of a positive quantity, a congruence mod 3 whose two sides differ by a multiple of 3, etc.
interval_cases
(first use: Section 4.1)
Given a natural-number or integer variable
intro
(first use: Section 4.1; for
Introduces a universally quantified variable (
left
(first use: Section 2.3)
Selects the left alternative of an “or” goal (
have
(first use: Section 2.1; with a lemma: Section 2.3; introducing a new goal: Section 2.4)
Records a fact (followed by the proof of that fact), which then becomes available as an extra hypothesis.
mod_cases
(first use: Section 3.4)
Introduces cases for a variable according to its residue modulo a specified number.
* numbers
(first use: Section 1.4; with at
for contradictions: Section 4.4)
Proves numeric facts, like
obtain
(first use for
Takes apart a hypothesis of the form “or” (
push_neg
(first use: Section 5.3)
Converts a hypothesis or goal to a logically equivalent form with negations pushed inwards as far as possible.
rel
(first use: Section 1.4; for congruences: Section 3.4; for logical equivalences: Section 5.3)
A “substitution-like” tactic for inequalities, or other relations such as congruences: looks for
the left-hand side of a specified inequality (or congruence, …) fact in the goal, and replaces it
with the right-hand side of that fact, if that replacement is “obviously” a valid inequality
(or modular arithmetic, …) deduction. Compare with rw
.
right
(first use: Section 2.3)
Selects the right alternative of an “or” goal (
ring
(first use: Section 1.2)
Solves algebraic equality goals such as
rw
(first use: Section 1.2; for ↔
hypotheses/lemmas: Section 4.2)
Substitution: looks for the left-hand side of a specified equality fact in the goal, and replaces it with the right-hand side of that fact.
With ↔
hypotheses/lemmas, replaces the left-hand side of the specified ↔
fact with
the right-hand side of that fact.
use
(first use: Section 2.5)
Provides a witness to an existential goal (