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 \(\forall\) and \(\to\) hypotheses, Section 4.1)
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 (\(\land\)) into sub-goals for its left and right parts.
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 \(n\) for which numeric upper and lower bounds are available, produce cases for each of the numeric possibilities for \(n\).
intro
(first use: Section 4.1; for \(\lnot\) goals: Section 4.5)
Introduces a universally quantified variable (\(\forall\)) or the antecedent of an implication (\(\to\)) from the goal, or assumes (for the sake of contradiction) the positive version of a negation (\(\lnot\)) goal.
left
(first use: Section 2.3)
Selects the left alternative of an “or” goal (\(\lor\)).
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 \(3\cdot 12 < 13 + 25\) or \(3\cdot 5+1=4\cdot 4\).
obtain
(first use for \(\lor\): Section 2.3; for \(\land\): Section 2.4; for \(\exists\): Section 2.5)
Takes apart a hypothesis of the form “or” (\(\lor\)), “and” (\(\land\)) or “there exists” (\(\exists\)).
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 (\(\lor\)).
ring
(first use: Section 1.2)
Solves algebraic equality goals such as \((x + y) ^ 2 = x ^ 2 + 2xy + y ^ 2\), when the proof is effectively “expand out both sides and rearrange”.
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 (\(\exists\)).