Lean Cheatsheet

kuniga.me > Docs > Lean Cheatsheet

# Lean Cheatsheet

NOTE: This refers to the community fork of Lean (test with v3.42).

## Index

1. Setup
2. Syntax
3. Inference
4. Symbols
5. Tactics
6. split
7. Tactic Combinators
8. How To?
9. References

## Setup

If you already have an existing folder, run this inside the folder.

## Syntax

### Function

Alternative: pattern matching.

Function Composition.

## Inference

Typing an underscore in an expression asks Lean to infer a suitable value for the expression and fill it in automatically.

## Symbols

For copy and pasting:

## Tactics

### apply

Given goal b and hypothesis h: a -> b, apply h turns goal b into a.

### assumption

The assumption tactic looks through the assumptions in context of the current goal, and if there is one matching the conclusion, it applies it.

### cases

Split a hyposesis of the form a ^ b into two hypothesis a and b.

### have

have q := f p, https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=7

### intro

If the current goal is a → b, intro h assumes a is true (adding as hypothesis h) and the goal becomes b.

### revert

If there’s a hypothesis h: a → b and the current goal is b, revert h, turns the goal into a → b.

### rewrite (rw)

• You give an axiom/lemma that states an equality of the form expr1 = expr2.
• It will try to find the first expression that matches expr1
• It will replace that expression everywhere in the current state.

Syntax:

Example:

reversed rewrite.

Replace expr2 with expr1 instead:

Syntax:

rewrite only the n-th match.

Syntax:

## split

If the current goal is a ∧ b, split generates 2 goals a and b. (Same as apply and.intro)

## Tactic Combinators

### repeat

Executes a tactic while it’s applicable. Example:

## How To?

### Assume the left-hand side of an implication in the goal

If the goal is of the form ⊢ x → y we add x to our hypothesis and prove y:

### Bind a value to ∀ in the goal

If the goal is of the form ⊢ ∀ x, f(x) we can bind x to some specific variable y and prove the goal for it:

### Bind a value to ∃ in the goal

If the goal is of the form ⊢ ∃ x, f(x) we can replace with a specific instance via existsi:

### Bind a value to ∀ in a hypothesis

If we have a hypothesis H: ∀ x, f(x), we can create a new hypothesis binding x with some instance via have Hy := H y:

### Bind a value to ∃ in a hypothesis

If we have a hypothesis H: ∃ x, f(x), we can introduce some y and create a new hypothesis that is H applied to y:

### Split a hypothesis in the form H1 ∧ H2 into two hypothesis

If we have a hypothesis H: H1 ∧ H2, we can get two hypothesis H1 and H2:

### Introduce new hypothesis within a proof

We can choose to prove an intermediate result within a proof for better readability/organization.

This adds a new hypothesis H and a new goal to prove that hypothesis. If this proof is long, it might be worth to define an actual lemma.

## References

• https://leanprover.github.io/theorem_proving_in_lean/tactics.html
• https://leanprover.github.io/reference/tactics.html
• https://leanprover-community.github.io//img/lean-tactics.pdf