## Lean Cheat Sheets

### Tactics for Connectives & Quantifiers

PropositionsTo introduceTo eliminate
`P β Q``intro`function application
`P β§ Q``split``cases`
`P β¨ Q``left`, `right``cases`
`β a : X, H``existsi``cases`
`β a : X, H``intro`function application
`P β Q``split``cases`
`Β¬P``intro`function application

### Other Tactics for Logic

#### `exact hp` (prove a goal `β’ P` if you have `hp : P` by copying `hp`)

How does `exact` work?

If the goal is `β’ X` then `exact hp` will close the goal if and only if `hp : X`

``````theorem not_not_intro (P : Prop) :
P β Β¬Β¬ P :=
begin
intro hp,
apply not.intro,
intro hnp,
apply hnp,
exact hp,
end
``````

#### `intro h` (turns `β’ P β Q` into `h : P, β’ Q`)

How does `intro` work?

`intro hp` will turn a goal `β’ P β Q` into a hypothesis `hp : P` and goal `β’ Q`. If `P` and `Q` are sets `intro p` means βlet `p` be an arbitrary element of `P`β. If `P` and `Q` are propositions then `intro hp` says βassume `P` is trueβ (i.e. βlet `hp` be a proof of `P`). We also use `intro` to prove a universally quantified statement.

``````theorem forall_impl
(A B : U β Prop) : (β x, A x β B x) β (β x, A x) β (β x, B x) :=
begin
intro h,
intro u,
intro a,
have e, from u a,
have h_a, from h a,
show B a, from h_a e,
-- exact h_a e,
end
``````

#### `apply h` (turns `h : P β Q, β’ Q` into `β’ P`)

How does `apply` work?

If you have `h : P β Q` and your goal is `β’ Q` then `apply h` changes the goal to `β’ P`. If you are trying to create a proof of `Q`, and `h` is a rule which turns proofs of `P` into proofs of `Q`, then it will suffice to construct a proof of `P`. It is the bottom-to-top version of application. Hereβs an example:

``````theorem curry (P Q R : Prop) : (P β§ Q β R) β (P β (Q β R) :=
begin
intro h,
intro hp,
intro hq,
apply h,
constructor,
exact hp,
exact hq,
end
``````

Puzzle: figure out what `constructor` does by examining what `Lean` tells you about your goals.

### Proving Equalities With Tactics

#### `refl` (prove `t = t` goals)

How does `refl` work?

`refl` proves goals of the form `t = t`, and more generally goals of the form `t ~ t` where `~` is any reflexive binary relation.

``````example (a b c d : β) : (a + b) * (c + d) = (a + b) * (c + d) :=
begin
refl,
end
``````

#### `rw h` (use a proof `h : x = y` to change `x`s to `y`s)

How does `rw` work?

The `rw` tactic corresponds to the substitution rule of equality which we discussed in the lecture on the equality predicate. If `h` is a proof of `A = B` (i.e. `h : x = y`), then `rw h` will change all `x`s in the goal to `y`s. Variants: `rw βh` (get the backward arrow with `\l`) changes `y` to `x` and `rw h at u` (changes `x` to `y` in hypothesis `u` instead of the goal). Here is an example:

``````example (m n : β) (h : n = m + 6) : 2 * n = 2 * (m + 6) :=
begin
rw h,
end
``````

Here is another example:

``````example (P Q : Prop) (h : P β Β¬ Q) : (P β Β¬ Β¬ P) β (Β¬ Q β Β¬ Β¬ Β¬  Q) :=
begin
rw β h,
intro u,
exact u,
end
``````

Note that here Lean uses propositional extensionality to equate two equivalent proposition.

``````#check propext
``````

#### `simp` (use relevant lemmas and hypotheses to simplify the goal)

How does `simp` work?

This tactic has several variants and it is used quite frequently. In its most basic form, simp will try to use relevant lemmas and hypotheses to simplify the goal. `dsimp` is similar to simp, except that it only uses definitional equalities. See here for a full guide for all usages of `simp`.

``````example : β n : β,  2 β  2 * 2 * n := begin
intro n,
cases n with d hd,
simp,
``````example (n : β) (h : n + 1 - 1 β  0) : n + 1 β  1 :=