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