## Background Link to heading

Today my colleague Brandon Rozek released a new Lean4 tutorial on his blog. Brandon really likes for people to be able to read his proofs (for some unknown reason). I decided to write this companion piece where I showcase what Lean4 looks like when you don’t care if people can read it. Towards this end I will be golfing Brandon’s tutorial, that is, going for the shortest proofs I can come up with for each provided theorem. Due to this, almost all of my proofs will be done constructively rather than using tactics, as you can often get much shorter proofs outside of tactic mode.

Reading and understanding these is great practice if you ever want to try understanding mathlib, as the developers frequently write completely unreadable non-tactic based proofs.

All examples can be run live on Lean4 Web here

# Disjunction and Conjunction Link to heading

None of these rules are particularly interesting or deviate substantially from the proofs presented in Rozek’s tutorial.

### Conjunctive Introduction Link to heading

```
example (H_p : p) (H_q : q) : p ∧ q :=
And.intro H_p H_q
```

### Conjunctive Elimination Link to heading

```
example (H_pq : p ∧ q) : p :=
And.left H_pq
```

### Disjunctive Introduction Link to heading

```
example (H_p : p) : p ∨ q :=
Or.intro_left q H_p
```

### Disjunctive Elimination Link to heading

```
example (H_pr : p → r) (H_qr : q → r) (H_pq : p ∨ q) : r :=
Or.elim H_pq H_pr H_qr
```

# Negation Link to heading

A bit more interesting, we can use `Not.elim`

for a particularly elegant proof of negation introduction.
For double negation elimination we just use `Classical.not_not`

.

### Negation Introduction Link to heading

```
example (H_pq : p → q) (H_pnq : p → ¬q) : ¬p :=
λH => Not.elim (H_pnq H) (H_pq H)
```

### Double Negation Elimination Link to heading

```
example {p: Prop} (H_nnp : ¬¬p) : p :=
Classical.not_not.mp H_nnp
```

# First Order Logic Link to heading

Universal introduction is the only slightly elegant one of these. The rest are already quite simple, even in Rozek’s tutorial.

### Universal Elimination Link to heading

```
example (P : α → Prop) (H : ∀ x, P x) : P y :=
H y
```

### Universal Introduction Link to heading

```
example (P Q R : α → Prop) (H_pq : ∀ x : α, P x → Q x)
(H_qr : ∀ x : α, Q x → R x) : ∀ x : α, P x → R x :=
λx Px => H_qr x (H_pq x Px)
```

### Existential Introduction Link to heading

```
example (P : α → Prop) (H: P y) : ∃ x: α, P x :=
Exists.intro y H
```

### Existential Elimination Link to heading

```
example {p : α → Prop} (H_epx : ∃ x, p x)
(H_pab : ∀ (a : α), p a → b) : b :=
Exists.elim H_epx H_pab
```

# Induction Link to heading

I use the real list class instead of Rozek’s custom list class.

### Append Nil Link to heading

The goal is to prove the `List.append_nil`

theorem that an empty list appended to any list returns the original list.
This is a clear usecase for structural induction. In tactic mode we would use the `induction`

tactic, but we can get a much shorter proof using `List.recOn`

.

```
example (as : List α) : as ++ [] = as :=
List.recOn as rfl (λh t ih => by simp [ih])
```

### Length Append Link to heading

The goal is to prove the `List.length_append`

theorem, which states that the length of a list formed from appending two lists is the sum of the originals lengths. While Rozek’s tutorial gives this as an example of something you can use double induction to solve, you actually only need single induction to solve it. My proof is just a
`List.recOn`

version of the proof given for `List.length_append`

in the source that uses `linarith`

to save characters over `Nat.succ_add`

.

```
example (as bs : List α) : (as ++ bs).length = as.length + bs.length :=
List.recOn as (by simp) (λh t ih => by simp [ih]; linarith)
```