3.1. Tactics Cheatsheet🔗

3.2. apply🔗

Summary: If we have the goal ⊢ Q, and a proof of h : P → Q, we only need to find a proof for P. This transition happens by apply h.

The apply-tactics works iteratively. This means that if apply h makes no progress, it uses the placeholder _ and tries to make apply h _.

Remarks:

• apply works up to equality by definition. This can be seen in the example above, where ¬P ↔ (P → False) is true by definition.

• apply h is frequently identical to refine ?_.

• If the use of apply closes the current goal, you might as well use exact instead of apply.

Lean.Parser.Tactic.apply : Lean.ParserDescr

3.3. apply?🔗

Summary: There are already a lot of proven statements in Mathlib. When using apply?, Mathlib is searched for statements whose types correspond to those of the statement to be proved. If this is not successful, Lean reports a timeout. If successful, it also reports which commands were found. If you click on it, this is inserted in place of apply?.

Examples

Try this: exact Nat.two_mul n

Lean.Parser.Tactic.apply? : Lean.ParserDescr

3.4. assumption🔗

Summary: If a hypothesis is identical to the goal, assumption closes the goal.

Examples

Remarks

• As in other tactics, assumption works up to definitional equality.

• Here is a trick: If you use <;> after a tactic, the forthcoming tactic is applied to apll goals.

Lean.Parser.Tactic.assumption : Lean.ParserDescr

3.5. by_cases🔗

Summary: If you have a term P : Prop as a hypothesis, by_cases hP : P returns two goals. The first one has hP : P, and the second one hP : ¬P. This tactic is thus identical to have hP : P ∨ ¬ P, exact em P, cases hP,. (The second expression is em : ∀ (p : Prop), p ∨ ¬p.)

Examples

In the second example, we use a variable of type bool This is defined as follows:

Bool : Type

false : Bool

true : Bool

«tacticBy_cases_:_» : Lean.ParserDescr

Notes

• Apparently, the by_cases tactic (just like by_contra) assumes that a statement is either true or false. This is also known as the law of excluded middle. In mathematics, proofs that do not use this rule are called constructive.

• For terms of type Prop, the tactic tauto (or tauto!) can draw various conclusions from a truth table.

3.6. by_contra🔗

Summary

The by_contra tactic provides a proof by contradiction. It is therefore assumed (i.e. transformed into a hypothesis) that the statement (after ⊢) is not true, and this must be made to contradict itself, i.e. a proof of false must be found.

Examples

Remarks

This tactic is stronger than exfalso. After all, there the goal is only converted to false without adding a new hypothesis. With by_contra, the new goal is also false, but there is still a new hypothesis.

3.7. calc🔗

Summary: As the word suggests, calc is about concrete calculations. This is not a tactic, but a lean mode. This means that you can enter this mode (with the word calc) and enter calculation steps and proofs that each individual calculation step is correct.

Examples

Here is a proof of the first binomial formula that only comes about by rewriting of calculating properties from the mathlib.

The same can be achieved without the calc mode, like this:

example (n : ℕ): (n+1)^2 = n^2 + 2*n + 1 := by
  have h : n + n = 2*n, by { nth_rewrite 0 ← one_mul n,
  nth_rewrite 1 ← one_mul n, rw ← add_mul, },
  rw [pow_two, mul_add, add_mul, mul_one (n+1), one_mul,
  ← pow_two, add_assoc, ← add_assoc n n 1,
  ← add_assoc, ← h],

However, this is much less readable.

Remarks

• The exact notation is important in calc mode.

• The calc mode not only works for equalities, but also for inequalities, subset-relations etc.

• The example above can be solved easily using linarith or ring.

• In order to generate a proof in calc mode, one can do it as follows (see the example below):

  • give the exact calculation steps without proof (using by sorry)

  • fill in the proofs which are left over.

Lean.calc : Lean.ParserDescr

calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz

calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz

calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz

3.8. cases'🔗

Summary: If a hypothesis is composed, i.e. can be expanded into two or more cases, cases' delivers exactly that. This can be used not only used with hypotheses h : P ∨ Q or h : P ∧ Q, but also with structures that consist of several cases, such as ∃... (here there is a variable and a statement) and x : bool or n : ℕ.

Examples:

Remarks:

• The application cases' n for n : ℕ is strictly weaker than complete induction (see induction). After all, cases only converts n : ℕ into the two cases 0 and succ n, but you cannot use the statement for n-1 to prove the statement for n.

• A more flexible version of cases' is rcases.

3.9. change🔗

Summary: Changes the goal (or a hypothesis) into a goal (or a hypothesis) that is defined the same.

Examples:

Remarks:

• As can be seen from the penultimate example, change also works for hypotheses.

• Since many tactics test for definitional equality anyway, change is often not necessary. However, it can help to make the proof more readable.

3.10. clear🔗

Summary: With clear h the hypothesis h is removed from the goal state (forgotten).

