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 $\mathrm{\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 ($\wedge$) 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 $\mathrm{\neg }$ goals: Section 4.5)

Introduces a universally quantified variable ($\mathrm{\forall }$) or the antecedent of an implication ($\to$) from the goal, or assumes (for the sake of contradiction) the positive version of a negation ($\mathrm{\neg }$) goal.

left (first use: Section 2.3)

Selects the left alternative of an “or” goal ($\vee$).

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 $\vee$: Section 2.3; for $\wedge$: Section 2.4; for $\mathrm{\exists }$: Section 2.5)

Takes apart a hypothesis of the form “or” ($\vee$), “and” ($\wedge$) or “there exists” ($\mathrm{\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 ($\vee$).

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 ($\mathrm{\exists }$).