diff --git a/Game.lean b/Game.lean
index 75fd90c..ffa2cc3 100644
--- a/Game.lean
+++ b/Game.lean
@@ -1,15 +1,15 @@
 import GameServer.Commands
 
 import Game.Levels.Tutorial
---import Game.Levels.Addition
---import Game.Levels.Multiplication
---import Game.Levels.Power
---import Game.Levels.Function
---import Game.Levels.Proposition
---import Game.Levels.AdvProposition
---import Game.Levels.AdvAddition
---import Game.Levels.AdvMultiplication
-----import Game.Levels.Inequality
+import Game.Levels.Addition
+-- import Game.Levels.Multiplication
+-- import Game.Levels.Power
+-- import Game.Levels.Function
+-- import Game.Levels.Proposition
+-- import Game.Levels.AdvProposition
+-- import Game.Levels.AdvAddition
+-- import Game.Levels.AdvMultiplication
+--import Game.Levels.Inequality
 
 Title "Natural Number Game"
 Introduction
diff --git a/Game/Levels/Addition/Level_5.lean b/Game/Levels/Addition/Level_5.lean
index 08215eb..60fa521 100644
--- a/Game/Levels/Addition/Level_5.lean
+++ b/Game/Levels/Addition/Level_5.lean
@@ -1,4 +1,5 @@
 import Game.Levels.Addition.Level_4
+import Game.MyNat.DecidableEq
 
 
 World "Addition"
@@ -7,9 +8,6 @@ Title "succ_eq_add_one"
 
 open MyNat
 
--- NOTE: this was `one_eq_succ_zero` but we need it earlier.
-axiom MyNat.one_eq_succ_zero' : (1 : ℕ) = succ 0
-
 Introduction
 "
 I've just added `one_eq_succ_zero` (a proof of `1 = succ 0`)
diff --git a/Game/Levels/Addition/Level_6.lean b/Game/Levels/Addition/Level_6.lean
index 95c1990..6ef8c71 100644
--- a/Game/Levels/Addition/Level_6.lean
+++ b/Game/Levels/Addition/Level_6.lean
@@ -76,7 +76,6 @@ $a + b + c = a + c + b$."
   rfl
 
 LemmaTab "Add"
-NewTactic simp -- TODO: Do we want it to be unlocked here?
 
 Conclusion
 "
diff --git a/Game/Levels/Tutorial.lean b/Game/Levels/Tutorial.lean
index ee0a02b..a9d7e2d 100644
--- a/Game/Levels/Tutorial.lean
+++ b/Game/Levels/Tutorial.lean
@@ -1,8 +1,9 @@
 import Game.Levels.Tutorial.L01rfl
 import Game.Levels.Tutorial.L02rw
 import Game.Levels.Tutorial.L03rw_practice
-import Game.Levels.Tutorial.L04one
-
+import Game.Levels.Tutorial.L04onetwothree
+import Game.Levels.Tutorial.L05add_zero
+import Game.Levels.Tutorial.L06add_succ
 
 World "Tutorial"
 Title "Tutorial World"
diff --git a/Game/Levels/Tutorial/L04one.lean b/Game/Levels/Tutorial/L04onetwothree.lean
similarity index 76%
rename from Game/Levels/Tutorial/L04one.lean
rename to Game/Levels/Tutorial/L04onetwothree.lean
index fc8d1e9..b15b95a 100644
--- a/Game/Levels/Tutorial/L04one.lean
+++ b/Game/Levels/Tutorial/L04onetwothree.lean
@@ -13,19 +13,27 @@ NewLemma MyNat.one_eq_succ_zero
 
 Introduction
 "
-The goals of the previous levels in the tutorial mentioned things like addition and multiplication of numbers. But now we start the game itself: building the natural numbers from scratch. Giuseppe Peano defined these numbers via three axioms:
+The goals of the previous levels in the tutorial mentioned things like addition and
+multiplication of numbers. But now we start the game itself: building the natural
+numbers from scratch. Giuseppe Peano defined these numbers via three axioms:
 
 * `0` is a number.
 * If `n` is a number, then the *successor* `succ n` of `n` (that is, the number after `n`) is a number.
 * That's it.
 
