# Natural Number Game
## Tutorial World
### Level 1 | rfl
```lean
rfl
```
---
### Level 2 | rw
```lean
rw[h]
rfl
```
---
### Level 3 | Numbers
```lean
rw[two_eq_succ_one]
rw[one_eq_succ_zero]
rfl
```
---
### Level 4 | Rewriting Backwards
```lean
rw[← one_eq_succ_zero]
rw[← two_eq_succ_one]
rfl
```
---
### Level 5 | Adding Zero
```lean
rw[add_zero]
rw[add_zero]
rfl
```
---
### Level 6 | Precision Rewriting
```lean
rw[add_zero c]
rw[add_zero]
rfl
```
---
### Level 7 | add_succ
```lean
rw[one_eq_succ_zero]
rw[add_succ]
rw[add_zero]
rfl
```
---
### Level 8 | 2 + 2 = 4
```lean
nth_rewrite 2 [two_eq_succ_one]
nth_rewrite 1 [two_eq_succ_one]
rw[one_eq_succ_zero]
rw[add_succ]
rw[add_succ]
rw[add_zero]
rw[← one_eq_succ_zero]
rw[← two_eq_succ_one]
rw[← three_eq_succ_two]
rw[← four_eq_succ_three]
rfl
```
---
## Addition World
### Level 1 | zero_add
```lean
induction n with d hd
rw[add_zero]
rfl
rw[add_succ]
rw[hd]
rfl
```
---
### Level 2 | succ_add
```lean
induction b with d hd
rw[add_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[add_succ]
rw[hd]
rfl
```
---
### Level 3 | add_comm (level boss)
```lean
induction b with a hd
rw[add_zero]
rw[zero_add]
rfl
rw[add_succ]
rw[hd]
rw[succ_add]
rfl
```
---
### Level 4 | add_assoc (associativity of addition)
```lean
induction a with d hd
rw[add_comm]
rw[add_comm]
rw[zero_add]
rw[zero_add]
rfl
rw[succ_add]
rw[succ_add]
rw[succ_add]
rw[hd]
rfl
```
---
### Level 5 | add_right_comm
```lean
rw[add_comm a]
rw[add_assoc]
rw[add_comm]
rfl
```
---
## Multiplication World
### Level 1 | mul_one
``` lean
rw[one_eq_succ_zero]
rw[mul_succ]
rw[mul_zero]
rw[zero_add]
rfl
```
---
### Level 2 | zero_mul
```lean
induction m with d hd
rw[mul_zero]
rfl
rw[mul_succ]
rw[hd]
rw[add_zero]
rfl
```
---
### Level 3 | succ_mul
```lean
induction b with d hd
rw[add_zero]
rw[mul_zero]
rw[mul_zero]
rfl
rw[mul_succ]
rw[mul_succ]
rw[hd]
rw[add_succ]
rw[add_succ]
rw[add_right_comm]
rfl
```
---
### Level 4 | mul_comm
```lean
induction b with d hd
rw[mul_zero]
rw[zero_mul]
rfl
rw[succ_mul]
rw[mul_succ]
rw[hd]
rfl
```
---
### Level 5 | one_mul
```lean
rw[one_eq_succ_zero]
rw[succ_mul]
rw[zero_mul]
rw[zero_add]
rfl
```
---
### Level 6 | two_mul
```lean
rw[two_eq_succ_one]
rw[succ_mul]
rw[one_mul]
rfl
```
---
### Level 7 | mul_add
```lean
induction c with d hd
rw[add_zero]
rw[mul_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[mul_succ]
rw[mul_succ]
rw[hd]
rw[add_assoc]
rfl
```
---
### Level 8 | add_mul
```lean
induction b with d hd
rw[add_zero]
rw[zero_mul]
rw[add_zero]
rfl
rw[succ_eq_add_one]
rw[<- add_assoc]
rw[mul_comm]
rw[mul_add]
rw[mul_comm]
rw[mul_one]
rw[hd]
rw[<- succ_eq_add_one]
rw[succ_mul]
rw[add_assoc]
rfl
```
---
### Level 9 | mul_assoc
```lean
induction b with d hd
rw[mul_zero]
rw[zero_mul]
rw[mul_zero]
rfl
rw[succ_mul]
rw[mul_succ]
rw[add_mul]
rw[mul_add]
rw[hd]
rfl
```
---
## Implication World
### Level 1 | The `exact` tactic
```lean
exact h1
```
---
### Level 2 | `exact` practice
```lean
rw[zero_add] at h
rw[zero_add] at h
exact h
```
---
### Level 3 | The `apply` tactic.
```lean
apply h2 at h1
exact h1
```
---
### Level 4 | succ_inj : the successor function is injective
```lean
rw[four_eq_succ_three] at h
rw[<- succ_eq_add_one] at h
apply succ_inj at h
exact h
```
---
### Level 5 | Arguing backwards
```lean
rw[four_eq_succ_three] at h
rw[<- succ_eq_add_one] at h
apply succ_inj at h
exact h
```
---
### Level 6 | intro
```lean
intro h
exact h
```
---
### Level 7 | intro practice
```lean
intro h
rw[<- succ_eq_add_one] at h
rw[<- succ_eq_add_one] at h
apply succ_inj at h
exact h
```
---
### Level 8 | ne
```lean
apply h2 at h1
exact h1
```
---
### Level 9 | zero_ne_succ
```lean
intro h
rw[one_eq_succ_zero] at h
apply zero_ne_succ at h
exact h
```
---
### Level 10 | $1\neq 0$
```lean
intro h
rw[one_eq_succ_zero] at h
symm at h
apply zero_ne_succ at h
exact h
```
---
### Level 11 | $2+2\neq 5$
```lean
intro h
rw[succ_add] at h
rw[succ_add] at h
rw[zero_add] at h
apply succ_inj at h
apply succ_inj at h
apply succ_inj at h
apply succ_inj at h
apply zero_ne_succ at h
exact h
```
---
## Power World
### Level 1 | zero_pow_zero
```lean
rw[pow_zero 0]
rfl
```
---
### Level 2 | zero_pow_succ
```lean
rw[pow_succ]
rw[mul_zero]
rfl
```
---
### Level 3 | pow_one
```lean
rw[one_eq_succ_zero]
rw[pow_succ]
rw[pow_zero]
rw[one_mul]
rfl
```
---
### Level 4 | one_pow
```lean
induction m with d hd
apply pow_zero
rw[pow_succ]
rw[mul_one]
apply hd
```
---
### Level 5 | pow_two
```lean
cases a
rw[two_eq_succ_one]
rw[zero_pow_succ, mul_zero]
rfl
rw[two_eq_succ_one]
rw[pow_succ]
rw[pow_one]
rfl
```
---
### Level 6 | pow_add
```lean
induction n with d hd
rw[add_zero, pow_zero, mul_one]
rfl
rw[add_succ]
rw[pow_succ]
rw[pow_succ]
rw[<- mul_assoc]
rw[hd]
rfl
```
---
### Level 7 | mul_pow
```lean
induction n with d hd
repeat rw[pow_zero]
rw[one_mul]
rfl
repeat rw[pow_succ]
rw[hd]
rw [mul_assoc (a ^ d) (b ^ d) (a * b)]
rw [← mul_assoc (b ^ d) a b]
rw [mul_comm (b ^ d) a]
rw [mul_assoc a (b ^ d) b]
rw [← mul_assoc (a ^ d) a (b ^ d * b)]
rfl
```
---
### Level 8 | pow_pow
```lean
induction n with d hd
rw[pow_zero, mul_zero, pow_zero]
rfl
rw[succ_eq_add_one, pow_add, mul_add]
rw[pow_add]
rw[<- hd]
rw[pow_one, mul_one]
rfl
```
---
### Level 9 | add_sq
```lean
rw[pow_two]
rw[add_mul]
repeat rw[mul_add]
repeat rw[<- pow_two]
rw[mul_comm b a]
simp_add
rw [← add_assoc]
rw [← two_mul]
rw[mul_assoc]
rfl
```
---
### Level 10 | Fermat's Last Theorem
Your move.
---
## Algorithm World
### Level 1 | add_left_comm
```lean
rw[<- add_assoc]
rw[add_comm a b]
rw[add_assoc]
rfl
```
---
### Level 2 | making life easier
```lean
repeat rw[add_assoc]
rw[add_left_comm b c d]
rw[add_comm b d]
rfl
```
---
### Level 3 | making life simple
```lean
simp only [add_left_comm, add_comm]
```
---
### Level 4 | the simplest approach
```lean
simp_add
```
---
### Level 5 | pred
```lean
rw[<- pred_succ a]
rw[<- pred_succ b]
rw[h]
rfl
```
---
### Level 6 | is_zero
```lean
intro h
rw [<- is_zero_succ a]
symm at h
apply zero_ne_succ at h
cases h
```
---
### Level 7 | An algorithm for equality
```lean
contrapose! h
apply succ_inj at h
exact h
```
---
### Level 8 | decide
```lean
decide
```
---
### Level 9 | decide again
```lean
decide
```
---
## Advanced Addition World
### Level 1 | add_right_cancel
```lean
intro h
induction n with d hd
rw[add_zero] at h
rw[add_zero] at h
exact h
repeat rw [add_succ] at h
apply succ_inj at h
apply hd at h
exact h
```
---
### Level 2 | add_left_cancel
```lean
intro h
induction n with h hd
rw[zero_add] at h
rw[zero_add] at h
exact h
repeat rw[succ_add] at h
apply succ_inj at h
apply hd at h
exact h
```
---
### Level 3 | add_left_eq_self
```lean
nth_rewrite 2 [← add_zero y]
rw[add_comm y 0]
apply add_right_cancel
```
---
### Level 4 | add_right_eq_self
```lean
nth_rewrite 2 [<- add_zero x]
apply add_left_cancel
```
---
### Level 5 | add_right_eq_zero
```lean
cases b with d
nth_rewrite 2 [<- add_zero 0]
apply add_right_cancel
intro h
symm at h
rw[add_succ] at h
apply zero_ne_succ at h
cases h
```
---
### Level 6 | add_left_eq_zero
```lean
cases a with d
nth_rewrite 2 [<- zero_add 0]
apply add_left_cancel
rw[succ_add]
intro h
symm
symm at h
apply zero_ne_succ at h
cases h
```
---
## $\leq$ World
### Level 1 | The `use` tactic
```lean
use 0
rw[add_zero]
rfl
```
---
### Level 2 | $0\leq x$
```lean
use x
rw[zero_add]
rfl
```
---
### Level 3 | $x\leq \text{succ} x$
```lean
rw[succ_eq_add_one]
use 1
rfl
```
---
### Level 4 | $x \leq y , y \leq z \implies x \leq z$
```lean
cases hxy with a ha
cases hyz with b hb
rw[ha] at hb
use a+b
rw[hb]
simp_add
```
---
### Level 5 | $x \leq 0 \implies x = 0 $
```lean
cases hx with a ha
symm at ha
apply add_right_eq_zero at ha
rw[ha]
rfl
```
---
### Level 6 | $x \leq y and y \leq x \implies x = y$
```lean
cases hxy with a ha
cases hyx with b hb
rw[ha]
rw[ha] at hb
rw [add_assoc] at hb
symm at hb
apply add_right_eq_self at hb
apply add_right_eq_zero at hb
rw[hb]
rw[add_zero]
rfl
```
---
### Level 7 | Dealing with `or`
```lean
cases h with hx hy
right
apply hx
left
apply hy
```
---
### Level 8 | $x \leq y \vee y \leq x$
```lean
induction y with d hd
right
apply zero_le
cases hd with h1 h2
left
exact le_trans x d (succ d) h1 (le_succ_self d)
cases h2 with c hc
cases c with v
rw[add_zero] at hc
left
rw[hc]
apply le_succ_self
right
use v
rw[hc]
rw[add_succ,succ_add]
rfl
```
---
### Level 9 | $\text{succ} x \leq \text{succ} y \implies x\leq y$
```lean
cases hx with d hd
use d
rw[succ_add] at hd
apply succ_inj at hd
exact hd
```
---
### Level 10 | $x\leq 1$
```lean
cases x with a
left
rfl
right
cases hx with d hd
rw[succ_add] at hd
rw[one_eq_succ_zero] at hd
apply succ_inj at hd
symm at hd
apply add_right_eq_zero at hd
rw[one_eq_succ_zero]
rw[hd]
rfl
```
---
### Level 11 | le_two
```lean
cases x with a
left
rfl
right
cases hx with d hd
rw[two_eq_succ_one, succ_add] at hd
apply succ_inj at hd
cases a with a
cases d with d
rw[one_eq_succ_zero, zero_add] at hd
apply succ_ne_zero at hd
left
cases hd
rw[one_eq_succ_zero, zero_add] at hd
apply succ_inj at hd
left
rw[<- add_zero d] at hd
symm at hd
apply add_right_eq_zero at hd
cases d with d
rw[one_eq_succ_zero]
rfl
apply succ_ne_zero at hd
cases hd
rw[one_eq_succ_zero, succ_add] at hd
apply succ_inj at hd
right
symm at hd
apply add_right_eq_zero at hd
cases hd
rw [two_eq_succ_one, one_eq_succ_zero]
rfl
```
---
## Advanced Multiplication World
### Level 1 | mul_le_mul_right
```lean
induction t with t
repeat rw[mul_zero]
apply le_refl
rw[succ_eq_add_one]
repeat rw[mul_add]
repeat rw[mul_one]
cases h with c hc
cases n_ih with d hd
use d+c
rw[hd,hc]
simp_add
```
---
### Level 2 | mul_left_ne_zero
```lean
intro hb
apply h
rw[hb]
rw[mul_zero]
rfl
```
---
### Level 3 | eq_succ_of_ne_zero
```lean
cases a with d
tauto
use d
rfl
```
---
### Level 4 | one_le_of_ne_zero
```lean
apply eq_succ_of_ne_zero at ha
cases ha with n hn
rw[hn]
rw[succ_eq_add_one]
use n
simp_add
```
---
### Level 5 | le_mul_right
```lean
nth_rewrite 1 [← one_mul a]
apply mul_left_ne_zero at h
apply one_le_of_ne_zero at h
apply mul_le_mul_right 1 b a at h
rw[mul_comm a b]
tauto
```
---
### Level 6 | mul_right_eq_one
```lean
have h2 : x*y ≠ 0
rw[h]
tauto
apply le_mul_right x y at h2
rw[h] at h2
apply le_one at h2
cases h2 with h0 h1
rw[h0] at h
rw[zero_mul] at h
tauto
tauto
```
---
### Level 7 | mul_ne_zero
```lean
contrapose! hb
apply one_le_of_ne_zero at ha
apply mul_le_mul_right 1 a b at ha
rw[hb] at ha
rw[one_mul] at ha
apply le_zero at ha
tauto
```
---
### Level 8 | mul_eq_zero
```lean
contrapose! h
cases h with ha hb
exact mul_ne_zero a b ha hb
```
---
### Level 9 | mul_left_cancel
```lean
induction b with d hd generalizing c
rw[mul_zero] at h
symm at h
apply mul_eq_zero a c at h
tauto
cases c with e
rw[mul_zero] at h
apply mul_eq_zero at h
tauto
repeat rw[mul_succ] at h
rw [succ_eq_add_one, succ_eq_add_one e]
have hde : d = e := hd e (add_right_cancel (a * d) (a * e) a h)
tauto
```
---
### Level 10 | mul_right_eq_self
```lean
nth_rewrite 2 [<- mul_one a] at h
apply mul_left_cancel at h
tauto
tauto
```
---