kuniga.me > Docs > Lean Cheatsheet

# Lean Cheatsheet

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

## Index

- Setup
- Syntax
- Inductive Type
- Function

- Inference
- Symbols
- Subscripts
- Arrows
- Operators

- Tactics
- apply
- assumption
- cases
- have
- intro
- revert
- rewrite (rw)

- split
- Tactic Combinators
- repeat

- How To?
- Assume the left-hand side of an implication in the goal
- Bind a value to ∀ in the goal
- Bind a value to ∃ in the goal
- Bind a value to ∀ in a hypothesis
- Bind a value to ∃ in a hypothesis
- Split a hypothesis in the form H1 ∧ H2 into two hypothesis
- Introduce new hypothesis within a proof

- References

## Setup

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

## Syntax

### Inductive Type

### 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:

### Subscripts

### Arrows

### Operators

## 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`

:

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