# 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\)).