kuniga.me > Docs > Lean Cheatsheet

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

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

Alternative: pattern matching.

**Function Composition.**

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

For copy and pasting:

Given goal `b`

and hypothesis `h: a -> b`

, `apply h`

turns goal `b`

into `a`

.

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

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

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

If the current goal is `a → b`

, `intro h`

assumes `a`

is true (adding as hypothesis `h`

) and the goal becomes `b`

.

If there’s a hypothesis `h: a → b`

and the current goal is `b`

, `revert h`

, turns the goal into `a → b`

.

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

**rewrite multiple hypothesis**

Syntax:

If the current goal is `a ∧ b`

, `split`

generates 2 goals `a`

and `b`

. (Same as `apply and.intro`

)

Executes a tactic while it’s applicable. Example:

If the goal is of the form `⊢ x → y`

we add `x`

to our hypothesis and prove `y`

:

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:

If the goal is of the form `⊢ ∃ x, f(x)`

we can replace with a specific instance via `existsi`

:

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`

:

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`

:

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.

- 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