Tactic Use

Tactic Description

rfl

If the goal is an equality, complete the proof if the two sides are either the same, or can be made the same by evaluation.

intros id1 id2 ...
or
intro id1

adds new hypothesis id1 : P1,id2 : P2, etc to premises, assuming goal is of the form P1 -> P2 -> P or ∀ x : P1, y : P2, P
The new goal will now be P
Note that if id is _, then Lean will generate a name for it.

‹P› (typed as \f< P \f>)

if there is only one hypothesis of type P, this is a way of referencing it anonymously in other tactics

cases id

if id is a hypothesis of some inductive type, perform case analysis on it, either constructing multiple hypotheses (if it is a product type) or multiple goals (if it is a sum type).

exact term

if term is a term of the same type as the goal, then this tactic completes the proof.

assumption

if there is some hypothesis that has the same type as the goal, then this tactic completes the proof by using that hypothesis.

case name id ... =>

if there is a goal called name, focus on it, and bind (optional) identifiers to parameters if available.

constructor

if the goal is an inductive type, try applying its constructors to see if any match.

apply H

H must be a hypothesis or theorem with type P1 -> P2 -> ... -> PN -> Q, where the goal has type Q. This tactic will replace the goal with N separate goals, P1, through PN, as it corresponds to deciding to prove the premises of H and then using it to prove the goal. In the simply case where you just have P -> Q this will replace Q with P

tactic1 <;> tactic2

Apply tactic1 to the current goal, and then apply tactic2 to all goals that are generated by the result of tactic1 (0, 1, or more).

induction id

If id is a hypothesis that is an inductive type, replace the current goal with cases for each of the constructors of the inductive type.

simp only [id, id, ...]

Evaluates the goal, but only using the functions specified in the list

simp only [id, id, ...] at H

The same as above, but simplifies in a hypothesis H

rw [H1, H2, ...]

If HN are equations that are hypotheses or theorems, rewrite the goal with them. Note that after rewriting, the tactic will attempt to close the goal using rfl

rw [<- H1, H2, ...] at H

The arrow allows to rewrite using the equation the other direction, and the at H allows you to specify a hypothesis where you rewrite, rather than the goal

try tac

Run tactic tac, and even if tac fails, still succeed, which is important when wrapping inside of <;>, as the chain will stop at the first failing tactic.

have H : T := by tac

Introduces a new local theorem called H, whose statement is T, proved by the tactic (or series of tacics tac.

contradiction

Looks for an impossible hypothesis (i.e., true = false , 1 = 0, etc. And use it to prove the goal. You can also often do this by doing case analysis on the impossible hypothesis, but this tactic is more convenient.

generalize H : expression = id

Creates new hypothesis H : expression = id , and replaces all occurrences of expression in the goal with id. This is particularly useful to be be able to do case analysis on the result of an expression (e.g., a boolean expression). Note that if you want to replace occurrences of expression in a hypothesis, you need to first revert it to move it back to the goal, and then intros it afterwards.

suffices h : H by ...

Creates new hypothesis h : H which you can use to complete the proof. Once you finish the proof, you now have to prove h : H. This can be useful to 'cut' a proof in the middle: first go from the middle to the end, and then go back and prove up to that middle point.

rename_i h

Gives a name h to the most recent anonymous hypothesis (unnamed or given with italicized, gray, crossed names). This can be useful if you manage to override a name, or you don't want to actually switch into a case before using names that it introduces.

simp [*, h1, h2]

Try to rewrite with any of the built-in simp theorems, any of the local hypotheses (*), or any of the theorems h1 and h2. You can also do this with only to avoid the built-in simp theorems.

exists e

Given a goal of type Exists P, exists e will instantiate the existential with the witness value e and close the goal if P e is trivially provable. If P e is not immediately provable, P e will become the goal.