-\"That's it\" means \"there is no other way to make numbers\". More on this later: we need to make sure we've cracked the basics before we start talking about infinity. First let's see if we can count to five.
+\"That's it\" means \"there is no other way to make numbers\". More on this later: we need to
+ make sure we've cracked the basics before we start talking about infinity. First let's see if we
+ can count to five.
 
 # Does this make a section?
 
-What kind of numbers can we make from Peano's axioms? Well, Peano gives us the number `0` and the function `succ` taking numbers to numbers. We could apply the function to the number and then get a new number `succ 0`, and we could name this number `1`. The theorem `one_eq_succ_zero` says that `1 = succ 0`.
+What kind of numbers can we make from Peano's axioms? Well, Peano gives us the number `0` and the
+function `succ` taking numbers to numbers. We could apply the function to the number and then get a
+ new number `succ 0`, and we could name this number `1`. The theorem `one_eq_succ_zero` says that
+ `1 = succ 0`.
 
-We could define `2` to either be `succ 1` or `succ (succ 0)`. Are these two choices definitely equal? Let's see if we can prove it.
+We could define `2` to either be `succ 1` or `succ (succ 0)`. Are these two choices definitely
+equal? Let's see if we can prove it.
 "
 Statement
 "$\\operatorname{succ}(1)=\\operatorname{succ}(\\operatorname{succ}(0))$."
