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