Example

3.11. congr🔗

Summary: If you have to show an equality f x = f y, then congr uses the statement that the equality is particularly true if x = y.

Examples:

Remarks:

• The related tactic congr' uses another parameter that determines how many recursive layers are eliminated in the goal; see the examples below.

• Besides the congr tactic there are several related results which can be applied, e.g. tsum_congr.

theorem tsum_congr.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f g : β → α}, (∀ (b : β), f b = g b) → ∑' (b : β), f b = ∑' (b : β), g b :=
fun {α} {β} [AddCommMonoid α] [TopologicalSpace α] {f g} hfg => congr_arg tsum (funext hfg)

3.12. constructor🔗

Summary: If the goal is of the type ⊢ P ∧ Q, it is replaced by constructor into two goals ⊢ P and ⊢ Q.

Examples

Remarks

Note that ⊢ P ↔ Q is identical to ⊢ (P → Q) ∧ (Q → P).

3.13. exact🔗

Summary: If the goal can be closed with a single command, then it can be closed with the exact tactic. Like many other tactics, exact also works with terms that are definitionally equal.

Examples:

Remarks:

• The related tyctics exact? searches for terms which close the goal; see apply?.

• If the proof consists of a single call of exact, it is easy to translate it to term mode; see easy proofs in term mode.

• In the third example, note the order in which the two hypotheses hP and hnP are applied. The first hypothesis after exact is always the one whose right side matches the goal. If the goal requires further input, it is appended afterwards.

3.14. exfalso🔗

Summary: The statement false → P is true for all P. If the current goal is ⊢ P, and you would apply this true statement using apply, the new goal would be ⊢ false. This is exactly what the exfalso tactic does.

Examples:

Remarks:

• If you use this tactic, you leave the realm of constructive mathematics. (This dispenses with the rule of the excluded middle.)

• exfalso is the same as apply False.elim; see the examples for exact.

3.15. have🔗

Summary: By using have we introduce a new goal, which we have to prove first. Afterwards, it is available as a hypothesis in all further goals. This is identical to first proving a lemma h with the statement after have h : and then reusing it at the appropriate place in the proof (for example with apply or rw).

Examples:

Remarks:

• Assume you want to use have. You could as well formulate a separate lemma and use it afterwards. It is not always clear which is better.

• If the proof of the statement is short and is only used once in your proof, you might want to consider replacing its proof in the place where it is needed.