diff --git a/Game/Levels/Tutorial/L05add_zero.lean b/Game/Levels/Tutorial/L05add_zero.lean
new file mode 100644
index 0000000..add164e
--- /dev/null
+++ b/Game/Levels/Tutorial/L05add_zero.lean
@@ -0,0 +1,90 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "Tutorial"
+Level 5
+Title "addition"
+
+open MyNat
+
+Introduction
+"
+Peano defined addition $a + b$ by adding two axioms to his system.
+Peano's first axiom was called `add_zero`. Here it is:
+
+* `add_zero : ∀ (a : ℕ), a + 0 = a`
+
+In words, the theorem says that if `a` is an arbitrary natural number, then `a + 0 = a`.
+Another way to think of `add_zero` is as a function, which eats a natural number `a`
+and returns a proof `add_zero a` of `a + 0 = a`.
+
+Let me show you how to use Lean's simplifier `simp`
+to do a lot of work for us."
+
+LemmaDoc MyNat.add_zero as "add_zero" in "Add"
+"One of the two axioms defining addition. It says `n + 0 = n`."
+
+namespace MyNat
+
+TacticDoc simp "The simplifier. `rw` on steroids.
+
+A bunch of lemmas like `add_zero : ∀ a, a + 0 = a`
+are tagged with the `@[simp]` tag. If the `simp` tactic
+is run by the user, the simplifier will try and rewrite
+as many of the lemmas tagged `@[simp]` as it can.
+
+`simp` is a *finishing tactic*. After you run `simp`,
+the goal should be closed. If it is not, it is best
+practice to write `simp?` instead and then replace the
+output with the appropriate `simp only` call. Inappropriate
+use of `simp` can make for very slow code.
+"
+NewTactic simp -- TODO: Do we want it to be unlocked here?
+
+Statement
+"$(a+(0+0)+(0+0+0)=a.$"
+  (a : ℕ)  : (a + (0 + 0)) + (0 + 0 + 0) = a := by
+  Hint "I want this to say \"Walkthrough\".
+
+  This is an annoying goal. One of rw [add_zero a]` amd `rw [add_zero 0]`
+  will work, but not the other. Can you figure out which? Try the one
+  that works."
+  Branch
+    rw [add_zero 0]
+    Hint "Walkthrough: Now `rw [add_zero a]` will work, so try that next."
+    rw [add_zero a]
+    Hint "OK this is getting old really quickly. And if we have to type
+    weird stuff like `rw [add_zero (a + 0)]` it will be even worse.
+    Fortunately `rw` can do smart rewriting. Go back to the very start
+    of this proof with \"undo\" and try `repeat rw [add_zero]`
+    "
+  Branch
+    repeat rw [add_zero]
+    Hint "`rw` can rewrite proofs of the form `? + 0 = ?`
+    where `?` is arbitrary, and it will just use the
+    first solution which matches for `?`.
+
+    The rest of he proof is easy, but don't finish yet, there's more.
+
+    Lean's simplifier is a tool which does repeated
+    rewriting. And `add_zero` is a `simp` lemma. So go back to the
+    start again and just try `simp`."
+  simp
+
+NewLemma MyNat.add_zero
+
+DefinitionDoc Add as "Add" "`Add a b`, with notation `a + b`, is
+the usual sum of natural numbers. Internally it is defined by
+induction on one of the variables, but that is an implementation issue;
+All you need to know is that `add_zero` and `zero_add` are both theorems."
+
+NewDefinition Add
+
+Conclusion
+"
+  The simplifier atempts to solve goals by using *repeated rewriting* of
+  *equalities* and *iff statements*, and then trying `rfl` at the end.
+
+  Let's now learn about Peano's second axiom for addition, `add_succ`.
+"
diff --git a/Game/Levels/Tutorial/L06add_succ.lean b/Game/Levels/Tutorial/L06add_succ.lean
new file mode 100644
index 0000000..a58761b
--- /dev/null
+++ b/Game/Levels/Tutorial/L06add_succ.lean
@@ -0,0 +1,47 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "Tutorial"
+Level 6
+Title "add_succ"
+
+open MyNat
+
+Introduction
+"
+Peano's second axiom was this:
+
+* `add_succ : ∀ (a b : ℕ), a + succ b = succ (a + b)`
+
+It tells you that you can move a `succ` left over an `+`. See if you can rewrite
+your way to a proof of this.
+"
+namespace MyNat
+
+LemmaDoc MyNat.add_succ as "add_succ" in "Add"
+"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
+
+Statement
+"For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = \\operatorname{succ}(a)$."
+    : a + succ 0 = succ a := by
+  Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
+  to make progress."
+  Hint (hidden := true) "Explicitely, type `rw [add_succ]`!"
+  rw [add_succ]
+  Hint "Now you see a term of the form `… + 0`, so you can use `add_zero`."
+  Hint (hidden := true) "Explicitely, type `rw [add_zero]`!"
+  rw [add_zero]
+  Hint (hidden := true) "Finally both sides are identical."
+  rfl
+
+Conclusion
+"
+You have finished tutorial world! If you're happy, let's move onto Addition World,
+and learn about proof by induction.
+
+## Inspection time
+
+If you want to examine your proofs, toggle \"Editor mode\" and click somewhere
+inside the proof to see the state of Lean's brain at that point.
+"
diff --git a/Game/Levels/Tutorial/Level_4.lean b/Game/Levels/Tutorial/Level_4.lean
deleted file mode 100644
index 2ccb143..0000000
--- a/Game/Levels/Tutorial/Level_4.lean
+++ /dev/null
@@ -1,100 +0,0 @@
-import Game.Metadata
-import Game.MyNat.Addition
-
-
-World "Tutorial"
-Level 4
-Title "addition"
-
-open MyNat
-
-Introduction
-"
-Peano defined addition $a + b$ by adding two axioms to his system.
-Peano's first axiom was called `add_zero`. Here it is:
-
-* `add_zero : ∀ (a : ℕ), a + 0 = a`
-
-An axiom is just a theorem with a secret proof. The *statement* of the theorem
-is `∀ (a : ℕ), a + 0 = a`, and the *proof* is `add_zero`. You can't unfold
-`add_zero` any more: it's an axiom. In Lean, every provable theorem has
-*exactly one proof*, and it's an \"atom\", just like if $G$ is a group
-then the elements of $G$ are atoms. The set theory provers (Mizar, Metamath etc)
-tell us that those atoms, if you look closely enough, are themselves sets.
-Let me coin a phrase for the simple type theorists such as Isabelle/HOL
-and he dependent type theorists such as Coq and Lean: let me call them the \"lower type theorists\".
-Whether or are dependent or simple depends on how seriously you care about category theory; it
-is not a coincidence that Hales' proof of Kepler had no category theory in it at all.
-
-The *lower type theorist*  a term which I coin to mean the both the simple type theorists
-such as Isabelle/HOL and the dependent type theorists such as Coq and Lean
-that is, the simple type theorist ()
-simply doesn't care.
-
-
-induction on $b$, or, more precisely, by *recursion* on $b$.
-In other words, he introduced two axiomsHe first explained how to add $0$ to a number: this is the base case.
-
-
-We will call this theorem `add_zero`.
-More precisely, `add_zero` is the name of the *proof* of the
-theorem. Note the name of this proof. Mathematicians sometimes call it
-\"Lemma 2.1\" or \"Hypothesis P6\" or something.
-But computer scientists call it `add_zero` because it tells you what the answer to
-\"x add zero\" is. It's a much better name than \"Lemma 2.1\".
-Even better, you can use the `rw` tactic
-with `add_zero`. If you ever see `x + 0` in your goal,
-`rw [add_zero]` should simplify it to `x`. This is
-because `add_zero` is a proof that `x + 0 = x`
-(more precisely, `add_zero x` is a proof that `x + 0 = x` but
-Lean can figure out the `x` from the context).
-
-Now here's the inductive step. If you know how to add $d$ to $a$, then Peano
-tells you how to add $\\operatorname{succ} (d)$ to $a$. It looks like this:
-
-- `add_succ (a d : ℕ) : a + (succ d) = succ (a + d)`
-
-What's going on here is that we assume `a + d` is already defined, and we define
-`a + (succ d)` to be the number after it.
-Note the name of this proof too: `add_succ` tells you how to add a successor
-to something.
-If you ever see `… + succ …` in your goal, you should be able to use
-`rw [add_succ]` to make progress.
-"
-
-LemmaDoc MyNat.add_succ as "add_succ" in "Add"
-"One of the two axioms defining addition. It says `n + (succ m) = succ (n + m)`."
-
-LemmaDoc MyNat.add_zero as "add_zero" in "Add"
-"One of the two axioms defining addition. It says `n + 0 = n`."
-
-Statement
-"For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = \\operatorname{succ}(a)$."
-    : a + succ 0 = succ a := by
-  Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
-  to make progress."
-  Hint (hidden := true) "Explicitely, type `rw [add_succ]`!"
-  rw [add_succ]
-  Hint "Now you see a term of the form `… + 0`, so you can use `add_zero`."
-  Hint (hidden := true) "Explicitely, type `rw [add_zero]`!"
-  Branch
-    simp? -- TODO
-  rw [MyNat.add_zero]
-  Hint (hidden := true) "Finally both sides are identical."
-  rfl
-
-NewLemma MyNat.add_succ MyNat.add_zero
-NewDefinition Add
-
-#check add_zero
-
-Conclusion
-"
-You have finished tutorial world! If you're happy, let's move onto Addition World,
-and learn about proof by induction.
-
-## Inspection time
-
-If you want to examine the proof, toggle \"Editor mode\" and click somewhere
-inside the proof to see the state at that point!
-"
diff --git a/Game/Levels/Tutorial/Level_5.lean b/Game/Levels/Tutorial/Level_5.lean
deleted file mode 100644
index 99d5a62..0000000
--- a/Game/Levels/Tutorial/Level_5.lean
+++ /dev/null
@@ -1,57 +0,0 @@
-import Game.Metadata
-import Game.MyNat.Addition
-
-
-World "Tutorial"
-Level 5
-Title "add_zero"
-
-open MyNat
-
-Introduction
-"
-  `add_zero` is a *proof*, and it is also a *function* at the same time.
-
-  `add_zero` is a proof of `∀ x, x + 0 = x`. In other words, it's a function
-  which eats a number `x` and spits out a proof that the two numbers `x + 0` and `x` are *equal*.
-
-  `rw` is a *tactic* which eats a list of equality proofs and then changes the goal.
-
-  Given the goal below, clearly the way to prove it is just to cancel out all the zeros.
-  So try * `rw [add_zero x]`.
-"
-
-LemmaDoc MyNat.add_succ as "add_succ" in "Add"
-"One of the two axioms defining addition. It says `n + (succ m) = succ (n + m)`."
-
-LemmaDoc MyNat.add_zero as "add_zero" in "Add"
-"One of the two axioms defining addition. It says `n + 0 = n`."
-
-Statement
-"For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = \\operatorname{succ}(a)$."
-    : a + succ 0 = succ a := by
-  Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
-  to make progress."
-  Hint (hidden := true) "Explicitely, type `rw [add_succ]`!"
-  rw [add_succ]
-  Hint "Now you see a term of the form `… + 0`, so you can use `add_zero`."
-  Hint (hidden := true) "Explicitely, type `rw [add_zero]`!"
-  Branch
-    simp? -- TODO
-  rw [add_zero]
-  Hint (hidden := true) "Finally both sides are identical."
-  rfl
-
-NewLemma MyNat.add_succ MyNat.add_zero
-NewDefinition Add
-
-Conclusion
-"
-You have finished tutorial world! If you're happy, let's move onto Addition World,
-and learn about proof by induction.
-
-## Inspection time
-
-If you want to examine the proof, toggle \"Editor mode\" and click somewhere
-inside the proof to see the state at that point!
-"
diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean
index e32ae37..17a8a74 100644
--- a/Game/MyNat/Addition.lean
+++ b/Game/MyNat/Addition.lean
@@ -5,16 +5,19 @@ namespace MyNat
 open MyNat
 
 def add : MyNat → MyNat → MyNat
-  | a, 0   => a
+  | a, zero  => a
   | a, MyNat.succ b => MyNat.succ (MyNat.add a b)
 
-instance : Add MyNat where
+instance instAdd : Add MyNat where
   add := MyNat.add
 
 /--
-This theorem proves that if you add zero to a MyNat you get back the same number.
+`add_zero a` is a proof of `a + 0 = a`.
+
+`add_zero` is a `simp` lemma, because if you see `a + 0`
+you usually want to simplify it to `a`.
 -/
-theorem add_zero (a : MyNat) : a + 0 = a := by rfl
+@[simp] theorem add_zero (a : MyNat) : a + 0 = a := by rfl
 
 /--
 This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat.
diff --git a/Game/MyNat/AdvAddition.lean b/Game/MyNat/AdvAddition.lean
index 7b12d58..2082a36 100644
--- a/Game/MyNat/AdvAddition.lean
+++ b/Game/MyNat/AdvAddition.lean
@@ -7,6 +7,6 @@ example (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
   simp
   sorry
 
-axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
+--axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
 
-axiom zero_ne_succ (a : ℕ) : 0 ≠ succ a
+--axiom zero_ne_succ (a : ℕ) : 0 ≠ succ a
diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
index 9ee4a02..ff6a207 100644
--- a/Game/MyNat/DecidableEq.lean
+++ b/Game/MyNat/DecidableEq.lean
@@ -1,4 +1,4 @@
-import Game.Levels.Tutorial.L02rw-- makes simps work?
+import Game.MyNat.Addition-- makes simps work?
 import Mathlib.Tactic
 namespace MyNat
 
@@ -51,7 +51,7 @@ We need to learn how to deal wiht a goal of the form `P → Q`
 
 -/
 
-theorem succ_inj (a b : ℕ) (h : succ a = succ b) : a = b := by
+theorem succ_inj {a b : ℕ} (h : succ a = succ b) : a = b := by
   apply_fun pred at h
   simpa
 
@@ -90,7 +90,7 @@ congrArg pred
 -/
 @[simp] theorem succ_eq_succ_iff : succ a = succ b ↔ a = b := by
   constructor
-  · exact succ_inj a b
+  · exact succ_inj
   · simp
 
 /-