• Suppose we have two goals (let's call them ⊢ 1 and ⊢ 2), and we need the statement of ⊢ 1 in the proof of ⊢ 2. We can first introduce a third goal with have h := ⊢ 1 (where ⊢ 1 is to be replaced by the statement). Then ⊢ 1 can be proved with exact, and has the statement ⊢ 1 available in the proof of ⊢ 2.

example (P : Prop) : False → P := by
  exact False.elim

3.16. induction🔗

Summary:

Inductive types allow the possibility of proving statements about them by means of induction. This includes, for example, the usual case of complete induction over natural numbers.

Examples

3.17. intro🔗

Summary

If the goal is of the form ⊢ P → Q or ∀ (n : ℕ), P n, you can proceed with intro P or intro n. You can use several intro commands at the same time to summarize a single one. A little more precisely, intro h1 h2 h3, is identical to intro h1; intro h2; intro h3.

Examples

Remarks

• Several intro commands in a row are best combined. Furthermore, rintro is a more flexible variant.

• A reversal of intro is revert.

3.18. left🔗

Summary:

The application of left, is identical to apply h for h : P → P ∨ Q. So if you have a goal of the form ⊢ P ∨ Q, left, causes you to have only the goal ⊢ P. After all, it is sufficient to show P to close the goal.

Examples:

The second example requires a little explanation. First of all, you have to understand that the goal ⊢ ℕ is to show that there is a term of type ℕ, i.e. that there is a natural number. Now you have to know how ℕ is implemented in Lean. This is

together with

notation `ℕ` := nat

This means: The type ℕ is defined by the fact that zero is a term of this type, and that there is a function succ : ℕ → ℕ. Thus, in the second example, the input left, is closed because by definition zero : ℕ holds, so in particular there is a term of type ℕ.

Remarks:

• See also right, for the equivalent tactic, which is apply h for h : Q → P ∨ Q.

• As in the second example, left, can always be applied when dealing with an inductive type with two constructors (such like ℕ).

3.19. linarith🔗

Summary: This tactic can prove equations and inequalities with the help of hypotheses. It is important that the hypotheses used are also only equations and inequalities. So here we are working mainly with the transitivity of < together with arithmetic rules.

Examples:

3.20. norm_num🔗

Summary:

As long as there are no variables, norm_num can do calculations which involve =, <, ≤ or ≠.

Examples:

Remarks

norm_num knows about some more operations, e.g. absolute values; see also the second example.

3.21. nth_rewrite🔗

Summary:

This tactic is related to rw. The difference is that you can specify the occurrence number of the term to be replaced on which rw is to be applied. The exact syntax is nth_rewrite k h, where k is the number (starting with $0$) of the term to be replaced and h is the hypothesis to be replaced. As with rw, this must be in the form h : x=y or h : A↔B.

Examples:

In the above example, Lean sees three terms of the form 0 + ?_: Number 0 is on the left-hand side, for numbers 1 and 2, on the right side (because of the parenthesis 0 + 0 + n = (0 + 0) + n), the second = is checked first. To the left of it is 0 + 0, which is by definition identical to 0. applying rw zero_add here, the term is converted to n. For number 2, you see 0 + 0, determine that it is of the desired form and convert it to 0.

3.22. obtain🔗

Summary: The obtain tactic can be used to merge have and cases into one command.

Examples:

3.23. push_neg🔗

Summary: In many steps of a proof, a negation must be carried out. In order to process the corresponding quantifiers etc. as well and to better reusable, the tactic push_neg is available.

Examples

Notes:

This tactic also works with other objects, such as sets.

3.24. rcases🔗

Summary: rcases is a more flexible version of cases. Here, it is allowed to use ⟨ hP, hQ ⟩ (or (hP | hQ)) to to split the hypotheses hP and hQ into their cases. As can be seen in the example above, it is also possible to nest ⟨.,.⟩ and (.|.).

Examples:

Remarks:

The last example shows how to use rcases to directly resolve a ∃ quantifier in a hypothesis that has more than one constraint (here: 0 ≤ m) and m < n can be resolved directly.

Lean.Elab.Tactic.RCases.RCasesPatt : Type

paren (ref : Lean.Syntax)
    : Lean.Elab.Tactic.RCases.RCasesPatt →
      Lean.Elab.Tactic.RCases.RCasesPatt

one (ref : Lean.Syntax)
    : Lean.Name → Lean.Elab.Tactic.RCases.RCasesPatt

clear (ref : Lean.Syntax)
    : Lean.Elab.Tactic.RCases.RCasesPatt

explicit (ref : Lean.Syntax)
    : Lean.Elab.Tactic.RCases.RCasesPatt →
      Lean.Elab.Tactic.RCases.RCasesPatt

typed (ref : Lean.Syntax)
    : Lean.Elab.Tactic.RCases.RCasesPatt →
      Lean.Term → Lean.Elab.Tactic.RCases.RCasesPatt

tuple (ref : Lean.Syntax)
    : List Lean.Elab.Tactic.RCases.RCasesPatt →
      Lean.Elab.Tactic.RCases.RCasesPatt

alts (ref : Lean.Syntax)
    : List Lean.Elab.Tactic.RCases.RCasesPatt →
      Lean.Elab.Tactic.RCases.RCasesPatt

3.25. refine🔗

Summary: The refine tactic is like exact with holes. More precisely: if the goal is to apply a combination of hypotheses, you can do that with 'refine' and write an open term '' for each. You then get each '' back as a new goal (where those with definitional equality are solved immediately).

Examples:

3.26. revert🔗

Summary: revert is the opposite of intro: It takes a hypothesis from the local context and inserts it as a precondition into the goal.

Examples

Remarks:

revert is rarely needed; actually only when you want to apply an already proven result exactly and first want to establish the correct form of the goal.

3.27. rfl🔗

Summary: This tactic proves the equality (or equivalence) of two definitionally equal terms.

Examples:

Remarks:

The second example works because both sides are by definition equal to succ succ succ 0.

Lean.Elab.Tactic.Rfl.evalApplyRfl
    : Lean.Elab.Tactic.Tactic

3.28. right🔗

Summary: See left, where the adjustments are obvious.

Examples

3.29. ring🔗

Summary: The ring uses rules of calculation such as associativity, commutativity, and distributivity to achieve the goal.

Examples

Remarks:

• The second example works even though ℕ is not a ring (but only a half-ring). It would also work with n : ℝ (since ℝ has more calculation rules than ℕ).

• ring is only used to close the goal.

3.30. rintro🔗

Summary: The rintro tactic is used to process several intro and cases tactics on one line.

Examples

Notes:

Here, more than two ∨ can also be split into cases in one step: With A ∨ B ∨ C, rintro (A | B | C) introduces three goals.

Lean.Elab.Tactic.RCases.rintro
    (pats : Lean.TSyntaxArray `rintroPat)
    (ty? : Option Lean.Term) (g : Lean.MVarId)
    : Lean.Elab.TermElabM (List Lean.MVarId)

3.31. rw🔗

Summary: rw stands for rewrite. For rw h to work, h must be an expression of the type h : x=y or h : A↔B. In this case, rw h replaces every term that is syntactically identical to x (or A) is replaced by y (or B). This also works if h is an already proven result (i.e. a lemma or theorem). With rw ← h is applied from right to left. (In the above example, y is replaced by x and B by A.)

Examples