diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean
index 8b75036..7b7a783 100644
--- a/server/nng/NNG.lean
+++ b/server/nng/NNG.lean
@@ -3,13 +3,13 @@ import GameServer.Commands
 import NNG.Levels.Tutorial
 import NNG.Levels.Addition
 import NNG.Levels.Multiplication
--- import NNG.Levels.Power
+import NNG.Levels.Power
 import NNG.Levels.Function
 import NNG.Levels.Proposition
 import NNG.Levels.AdvProposition
 import NNG.Levels.AdvAddition
 import NNG.Levels.AdvMultiplication
--- import NNG.Levels.Inequality
+--import NNG.Levels.Inequality
 
 Game "NNG"
 Title "Natural Number Game"
@@ -57,9 +57,8 @@ If you delete it, your progress will be lost!
 
 "
 
-Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition
-Path AdvAddition → AdvMultiplication -- → Inequality
-Path Addition → Multiplication → AdvMultiplication
--- Path Multiplication → Power
+Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition → AdvMultiplication
+Path Addition → Multiplication → AdvMultiplication -- → Inequality
+Path Multiplication → Power
 
 MakeGame
diff --git a/server/nng/NNG/Doc/Definitions.lean b/server/nng/NNG/Doc/Definitions.lean
index 860c789..5cd0730 100644
--- a/server/nng/NNG/Doc/Definitions.lean
+++ b/server/nng/NNG/Doc/Definitions.lean
@@ -15,6 +15,8 @@ The natural numbers implemented in Lean's core are called `Nat`.
 
 If you end up getting someting of type `Nat` in this game, you probably
 need to write `(4 : ℕ)` to force it to be of type `MyNat`.
+
+*Write with `\\N`.*
 "
 
 DefinitionDoc Add as "+" "
@@ -23,5 +25,64 @@ Addition on `ℕ` is defined through two axioms:
 * `add_zero (a : ℕ) : a + 0 = a`
 * `add_succ (a d : ℕ) : a + succ d = succ (a + d)`
 "
-  
-DefinitionDoc Mul as "*" ""
\ No newline at end of file
+
+DefinitionDoc Pow as "^" "
+Power on `ℕ` is defined through two axioms:
+
+* `pow_zero (a : ℕ) : a ^ 0 = 1`
+* `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`
+
+## Game-specific notes
+
+Note that you might need to manually specify the type of the first number:
+
+```
+(2 : ℕ) ^ 1
+```
+
+If you write `2 ^ 1` then lean will try to work in it's inbuild `Nat`, not in
+the game's natural numbers `MyNat`.
+"
+
+DefinitionDoc One as "1" "
+`1 : ℕ` is by definition `succ 0`. Use `one_eq_succ_zero`
+to change between the two.
+"
+
+DefinitionDoc False as "False" "
+`False` is a proposition that that is always false, in contrast to `True` which is always true.
+
+A proof of `False`, i.e. `(h : False)` is used to implement a contradiction: From a proof of `False`
+anything follows, *ad absurdum*.
+
+For example, \"not\" (`¬ A`) is therefore implemented as `A → False`.
+(\"If `A` is true then we have a contradiction.\")
+"
+
+DefinitionDoc Not as "¬" "
+Logical \"not\" is implemented as `¬ A := A → False`.
+
+*Write with `\\n`.*
+"
+
+DefinitionDoc And as "∧" "
+(missing)
+
+*Write with `\\and`.*
+"
+
+DefinitionDoc Or as "∨" "
+(missing)
+
+*Write with `\\or`.*
+"
+
+DefinitionDoc Iff as "↔" "
+(missing)
+
+*Write with `\\iff`.*
+"
+
+DefinitionDoc Mul as "*" ""
+
+DefinitionDoc Ne as "≠" ""
\ No newline at end of file
diff --git a/server/nng/NNG/Doc/Lemmas.lean b/server/nng/NNG/Doc/Lemmas.lean
index 821b846..e861b84 100644
--- a/server/nng/NNG/Doc/Lemmas.lean
+++ b/server/nng/NNG/Doc/Lemmas.lean
@@ -1,31 +1,37 @@
 import GameServer.Commands
 
-LemmaDoc MyNat.add_zero as "add_zero" in "Nat"
+LemmaDoc MyNat.add_zero as "add_zero" in "Add"
 "`add_zero (a : ℕ) : a + 0 = a`
 
 This is one of the two axioms defining addition on `ℕ`."
 
-LemmaDoc MyNat.add_succ as "add_succ" in "Nat"
+LemmaDoc MyNat.add_succ as "add_succ" in "Add"
 "`add_succ (a d : ℕ) : a + (succ d) = succ (a + d)`
 
 This is the second axiom definiting addition on `ℕ`"
 
-LemmaDoc MyNat.zero_add as "zero_add" in "Nat"
+LemmaDoc MyNat.zero_add as "zero_add" in "Add"
 "(missing)"
 
-LemmaDoc MyNat.add_assoc as "add_assoc" in "Nat"
+LemmaDoc MyNat.add_assoc as "add_assoc" in "Add"
 "(missing)"
 
-LemmaDoc MyNat.succ_add as "succ_add" in "Nat"
+LemmaDoc MyNat.succ_add as "succ_add" in "Add"
 "(missing)"
 
-LemmaDoc MyNat.add_comm as "add_comm" in "Nat"
+LemmaDoc MyNat.add_comm as "add_comm" in "Add"
 "(missing)"
 
 LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "Nat"
 "(missing)"
 
-LemmaDoc not_iff_imp_false as "not_iff_imp_false" in "Prop"
+LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_one_eq_succ as "add_one_eq_succ" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_right_comm as "add_right_comm" in "Add"
 "(missing)"
 
 LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat"
@@ -33,3 +39,130 @@ LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat"
 
 LemmaDoc MyNat.zero_ne_succ as "zero_ne_succ" in "Nat"
 "(missing)"
+
+
+/-? Multiplication World -/
+
+LemmaDoc MyNat.mul_zero as "mul_zero" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_succ as "mul_succ" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.zero_mul as "zero_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_one as "mul_one" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.one_mul as "one_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_add as "mul_add" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_assoc as "mul_assoc" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.succ_mul as "succ_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.add_mul as "add_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_comm as "mul_comm" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_left_comm as "mul_left_comm" in "Mul"
+"(missing)"
+
+
+
+LemmaDoc MyNat.succ_eq_succ_of_eq as "succ_eq_succ_of_eq" in "Nat"
+"(missing)"
+
+LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "Add"
+"(missing)"
+
+LemmaDoc Ne.symm as "Ne.symm" in "Nat"
+"(missing)"
+
+LemmaDoc Eq.symm as "Eq.symm" in "Nat"
+"(missing)"
+
+LemmaDoc Iff.symm as "Iff.symm" in "Nat"
+"(missing)"
+
+LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Add"
+"(missing)"
+  
+LemmaDoc MyNat.add_right_cancel_iff as "add_right_cancel_iff" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.eq_zero_of_add_right_eq_self as "eq_zero_of_add_right_eq_self" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_left_eq_zero as "add_left_eq_zero" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_right_eq_zero as "add_right_eq_zero" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.eq_zero_or_eq_zero_of_mul_eq_zero as "eq_zero_or_eq_zero_of_mul_eq_zero" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_left_cancel as "mul_left_cancel" in "Mul"
+"(missing)"
+
+
+LemmaDoc MyNat.zero_pow_zero as "zero_pow_zero" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_zero as "pow_zero" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_succ as "pow_succ" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.zero_pow_succ as "zero_pow_succ" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_one as "pow_one" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.one_pow as "one_pow" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_add as "pow_add" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.mul_pow as "mul_pow" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_pow as "pow_pow" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
+"(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
diff --git a/server/nng/NNG/Doc/Tactics.lean b/server/nng/NNG/Doc/Tactics.lean
index 1dda959..009fe27 100644
--- a/server/nng/NNG/Doc/Tactics.lean
+++ b/server/nng/NNG/Doc/Tactics.lean
@@ -153,14 +153,34 @@ TacticDoc left
 "
 "
 
+TacticDoc revert
+"
+"
+
+TacticDoc tauto
+"
+"
+
 TacticDoc right
 "
 "
 
+TacticDoc by_cases
+"
+"
+
 TacticDoc contradiction
 "
 "
 
 TacticDoc exfalso
 "
+"
+
+TacticDoc simp
+"
+"
+
+TacticDoc «repeat»
+"
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Addition.lean b/server/nng/NNG/Levels/Addition.lean
index 27e5416..52b5dec 100644
--- a/server/nng/NNG/Levels/Addition.lean
+++ b/server/nng/NNG/Levels/Addition.lean
@@ -1,47 +1,36 @@
-import NNG.Levels.Addition.Level_1
-import NNG.Levels.Addition.Level_2
-import NNG.Levels.Addition.Level_3
-import NNG.Levels.Addition.Level_4
-import NNG.Levels.Addition.Level_5
 import NNG.Levels.Addition.Level_6
 
-
 Game "NNG"
 World "Addition"
 Title "Addition World"
 
 Introduction
 "
-Hi!
-"
-
--- Introduction
--- "
--- Welcome to Addition World. If you've done all four levels in tutorial world
--- and know about `rewrite` and `rfl`, then you're in the right place. Here's
--- a reminder of the things you're now equipped with which we'll need in this world.
+Welcome to Addition World. If you've done all four levels in tutorial world
+and know about `rw` and `rfl`, then you're in the right place. Here's
+a reminder of the things you're now equipped with which we'll need in this world.
 
--- ## Data:
+## Data:
 
---   * a type called `ℕ` or `MyNat`.
---   * a term `0 : ℕ`, interpreted as the number zero.
---   * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\".
---   * Usual numerical notation `0,1,2` etc. (although `2` onwards will be of no use to us until much later ;-) ).
---   * Addition (with notation `a + b`).
+  * a type called `ℕ` or `MyNat`.
+  * a term `0 : ℕ`, interpreted as the number zero.
+  * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\".
+  * Usual numerical notation `0,1,2` etc. (although `2` onwards will be of no use to us until much later ;-) ).
+  * Addition (with notation `a + b`).
 
--- ## Theorems:
+## Theorems:
 
---   * `add_zero (a : ℕ) : a + 0 = a`. Use with `rewrite [add_zero]`.
---   * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rewrite [add_succ]`.
---   * The principle of mathematical induction. Use with `induction` (which we learn about in this chapter).
+  * `add_zero (a : ℕ) : a + 0 = a`. Use with `rw [add_zero]`.
+  * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rw [add_succ]`.
+  * The principle of mathematical induction. Use with `induction` (which we learn about in this chapter).
 
 
--- ## Tactics:
+## Tactics:
 
---   * `rfl` :  proves goals of the form `X = X`.
---   * `rewrite [h]` : if `h` is a proof of `A = B`, changes all `A`'s in the goal to `B`'s.
---   * `induction n with d hd` : we're going to learn this right now.
+  * `rfl` :  proves goals of the form `X = X`.
+  * `rw [h]` : if `h` is a proof of `A = B`, changes all `A`'s in the goal to `B`'s.
+  * `induction n with d hd` : we're going to learn this right now.
 
 
--- You will also find all this information in your Inventory to read the documentation.
--- "
\ No newline at end of file
+You will also find all this information in your Inventory to read the documentation.
+"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Addition/Level_1.lean b/server/nng/NNG/Levels/Addition/Level_1.lean
index f9d0cdc..884d82a 100644
--- a/server/nng/NNG/Levels/Addition/Level_1.lean
+++ b/server/nng/NNG/Levels/Addition/Level_1.lean
@@ -8,8 +8,6 @@ Title "the induction tactic."
 
 open MyNat
 
-set_option tactic.hygienic false
-
 Introduction
 "
 OK so let's see induction in action. We're going to prove
@@ -36,7 +34,7 @@ note that `zero_add` is about zero add something, and `add_zero` is about someth
 The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`.
 "
 
-Statement MyNat.zero_add
+Statement MyNat.zero_add (attr := simp)
 "For all natural numbers $n$, we have $0 + n = n$."
     (n : ℕ) : 0 + n = n := by
   Hint "You can start a proof by induction over `n` by typing:
@@ -56,20 +54,25 @@ Statement MyNat.zero_add
     `{hn} : 0 + {n} = {n}` and you need to prove the statement for `succ {n}`."
     Hint (hidden := true) "look at `add_succ`."
     rw [add_succ]
+    Branch
+      simp? -- TODO
     Hint (hidden := true) "At this point you see the term `0 + {n}`, so you can use the
     induction hypothesis with `rw [{hn}]`."
     rw [hn]
     rfl
 
+attribute [simp] MyNat.zero_add
+
 NewTactic induction
+LemmaTab "Add"
 
 Conclusion
 "
 ## Now venture off on your own.
 
-Those three tactics: 
+Those three tactics:
 
-* `induction n with d hd` 
+* `induction n with d hd`
 * `rw [h]`
 * `rfl`
 
@@ -86,8 +89,7 @@ We're going to stop explaining stuff carefully now. If you get stuck or want
 to know more about Lean (e.g. how to do much harder maths in Lean),
 ask in `#new members` at
 [the Lean chat](https://leanprover.zulipchat.com)
-(login required, real name preferred). Kevin or Mohammad or one of the other
-people there might be able to help.
+(login required, real name preferred). Any of the people there might be able to help.
 
 Good luck! Click on \"Next\" to solve some levels on your own.
 "
diff --git a/server/nng/NNG/Levels/Addition/Level_2.lean b/server/nng/NNG/Levels/Addition/Level_2.lean
index b220ee6..0018018 100644
--- a/server/nng/NNG/Levels/Addition/Level_2.lean
+++ b/server/nng/NNG/Levels/Addition/Level_2.lean
@@ -1,4 +1,3 @@
-import NNG.Metadata
 import NNG.Levels.Addition.Level_1
 
 Game "NNG"
@@ -25,7 +24,7 @@ Statement MyNat.add_assoc
 "On the set of natural numbers, addition is associative.
 In other words, for all natural numbers $a, b$ and $c$, we have
 $ (a + b) + c = a + (b + c). $"
-    (a b c : ℕ) : (a + b) + c = a + (b + c)  := by
+    (a b c : ℕ) : (a + b) + c = a + (b + c) := by
   Hint "Because addition was defined by recursion on the right-most variable,
   use induction on the right-most variable (try other variables at your peril!).
 
@@ -34,8 +33,9 @@ $ (a + b) + c = a + (b + c). $"
   Branch
     induction a
     Hint "Good luck with that…"
-    rw [zero_add, zero_add]
-    rfl
+    simp?
+    --rw [zero_add, zero_add]
+    --rfl
   Branch
     induction b
     Hint "Good luck with that…"
@@ -54,10 +54,5 @@ $ (a + b) + c = a + (b + c). $"
   rw [hc]
   rfl
 
-
-Conclusion
-"
-
-"
-
-NewLemma MyNat.zero_add
\ No newline at end of file
+NewLemma MyNat.zero_add
+LemmaTab "Add"
diff --git a/server/nng/NNG/Levels/Addition/Level_3.lean b/server/nng/NNG/Levels/Addition/Level_3.lean
index 7e63ed4..a8329ce 100644
--- a/server/nng/NNG/Levels/Addition/Level_3.lean
+++ b/server/nng/NNG/Levels/Addition/Level_3.lean
@@ -1,4 +1,3 @@
-import NNG.Metadata
 import NNG.Levels.Addition.Level_2
 
 Game "NNG"
@@ -46,6 +45,8 @@ $ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$."
     rw [add_succ]
     rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/Addition/Level_4.lean b/server/nng/NNG/Levels/Addition/Level_4.lean
index 267ae1e..8a9ad42 100644
--- a/server/nng/NNG/Levels/Addition/Level_4.lean
+++ b/server/nng/NNG/Levels/Addition/Level_4.lean
@@ -1,4 +1,3 @@
-import NNG.Metadata
 import NNG.Levels.Addition.Level_3
 
 Game "NNG"
@@ -21,6 +20,7 @@ Statement MyNat.add_comm
 In other words, for all natural numbers $a$ and $b$, we have
 $a + b = b + a$."
     (a b : ℕ) : a + b = b + a := by
+  Hint (hidden := true) "You might want to start by induction."
   Branch
     induction a with d hd
     · rw [zero_add]
@@ -39,6 +39,8 @@ $a + b = b + a$."
     rw [succ_add]
     rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 If you got this far -- nice! You're nearly ready to make a choice:
diff --git a/server/nng/NNG/Levels/Addition/Level_5.lean b/server/nng/NNG/Levels/Addition/Level_5.lean
index bfa30eb..3367aaf 100644
--- a/server/nng/NNG/Levels/Addition/Level_5.lean
+++ b/server/nng/NNG/Levels/Addition/Level_5.lean
@@ -1,5 +1,3 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
 import NNG.Levels.Addition.Level_4
 
 Game "NNG"
@@ -9,13 +7,11 @@ Title "succ_eq_add_one"
 
 open MyNat
 
-theorem one_eq_succ_zero : (1 : ℕ) = succ 0 := by simp only
-
-NewLemma MyNat.one_eq_succ_zero
+axiom MyNat.one_eq_succ_zero : (1 : ℕ) = succ 0
 
 Introduction
 "
-I've just added `one_eq_succ_zero` (a proof of $1 = \\operatorname{succ}(0)$)
+I've just added `one_eq_succ_zero` (a proof of `1 = succc 0`)
 to your list of theorems; this is true
 by definition of $1$, but we didn't need it until now.
 
@@ -28,7 +24,7 @@ some theorems about $0$ (`zero_add`, `add_zero`), but, other than `1 = succ 0`,
 no theorems at all which mention $1$. Let's prove one now.
 "
 
-Statement --MyNat.succ_eq_add_one
+Statement MyNat.succ_eq_add_one
 "For any natural number $n$, we have
 $ \\operatorname{succ}(n) = n+1$ ."
     (n : ℕ) : succ n = n + 1 := by
@@ -37,6 +33,10 @@ $ \\operatorname{succ}(n) = n+1$ ."
   rw [add_zero]
   rfl
 
+NewLemma MyNat.one_eq_succ_zero
+NewDefinition One
+LemmaTab "Add"
+
 Conclusion
 "
 Well done! On to the last level!
diff --git a/server/nng/NNG/Levels/Addition/Level_6.lean b/server/nng/NNG/Levels/Addition/Level_6.lean
index 44008e0..70fdb5c 100644
--- a/server/nng/NNG/Levels/Addition/Level_6.lean
+++ b/server/nng/NNG/Levels/Addition/Level_6.lean
@@ -1,5 +1,3 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
 import NNG.Levels.Addition.Level_5
 
 Game "NNG"
@@ -25,23 +23,92 @@ then the space bar (note that this is L for left, not a number 1).
 Similarly, if `h : a = b` then `rw [h]` will change `a`'s to `b`'s
 and `rw [← h]` will change `b`'s to `a`'s.
 
-Also, you can be (and will need to be, in this level) more precise
-about where to rewrite theorems. `rw add_comm,` will just find the
-first `? + ?` it sees and swap it around. You can target more specific
-additions like this: `rw add_comm a` will swap around
-additions of the form `a + ?`, and `rw add_comm a b,` will only
-swap additions of the form `a + b`.
+
 "
 
-Statement --add_right_comm
+Statement MyNat.add_right_comm
 "For all natural numbers $a, b$ and $c$, we have
 $a + b + c = a + c + b$."
     (a b c : ℕ) : a + b + c = a + c + b := by
+  Hint (hidden := true) "You want to change your goal to `a + (b + c) = _`
+  so that you can then use commutativity."
   rw [add_assoc]
+  Hint "Here you need to be more precise about where to rewrite theorems.
+  `rw [add_comm]` will just find the
+  first `_ + _` it sees and swap it around. You can target more specific
+  additions like this: `rw [add_comm a]` will swap around
+  additions of the form `a + _`, and `rw [add_comm a b]` will only
+  swap additions of the form `a + b`."
+  Branch
+    rw [add_comm]
+    Hint "`rw [add_comm]` just rewrites to first instance of `_ + _` it finds, which
+    is not what you want to do here. Instead you can provide the arguments explicitely:
+
+    * `rw [add_comm b c]`
+    * `rw [add_comm b]`
+    * `rw [add_comm b _]`
+    * `rw [add_comm _ c]`
+
+    would all have worked. You should go back and try again.
+    "
   rw [add_comm b c]
+  Branch
+    rw [add_assoc]
+    rfl
   rw [←add_assoc]
   rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
+If you have got this far, then you have become very good at
+manipulating equalities in Lean. You can also now collect
+four collectibles (or `instance`s, as Lean calls them)
+
+```
+MyNat.addSemigroup     -- (after level 2)
+MyNat.addMonoid        -- (after level 2)
+MyNat.addCommSemigroup -- (after level 4)
+MyNat.addCommMonoid    -- (after level 4)
+```
+
+These say that `ℕ` is a commutative semigroup/monoid.
+
+In Multiplication World you will be able to collect such
+advanced collectibles as `MyNat.commSemiring` and
+`MyNat.distrib`, and then move on to power world and
+the famous collectible at the end of it.
+
+One last thing -- didn't you think that solving this level
+`add_right_comm` was boring? Check out this AI that can do it for us.
+
+From now on, the `simp` AI becomes accessible (it's just an advanced
+tactic really), and can nail some really tedious-for-a-human-to-solve
+goals. For example check out this one-line proof:
+
+```
+example (a b c d e : ℕ ) :
+    (((a + b) + c) + d) + e = (c + ((b + e) + a)) + d := by
+  simp
+```
+
+Imagine having to do that one by hand! The AI closes the goal
+because it knows how to use associativity and commutativity
+sensibly in a commutative monoid.
+
+You are now done with addition world. Go back to the main menu (top left)
+and decide whether to press on with multiplication world and power world
+(which can be solved with `rw`, `refl` and `induction`), or to go on
+to Function World where you can learn the tactics needed to prove
+goals of the form $P\\implies Q$, thus enabling you to solve more
+advanced addition world levels such as $a+t=b+t\\implies a=b$. Note that
+Function World is more challenging mathematically; but if you can do Addition
+World you can surely do Multiplication World and Power World.
 "
+
+-- First we have to get the `AddCommMonoid` collectible,
+-- which we do by saying the magic words which make Lean's type class inference
+-- system give it to us.
+-- -/
+-- instance : add_comm_monoid mynat := by structure_helper
diff --git a/server/nng/NNG/Levels/AdvAddition.lean b/server/nng/NNG/Levels/AdvAddition.lean
index 129b734..6be2f2b 100644
--- a/server/nng/NNG/Levels/AdvAddition.lean
+++ b/server/nng/NNG/Levels/AdvAddition.lean
@@ -1,23 +1,28 @@
-import NNG.Levels.AdvAddition.Level_1
-import NNG.Levels.AdvAddition.Level_2
-import NNG.Levels.AdvAddition.Level_3
-import NNG.Levels.AdvAddition.Level_4
-import NNG.Levels.AdvAddition.Level_5
-import NNG.Levels.AdvAddition.Level_6
-import NNG.Levels.AdvAddition.Level_7
-import NNG.Levels.AdvAddition.Level_8
-import NNG.Levels.AdvAddition.Level_9
-import NNG.Levels.AdvAddition.Level_10
-import NNG.Levels.AdvAddition.Level_11
-import NNG.Levels.AdvAddition.Level_12
 import NNG.Levels.AdvAddition.Level_13
 
-
 Game "NNG"
 World "AdvAddition"
 Title "Advanced Addition World"
 
 Introduction
 "
-  Hi
+Peano's original collection of axioms for the natural numbers contained two further
+assumptions, which have not yet been mentioned in the game:
+
+```
+succ_inj (a b : ℕ) :
+  succ a = succ b → a = b
+
+zero_ne_succ (a : ℕ) :
+  zero ≠ succ a
+```
+
+The reason they have not been used yet is that they are both implications,
+that is,
+of the form $P\\implies Q$. This is clear for `succ_inj a b`, which
+says that for all $a$ and $b$ we have $\\operatorname{succ}(a)=\\operatorname{succ}(b)\\implies a=b$.
+For `zero_ne_succ` the trick is that $X\\ne Y$ is *defined to mean*
+$X = Y\\implies{\\tt False}$. If you have played through proposition world,
+you now have the required Lean skills (i.e., you know the required
+tactics) to work with these implications.
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_1.lean b/server/nng/NNG/Levels/AdvAddition/Level_1.lean
index 622fcc9..e1aee09 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_1.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_1.lean
@@ -1,5 +1,6 @@
 import NNG.Metadata
 import NNG.MyNat.AdvAddition
+import NNG.Levels.Addition
 
 Game "NNG"
 World "AdvAddition"
@@ -10,44 +11,35 @@ open MyNat
 
 Introduction
 "
-Peano's original collection of axioms for the natural numbers contained two further
-assumptions, which have not yet been mentioned in the game:
+Let's finally learn how to use `succ_inj`:
 
 ```
-succ_inj {a b : mynat} :
-  succ(a) = succ(b) → a = b
-
-zero_ne_succ (a : mynat) :
-  zero ≠ succ(a)
- ```
-
-The reason they have not been used yet is that they are both implications,
-that is,
-of the form $P\\implies Q$. This is clear for `succ_inj a b`, which
-says that for all $a$ and $b$ we have $succ(a)=succ(b)\\implies a=b$.
-For `zero_ne_succ` the trick is that $X\ne Y$ is *defined to mean*
-$X = Y\\implies{\\tt false}$. If you have played through Proposition world,
-you now have the required Lean skills (i.e., you know the required
-tactics) to work with these implications.
-Let's finally learn how to use `succ_inj`. You should know a couple
-of ways to prove the below -- one directly using an `exact`,
-and one which uses an `apply` first. But either way you'll need to use `succ_inj`.
+succ_inj (a b : ℕ) :
+  succ a = succ b → a = b
+```
 "
 
 Statement -- MyNat.succ_inj'
-"For all naturals $a$ and $b$, if we assume $succ(a)=succ(b)$, then we can
-deduce $a=b$."
+"For all naturals $a$ and $b$, if we assume $\\operatorname{succ}(a)=\\operatorname{succ}(b)$,
+then we can deduce $a=b$."
     {a b : ℕ} (hs : succ a = succ b) :  a = b := by
-    exact succ_inj hs
+  Hint "You should know a couple
+  of ways to prove the below -- one directly using an `exact`,
+  and one which uses an `apply` first. But either way you'll need to use `succ_inj`."
+  Branch
+    apply succ_inj
+    exact hs
+  exact succ_inj hs
 
-NewLemma MyNat.succ_inj MyNat.zero_ne_succ
+NewLemma MyNat.succ_inj
+LemmaTab "Nat"
 
 Conclusion
 "
-## Important thing.
+**Important thing**:
 
-You can rewrite proofs of *equalities*. If `h : A = B` then `rw h` changes `A`s to `B`s.
-But you *cannot rewrite proofs of implications*. `rw succ_inj` will *never work*
+You can rewrite proofs of *equalities*. If `h : A = B` then `rw [h]` changes `A`s to `B`s.
+But you *cannot rewrite proofs of implications*. `rw [succ_inj]` will *never work*
 because `succ_inj` isn't of the form $A = B$, it's of the form $A\\implies B$. This is one
 of the most common mistakes I see from beginners. $\\implies$ and $=$ are *two different things*
 and you need to be clear about which one you are using.
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_10.lean b/server/nng/NNG/Levels/AdvAddition/Level_10.lean
index e591844..8e92bb8 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_10.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_10.lean
@@ -1,6 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
-import NNG.MyNat.Multiplication
+import NNG.Levels.AdvAddition.Level_9
+import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvAddition"
@@ -11,64 +10,66 @@ open MyNat
 
 Introduction
 "
-In Lean, `a ≠ b` is *defined to mean* `(a = b) → false`. 
+In Lean, `a ≠ b` is *defined to mean* `(a = b) → False`.
 This means that if you see `a ≠ b` you can *literally treat
-it as saying* `(a = b) → false`. Computer scientists would
-say that these two terms are *definitionally equal*. 
+it as saying* `(a = b) → False`. Computer scientists would
+say that these two terms are *definitionally equal*.
 
 The following lemma, $a+b=0\\implies b=0$, will be useful in inequality world.
-Let me go through the proof, because it introduces several new
-concepts: 
-
-* `cases b`, where `b : mynat`
-* `exfalso`
-* `apply succ_ne_zero`
-
-We're going to prove $a+b=0\\implies b=0$. Here is the
-strategy. Each natural number is either `0` or `succ(d)` for
-some other natural number `d`. So we can start the proof
-with 
-
-`cases b with d,`
-
-and then we have two goals, the case `b = 0` (which you can solve easily)
-and the case `b = succ(d)`, which looks like this:
-
-```
-a d : mynat,
-H : a + succ d = 0
-⊢ succ d = 0
-```
-
-Our goal is impossible to prove. However our hypothesis `H`
-is also impossible, meaning that we still have a chance!
-First let's see why `H` is impossible. We can
-
-`rw add_succ at H,`
-
-to turn `H` into `H : succ (a + d) = 0`. Because
-`succ_ne_zero (a + d)` is a proof that `succ (a + d) ≠ 0`,
-it is also a proof of the implication `succ (a + d) = 0 → false`.
-Hence `succ_ne_zero (a + d) H` is a proof of `false`!
-Unfortunately our goal is not `false`, it's a generic
-false statement. 
-
-Recall however that the `exfalso` command turns any goal into `false`
-(it's logically OK because `false` implies every proposition, true or false).
-You can probably take it from here.
 "
 
-Statement -- add_left_eq_zero
-"If $a$ and $b$ are natural numbers such that 
+Statement MyNat.add_left_eq_zero
+"If $a$ and $b$ are natural numbers such that
 $$ a + b = 0, $$
 then $b = 0$."
-    {{a b : ℕ}} (H : a + b = 0) : b = 0 := by
+    {a b : ℕ} (h : a + b = 0) : b = 0 := by
+  Hint "
+  You want to start of by making a distinction `b = 0` or `b = succ d` for some
+  `d`. You can do this with
+
+  ```
+  induction b
+  ```
+  even if you are never going to use the induction hypothesis.
+  "
+
+  -- TODO: induction vs rcases
+
+  Branch
+    rcases b
+    -- TODO: `⊢ zero = 0` :(
   induction b with d
-  rfl
-  rw [add_succ] at H
-  exfalso
-  apply succ_ne_zero (a + d)
-  exact H
+  · rfl
+  · Hint "This goal seems impossible! However, our hypothesis `h` is also impossible,
+    meaning that we still have a chance!
+    First let's see why `h` is impossible. We can
+
+    ```
+    rw [add_succ] at h
+    ```
+    "
+    rw [add_succ] at h
+    Hint "
+    Because `succ_ne_zero (a + {d})` is a proof that `succ (a + {d}) ≠ 0`,
+    it is also a proof of the implication `succ (a + {d}) = 0 → False`.
+    Hence `succ_ne_zero (a + {d}) h` is a proof of `False`!
+
+    Unfortunately our goal is not `False`, it's a generic
+    false statement.
+
+    Recall however that the `exfalso` command turns any goal into `False`
+    (it's logically OK because `False` implies every proposition, true or false).
+    You can probably take it from here.
+    "
+    Branch
+      have j := succ_ne_zero (a + d) h
+      exfalso
+      exact j
+    exfalso
+    apply succ_ne_zero (a + d)
+    exact h
+
+LemmaTab "Add"
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_11.lean b/server/nng/NNG/Levels/AdvAddition/Level_11.lean
index 526f92c..ffde445 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_11.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_11.lean
@@ -1,5 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_10
 
 Game "NNG"
 World "AdvAddition"
@@ -8,22 +7,22 @@ Title "add_right_eq_zero"
 
 open MyNat
 
-theorem MyNat.add_left_eq_zero {{a b : ℕ}} (H : a + b = 0) : b = 0 := by sorry
-
 Introduction
 "
-We just proved `add_left_eq_zero (a b : mynat) : a + b = 0 → b = 0`.
+We just proved `add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0`.
 Hopefully `add_right_eq_zero` shouldn't be too hard now.
 "
 
-Statement
-"If $a$ and $b$ are natural numbers such that 
+Statement MyNat.add_right_eq_zero
+"If $a$ and $b$ are natural numbers such that
 $$ a + b = 0, $$
 then $a = 0$."
     {a b : ℕ} : a + b = 0 → a = 0 := by
-  intro H
-  rw [add_comm] at H
-  exact add_left_eq_zero H
+  intro h
+  rw [add_comm] at h
+  exact add_left_eq_zero h
+
+LemmaTab "Add"
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_12.lean b/server/nng/NNG/Levels/AdvAddition/Level_12.lean
index a6df33c..8995e0f 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_12.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_12.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_11
+
 
 Game "NNG"
 World "AdvAddition"
@@ -12,20 +12,22 @@ Introduction
 "
 We have
 
-  * `succ_eq_add_one (n : mynat) : succ n = n + 1`
+```
+succ_eq_add_one (n : ℕ) : succ n = n + 1
+```
 
 but sometimes the other way is also convenient.
 "
 
-theorem succ_eq_add_one (d : ℕ) : succ d = d + 1 := by sorry
-
-Statement
+Statement MyNat.add_one_eq_succ
 "For any natural number $d$, we have
 $$ d+1 = \\operatorname{succ}(d). $$"
     (d : ℕ) : d + 1 = succ d := by
   rw [succ_eq_add_one]
   rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_13.lean b/server/nng/NNG/Levels/AdvAddition/Level_13.lean
index 663a292..d664492 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_13.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_13.lean
@@ -1,5 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_12
 
 Game "NNG"
 World "AdvAddition"
@@ -11,24 +10,29 @@ open MyNat
 Introduction
 "
 The last level in Advanced Addition World is the statement
-that $n\\not=\\operatorname{succ}(n)$. When you've done this
-you've completed Advanced Addition World and can move on
-to Advanced Multiplication World (after first doing
-Multiplication World, if you didn't do it already). 
+that $n\\not=\\operatorname{succ}(n)$.
 "
 
 Statement --ne_succ_self
 "For any natural number $n$, we have
 $$ n \\neq \\operatorname{succ}(n). $$"
      (n : ℕ) : n ≠ succ n := by
+  Hint (hidden := true) "I would start a proof by induction on `n`."
   induction n with d hd
-  apply zero_ne_succ
-  intro hs
-  apply hd
-  apply succ_inj
-  assumption
+  · apply zero_ne_succ
+  · Hint (hidden := true) "If you have no clue, you could start with `rw [Ne, Not]`."
+    Branch
+      rw [Ne, Not]
+    intro hs
+    apply hd
+    apply succ_inj
+    exact hs
+
+LemmaTab "Nat"
 
 Conclusion
 "
-
+Congratulations. You've completed Advanced Addition World and can move on
+to Advanced Multiplication World (after first doing
+Multiplication World, if you didn't do it already).
 "
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_2.lean b/server/nng/NNG/Levels/AdvAddition/Level_2.lean
index dceae92..97937fd 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_2.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_2.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_1
+
 
 Game "NNG"
 World "AdvAddition"
@@ -11,43 +11,46 @@ open MyNat
 Introduction
 "
 In the below theorem, we need to apply `succ_inj` twice. Once to prove
-$succ(succ(a))=succ(succ(b))\\implies succ(a)=succ(b)$, and then again
-to prove $succ(a)=succ(b)\\implies a=b$. However `succ(a)=succ(b)` is
+$\\operatorname{succ}(\\operatorname{succ}(a))=\\operatorname{succ}(\\operatorname{succ}(b))
+\\implies \\operatorname{succ}(a)=\\operatorname{succ}(b)$, and then again
+to prove $\\operatorname{succ}(a)=\\operatorname{succ}(b)\\implies a=b$.
+However `succ a = succ b` is
 nowhere to be found, it's neither an assumption or a goal when we start
 this level. You can make it with `have` or you can use `apply`.
 "
 
 Statement
-"For all naturals $a$ and $b$, if we assume $succ(succ(a))=succ(succ(b))$, then we can
-deduce $a=b$. "
-    {a b : ℕ} (h : succ (succ a) = succ ( succ b )) : a = b := by
+"For all naturals $a$ and $b$, if we assume
+$\\operatorname{succ}(\\operatorname{succ}(a))=\\operatorname{succ}(\\operatorname{succ}(b))$,
+then we can deduce $a=b$. "
+    {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
+  Branch
+    exact succ_inj (succ_inj h)
   apply succ_inj
   apply succ_inj
   assumption
 
+LemmaTab "Nat"
+
 Conclusion
 "
-## Sample solutions to this level. 
+## Sample solutions to this level.
 
 Make sure you understand them all. And remember that `rw` should not be used
 with `succ_inj` -- `rw` works only with equalities or `↔` statements,
 not implications or functions.
 
-example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
-begin
-  apply succ_inj,
-  apply succ_inj,
+```
+example {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
+  apply succ_inj
+  apply succ_inj
   exact h
-end 
-
-example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
-begin
-  apply succ_inj,
-  exact succ_inj(h),
-end 
-
-example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
-begin
-  exact succ_inj(succ_inj(h)),
-end 
+
+example {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
+  apply succ_inj
+  exact succ_inj h
+
+example {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
+  exact succ_inj (succ_inj h)
+```
 "
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_3.lean b/server/nng/NNG/Levels/AdvAddition/Level_3.lean
index 8d8cc21..2ed3998 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_3.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_3.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_2
+
 
 Game "NNG"
 World "AdvAddition"
@@ -11,20 +11,18 @@ open MyNat
 Introduction
 "
 We are going to prove something completely obvious: if $a=b$ then
-$succ(a)=succ(b)$. This is *not* `succ_inj`!
-This is trivial -- we can just rewrite our proof of `a=b`.
-But how do we get to that proof? Use the `intro` tactic.
+$\\operatorname{succ}(a)=\\operatorname{succ}(b)$. This is *not* `succ_inj`!
 "
 
-Statement
-"For all naturals $a$ and $b$, $a=b\\implies succ(a)=succ(b)$. 
-"
+Statement MyNat.succ_eq_succ_of_eq
+"For all naturals $a$ and $b$, $a=b\\implies \\operatorname{succ}(a)=\\operatorname{succ}(b)$."
     {a b : ℕ} : a = b → succ a = succ b := by
+  Hint "This is trivial -- we can just rewrite our proof of `a=b`.
+  But how do we get to that proof? Use the `intro` tactic."
   intro h
+  Hint "Now we can indeed just `rw` `a` to `b`."
   rw [h]
+  Hint (hidden := true) "Recall that `rfl` closes these goals."
   rfl
 
-Conclusion
-"
-
-"
+LemmaTab "Nat"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_4.lean b/server/nng/NNG/Levels/AdvAddition/Level_4.lean
index 5fdad86..42e3afd 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_4.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_4.lean
@@ -1,5 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_3
 
 Game "NNG"
 World "AdvAddition"
@@ -11,19 +10,7 @@ open MyNat
 Introduction
 "
 Here is an `iff` goal. You can split it into two goals (the implications in both
-directions) using the `split` tactic, which is how you're going to have to start.
-
-`split,`
-
-Now you have two goals. The first is exactly `succ_inj` so you can close
-it with
-
-`exact succ_inj,`
-
-and the second one you could solve by looking up the name of the theorem
-you proved in the last level and doing `exact <that name>`, or alternatively
-you could get some more `intro` practice and seeing if you can prove it
-using `intro`, `rw` and `refl`.
+directions) using the `constructor` tactic, which is how you're going to have to start.
 "
 
 Statement
@@ -31,10 +18,25 @@ Statement
 "
     (a b : ℕ) : succ a = succ b ↔ a = b := by
   constructor
+  Hint "Now you have two goals. The first is exactly `succ_inj` so you can close
+  it with
+
+  ```
   exact succ_inj
-  intro H
-  rw [H]
-  rfl
+  ```
+  "
+  · exact succ_inj
+  · Hint "The second one you could solve by looking up the name of the theorem
+    you proved in the last level and doing `exact <that name>`, or alternatively
+    you could get some more `intro` practice and seeing if you can prove it
+    using `intro`, `rw` and `rfl`."
+    Branch
+      exact succ_eq_succ_of_eq
+    intro h
+    rw [h]
+    rfl
+
+LemmaTab "Nat"
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_5.lean b/server/nng/NNG/Levels/AdvAddition/Level_5.lean
index d46fcba..98b09b3 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_5.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_5.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_4
+
 
 Game "NNG"
 World "AdvAddition"
@@ -11,18 +11,19 @@ open MyNat
 Introduction
 "
 The theorem `add_right_cancel` is the theorem that you can cancel on the right
-when you're doing addition -- if `a + t = b + t` then `a = b`. After `intro h`
-I'd recommend induction on `t`. Don't forget that `rw add_zero at h` can be used
-to do rewriting of hypotheses rather than the goal.
+when you're doing addition -- if `a + t = b + t` then `a = b`. 
 "
 
-Statement
+Statement MyNat.add_right_cancel
 "On the set of natural numbers, addition has the right cancellation property.
 In other words, if there are natural numbers $a, b$ and $c$ such that
 $$ a + t = b + t, $$
 then we have $a = b$."
     (a t b : ℕ) : a + t = b + t → a = b := by
+  Hint (hidden := true) "You should start with `intro`."
   intro h
+  Hint "I'd recommend now induction on `t`. Don't forget that `rw [add_zero] at h` can be used
+  to do rewriting of hypotheses rather than the goal."
   induction t with d hd
   rw [add_zero] at h
   rw [add_zero] at h
@@ -30,8 +31,13 @@ then we have $a = b$."
   apply hd
   rw [add_succ] at h
   rw [add_succ] at h
+  Hint (hidden := true) "At this point `succ_inj` might be useful."
   exact succ_inj h
 
+-- TODO: Display at this level after induction is confusing: old assumption floating in context
+
+LemmaTab "Add"
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_6.lean b/server/nng/NNG/Levels/AdvAddition/Level_6.lean
index 47f6332..3004e97 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_6.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_6.lean
@@ -1,5 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_5
 
 Game "NNG"
 World "AdvAddition"
@@ -11,23 +10,27 @@ open MyNat
 Introduction
 "
 The theorem `add_left_cancel` is the theorem that you can cancel on the left
-when you're doing addition -- if `t + a = t + b` then `a = b`. 
-There is a three-line proof which ends in `exact add_right_cancel a t b` (or even
-`exact add_right_cancel _ _ _`); this
-strategy involves changing the goal to the statement of `add_right_cancel` somehow.
-
+when you're doing addition -- if `t + a = t + b` then `a = b`.
 "
 
-Statement
+Statement MyNat.add_left_cancel
 "On the set of natural numbers, addition has the left cancellation property.
 In other words, if there are natural numbers $a, b$ and $t$ such that
 $$ t + a = t + b, $$
 then we have $a = b$."
     (t a b : ℕ) : t + a = t + b → a = b := by
+  Hint "There is a three-line proof which ends in `exact add_right_cancel a t b` (or even
+  `exact add_right_cancel _ _ _`); this
+  strategy involves changing the goal to the statement of `add_right_cancel` somehow."
   rw [add_comm]
   rw [add_comm t]
+  Hint "Now that looks like `add_right_cancel`!"
+  Hint (hidden := true) "`exact add_right_cancel` does not work. You need
+  `exact add_right_cancel a t b` or `exact add_right_cancel _ _ _`."
   exact add_right_cancel a t b
 
+LemmaTab "Add"
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_7.lean b/server/nng/NNG/Levels/AdvAddition/Level_7.lean
index d17bdf1..15d1c7d 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_7.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_7.lean
@@ -1,5 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_6
 
 Game "NNG"
 World "AdvAddition"
@@ -11,25 +10,21 @@ open MyNat
 Introduction
 "
 It's sometimes convenient to have the \"if and only if\" version
-of theorems like `add_right_cancel`. Remember that you can use `split`
+of theorems like `add_right_cancel`. Remember that you can use `constructor`
 to split an `↔` goal into the `→` goal and the `←` goal.
-
-## Pro tip:
-
-`exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\"
 "
 
-Statement --add_right_cancel_iff 
-"For all naturals $a$, $b$ and $t$, 
+Statement MyNat.add_right_cancel_iff
+"For all naturals $a$, $b$ and $t$,
 $$ a + t = b + t\\iff a=b. $$
 "
     (t a b : ℕ) :  a + t = b + t ↔ a = b := by
   constructor
-  exact add_right_cancel _ _ _ -- done that way already,
-  intro H -- H : a = b,
-  rw [H]
-  rfl
-Conclusion
-"
+  · Hint "Pro tip: `exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\"."
+    exact add_right_cancel _ _ _
+  · intro H
+    rw [H]
+    rfl
+
+LemmaTab "Add"
 
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_8.lean b/server/nng/NNG/Levels/AdvAddition/Level_8.lean
index ff5ffad..53d0cee 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_8.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_8.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_7
+
 
 Game "NNG"
 World "AdvAddition"
@@ -14,17 +14,20 @@ The lemma you're about to prove will be useful when we want to prove that $\\leq
 There are some wrong paths that you can take with this one.
 "
 
-Statement --eq_zero_of_add_right_eq_self
-"If $a$ and $b$ are natural numbers such that 
+Statement MyNat.eq_zero_of_add_right_eq_self
+"If $a$ and $b$ are natural numbers such that
 $$ a + b = a, $$
 then $b = 0$."
     {a b : ℕ} : a + b = a → b = 0 := by
   intro h
+  Hint (hidden := true) "Look at `add_left_cancel`."
   apply add_left_cancel a
   rw [h]
   rw [add_zero]
   rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_9.lean b/server/nng/NNG/Levels/AdvAddition/Level_9.lean
index 1563958..1dd69d2 100644
--- a/server/nng/NNG/Levels/AdvAddition/Level_9.lean
+++ b/server/nng/NNG/Levels/AdvAddition/Level_9.lean
@@ -1,5 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.AdvAddition
+import NNG.Levels.AdvAddition.Level_8
 
 Game "NNG"
 World "AdvAddition"
@@ -11,23 +10,43 @@ open MyNat
 Introduction
 "
 Levels 9 to 13 introduce the last axiom of Peano, namely
-that $0\\not=\\operatorname{succ}(a)$. The proof of this is called `zero_ne_succ a`. 
+that $0\\not=\\operatorname{succ}(a)$. The proof of this is called `zero_ne_succ a`.
 
-`zero_ne_succ (a : mynat) : 0 ≠ succ(a)`
+```
+zero_ne_succ (a : ¬) : 0 ≠ succ a
+```
 
-The `symmetry` tactic will turn any goal of the form `R x y` into `R y x`,
-if `R` is a symmetric binary relation (for example `=` or `≠`).
-In particular, you can prove `succ_ne_zero` below by first using
-`symmetry` and then `exact zero_ne_succ a`. 
+$X\\ne Y$ is *defined to mean* $X = Y\\implies{\\tt False}$, similar to how `¬A` was defined.
 "
+-- TODO: I dont think there is a `symmetry` tactic anymore.
+-- The `symmetry` tactic will turn any goal of the form `R x y` into `R y x`,
+-- if `R` is a symmetric binary relation (for example `=` or `≠`).
+-- In particular, you can prove `succ_ne_zero` below by first using
+-- `symmetry` and then `exact zero_ne_succ a`.
 
-Statement -- succ_ne_zero
+Statement MyNat.succ_ne_zero
 "Zero is not the successor of any natural number."
     (a : ℕ) : succ a ≠ 0 := by
+  Hint "You have several options how to start. One would be to recall that `≠` is defined as
+  `(· = ·) → False` and start with `intro`. Or do `rw [Ne, Not]` to explicitely remove the
+  `≠`. Or you could use the lemma `Ne.symm (a b : ℕ) : a ≠ b → b ≠ a` which I just added to your
+  inventory."
+  Branch
+    rw [Ne, Not]
+    intro h
+    apply zero_ne_succ a
+    rw [h]
+    rfl
+  Branch
+    exact (zero_ne_succ a).symm
   apply Ne.symm
   exact zero_ne_succ a
 
 
+NewLemma MyNat.zero_ne_succ Ne.symm Eq.symm Iff.symm
+NewDefinition Ne
+LemmaTab "Nat"
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/AdvMultiplication.lean b/server/nng/NNG/Levels/AdvMultiplication.lean
index 903e3d9..b13e064 100644
--- a/server/nng/NNG/Levels/AdvMultiplication.lean
+++ b/server/nng/NNG/Levels/AdvMultiplication.lean
@@ -10,4 +10,8 @@ Title "Advanced Multiplication World"
 
 Introduction
 "
+Welcome to Advanced Multiplication World! Before attempting this
+world you should have completed seven other worlds, including
+Multiplication World and Advanced Addition World. There are four
+levels in this world.
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean
index 1efa887..0f87b1c 100644
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean
+++ b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean
@@ -1,7 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.Multiplication
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
+import NNG.Levels.Multiplication
+import NNG.Levels.AdvAddition
 
 Game "NNG"
 World "AdvMultiplication"
@@ -12,28 +10,24 @@ open MyNat
 
 Introduction
 "
-Welcome to Advanced Multiplication World! Before attempting this
-world you should have completed seven other worlds, including
-Multiplication World and Advanced Addition World. There are four
-levels in this world.
-
-Recall that if `b : mynat` is a hypothesis and you do `cases b with n`,
-your one goal will split into two goals, 
-namely the cases `b = 0` and `b = succ(n)`. So `cases` here is like
-a weaker version of induction (you don't get the inductive hypothesis).
-
 ## Tricks
 
-1) if your goal is `⊢ X ≠ Y` then `intro h` will give you `h : X = Y` and
-a goal of `⊢ false`. This is because `X ≠ Y` *means* `(X = Y) → false`.
-Conversely if your goal is `false` and you have `h : X ≠ Y` as a hypothesis
+1) if your goal is `X ≠ Y` then `intro h` will give you `h : X = Y` and
+a goal of `False`. This is because `X ≠ Y` *means* `(X = Y) → False`.
+Conversely if your goal is `False` and you have `h : X ≠ Y` as a hypothesis
 then `apply h` will turn the goal into `X = Y`.
 
-2) if `hab : succ (3 * x + 2 * y + 1) = 0` is a hypothesis and your goal is `⊢ false`,
+2) if `hab : succ (3 * x + 2 * y + 1) = 0` is a hypothesis and your goal is `False`,
 then `exact succ_ne_zero _ hab` will solve the goal, because Lean will figure
 out that `_` is supposed to be `3 * x + 2 * y + 1`.
 
 "
+-- TODO: cases
+-- Recall that if `b : ℕ` is a hypothesis and you do `cases b with n`,
+-- your one goal will split into two goals,
+-- namely the cases `b = 0` and `b = succ n`. So `cases` here is like
+-- a weaker version of induction (you don't get the inductive hypothesis).
+
 
 Statement
 "The product of two non-zero natural numbers is non-zero."
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean
index 1d78a7b..5f0c945 100644
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean
+++ b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean
@@ -1,7 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.Multiplication
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
+import NNG.Levels.AdvMultiplication.Level_1
 
 Game "NNG"
 World "AdvMultiplication"
@@ -15,14 +12,14 @@ Introduction
 A variant on the previous level.
 "
 
-Statement -- eq_zero_or_eq_zero_of_mul_eq_zero
+Statement MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
 "If $ab = 0$, then at least one of $a$ or $b$ is equal to zero."
     (a b : ℕ) (h : a * b = 0) :
   a = 0 ∨ b = 0 := by
   induction a with d
   left
   rfl
-  induction b with e he
+  induction b with e
   right
   rfl
   exfalso
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean
index 4f67dca..42bca60 100644
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean
+++ b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean
@@ -1,7 +1,5 @@
-import NNG.Metadata
-import NNG.MyNat.Multiplication
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
+import NNG.Levels.AdvMultiplication.Level_2
+
 
 Game "NNG"
 World "AdvMultiplication"
@@ -15,13 +13,10 @@ Introduction
 Now you have `eq_zero_or_eq_zero_of_mul_eq_zero` this is pretty straightforward.
 "
 
-axiom eq_zero_or_eq_zero_of_mul_eq_zero (a b : ℕ) (h : a * b = 0) : a = 0 ∨ b = 0 
-axiom zero_mul (a : ℕ) : 0 * a = 0
-
 Statement
 "$ab = 0$, if and only if at least one of $a$ or $b$ is equal to zero.
 "
-    (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 := by
+    {a b : ℕ} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
   constructor
   intro h
   exact eq_zero_or_eq_zero_of_mul_eq_zero a b h
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean
index 0f8068f..edf732d 100644
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean
+++ b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean
@@ -1,7 +1,4 @@
-import NNG.Metadata
-import NNG.MyNat.Multiplication
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
+import NNG.Levels.AdvMultiplication.Level_3
 
 Game "NNG"
 World "AdvMultiplication"
@@ -19,14 +16,17 @@ People find this level hard. I have probably had more questions about this
 level than all the other levels put together, in fact. Many levels in this
 game can just be solved by \"running at it\" -- do induction on one of the
 variables, keep your head, and you're done. In fact, if you like a challenge,
-it might be instructive if you stop reading after the end of this paragraph and try solving this level now by induction,
-seeing the trouble you run into, and reading the rest of these comments afterwards. This level
+it might be instructive if you stop reading after the end of this paragraph
+and try solving this level now by induction,
+seeing the trouble you run into, and reading the rest of these comments afterwards.
+This level
 has a sting in the tail. If you are a competent mathematician, try
 and figure out what is going on. Write down a maths proof of the
 theorem in this level. Exactly what statement do you want to prove
 by induction? It is subtle.
 
-Ok so here are some spoilers. The problem with naively running at it, is that if you try induction on,
+Ok so here are some spoilers. The problem with naively running at it,
+is that if you try induction on,
 say, $c$, then you are imagining a and b as fixed, and your inductive
 hypothesis $P(c)$ is $ab=ac \\implies b=c$. So for your inductive step
 you will be able to assume $ab=ad \\implies b=d$ and your goal will
@@ -36,30 +36,64 @@ $ab=ad$ is not true! The statement $P(c)$ (with $a$ and $b$ regarded
 as constants) is not provable by induction.
 
 What you *can* prove by induction is the following *stronger* statement.
-Imagine $a\not=0$ as fixed, and then prove \"for all $b$, if $ab=ac$ then $b=c$\"
+Imagine $a\\ne 0$ as fixed, and then prove \"for all $b$, if $ab=ac$ then $b=c$\"
 by induction on $c$. This gives us the extra flexibility we require.
 Note that we are quantifying over all $b$ in the inductive hypothesis -- it
-is essential that $b$ is not fixed. 
+is essential that $b$ is not fixed.
 
 You can do this in two ways in Lean -- before you start the induction
-you can write `revert b,`. The `revert` tactic is the opposite of the `intro`
+you can write `revert b`. The `revert` tactic is the opposite of the `intro`
 tactic; it replaces the `b` in the hypotheses with \"for all $b$\" in the goal.
 
-Alternatively, you can write `induction c with d hd
-generalizing b` as the first line of the proof. 
+[TODO: The second way does not work yet in this game]
 
 If you do not modify your technique in this way, then this level seems
 to be impossible (judging by the comments I've had about it!)
 "
+-- Alternatively, you can write `induction c with d hd
+-- generalizing b` as the first line of the proof.
 
-Statement
+
+Statement MyNat.mul_left_cancel
 "If $a \\neq 0$, $b$ and $c$ are natural numbers such that
 $ ab = ac, $
 then $b = c$."
     (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c := by
-  sorry
+  Hint "NOTE: As is, this level is probably too hard and contains no hints yet.
+  Good luck!
+
+  Your first step should be `revert b`!"
+  revert b
+  induction c with c hc
+  · intro b hb
+    rw [mul_zero] at hb
+    rcases eq_zero_or_eq_zero_of_mul_eq_zero _ _ hb
+    exfalso
+    apply ha
+    exact h
+    exact h
+  · intro b h
+    induction b with b hb
+    exfalso
+    apply ha
+    rw [mul_zero] at h
+    rcases eq_zero_or_eq_zero_of_mul_eq_zero _ _ h.symm with h | h
+    exact h
+    exfalso
+    exact succ_ne_zero _ h
+    rw [mul_succ, mul_succ] at h
+    have j : b = c
+    apply hc
+    exact add_right_cancel _ _ _ h
+    rw [j]
+    rfl
+-- TODO: generalizing b.
+
+NewTactic revert
 
 Conclusion
 "
 
 "
+
+
diff --git a/server/nng/NNG/Levels/AdvProposition.lean b/server/nng/NNG/Levels/AdvProposition.lean
index 8d38a47..f9a2e46 100644
--- a/server/nng/NNG/Levels/AdvProposition.lean
+++ b/server/nng/NNG/Levels/AdvProposition.lean
@@ -16,4 +16,8 @@ Title "Advanced Proposition World"
 
 Introduction
 "
+In this world we will learn five key tactics needed to solve all the
+levels of the Natural Number Game, namely `constructor`, `rcases`, `left`, `right`, and `exfalso`.
+These, and `use` (which we'll get to in Inequality World) are all the
+tactics you will need to beat all the levels of the game.
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_1.lean b/server/nng/NNG/Levels/AdvProposition/Level_1.lean
index b3989db..3dd7aa0 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_1.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_1.lean
@@ -10,30 +10,31 @@ open MyNat
 
 Introduction
 "
-In this world we will learn five key tactics needed to solve all the
-levels of the Natural Number Game, namely `split`, `cases`, `left`, `right`, and `exfalso`.
-These, and `use` (which we'll get to in Inequality World) are all the
-tactics you will need to beat all the levels of the game.
-
-## Level 1: the `split` tactic.
-
 The logical symbol `∧` means \"and\". If $P$ and $Q$ are propositions, then
-$P\\land Q$ is the proposition \"$P$ and $Q$\". If your *goal* is `P ∧ Q` then
-you can make progress with the `split` tactic, which turns one goal `⊢ P ∧ Q`
-into two goals, namely `⊢ P` and `⊢ Q`. In the level below, after a `split`,
-you will be able to finish off the goals with the `exact` tactic.
+$P\\land Q$ is the proposition \"$P$ and $Q$\".
 "
 
 Statement
 "If $P$ and $Q$ are true, then $P\\land Q$ is true."
     (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
+  Hint "If your *goal* is `P ∧ Q` then
+  you can make progress with the `constructor` tactic, which turns one goal `P ∧ Q`
+  into two goals, namely `P` and `Q`."
   constructor
+  Hint "Now you have two goals. The first one is `P`, which you can proof now. The
+  second one is `Q` and you see it in the queue \"Other Goals\". You will have to prove it afterwards."
+  Hint (hidden := true) "This first goal can be proved with `exact p`."
   exact p
+  -- Hint "Observe that now the first goal has been proved, so it disappears and you continue
+  -- proving the second goal."
+  -- Hint (hidden := true) "Like the first goal, this is a case for `exact`."
+  -- -- TODO: It looks like these hints get shown above as well, but weirdly the hints from
+  -- -- above to not get shown here.
   exact q
 
 NewTactic constructor
+NewDefinition And
 
 Conclusion
 "
-
 "
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_10.lean b/server/nng/NNG/Levels/AdvProposition/Level_10.lean
index b83c69d..f543a3c 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_10.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_10.lean
@@ -1,11 +1,10 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
 Level 10
-Title "Level 10: the law of the excluded middle."
+Title "The law of the excluded middle."
 
 open MyNat
 
@@ -14,39 +13,8 @@ Introduction
 We proved earlier that `(P → Q) → (¬ Q → ¬ P)`. The converse,
 that `(¬ Q → ¬ P) → (P → Q)` is certainly true, but trying to prove
 it using what we've learnt so far is impossible (because it is not provable in
-constructive logic). For example, after
+constructive logic).
 
-```
-intro h,
-intro p,
-repeat {rw not_iff_imp_false at h},
-```
-
-in the below, you are left with
-```
-P Q : Prop,
-h : (Q → false) → P → false
-p : P
-⊢ Q
-```
-
-The tools you have are not sufficient to continue. But you can just
-prove this, and any other basic lemmas of this form like `¬ ¬ P → P`,
-using the `by_cases` tactic. Instead of starting with all the `intro`s,
-try this instead:
-
-`by_cases p : P; by_cases q : Q,`
-
-**Note the semicolon**! It means \"do the next tactic to all the goals, not just the top one\".
-After it, there are four goals, one for each of the four possibilities PQ=TT, TF, FT, FF.
-You can see that `p` is a proof of `P` in some of the goals, and a proof of `¬ P` in others.
-Similar comments apply to `q`. 
-
-`repeat {cc}` then finishes the job.
-
-This approach assumed that `P ∨ ¬ P` was true; the `by_cases` tactic just does `cases` on
-this result. This is called the law of the excluded middle, and it cannot be proved just
-using tactics such as `intro` and `apply`.
 "
 
 Statement
@@ -54,26 +22,44 @@ Statement
 $$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$ 
 "
     (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by
-  by_cases p : P
-  · by_cases q : Q
-    intro h p' -- cc
-    assumption
-    intro h p'
-    have g : ¬ P := h q
-    contradiction
-  · by_cases q : Q
-    intro h p
-    assumption
-    intro h p
-    contradiction
+  Hint "For example, you could start as always with
+
+  ```
+  intro h p
+  ```
+  "
+  intro h p
+  Hint "From here there is no way to continue with the tactics you've learned so far.
+
+  Instead you can call `by_cases q : Q`. This creates **two goals**, once under the assumption
+  that `Q` is true, once assuming `Q` is false."
+  by_cases q : Q
+  Hint "This first case is trivial."
+  exact q
+  Hint "The second case needs a bit more work, but you can get there with the tactics you've already
+  learned beforehand!"
+  have j := h q
+  exfalso
+  apply j
+  exact p
+
+NewTactic by_cases
 
 Conclusion
 "
+This approach assumed that `P ∨ ¬ P` is true, which is called \"law of excluded middle\".
+It cannot be proven using just tactics like `intro` or `apply`.
+`by_cases p : P` just does `rcases` on this result `P ∨ ¬ P`.
+
+
 OK that's enough logic -- now perhaps it's time to go on to Advanced Addition World!
 Get to it via the main menu.
+"
 
-## Pro tip
+-- TODO: I cannot really import `tauto` because of the notation `ℕ` that's used
+-- for `MyNat`.
+-- ## Pro tip
 
-In fact the tactic `tauto!` just kills this goal (and many other logic goals) immediately.
+-- In fact the tactic `tauto` just kills this goal (and many other logic goals) immediately. You'll be
+-- able to use it from now on.
 
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_2.lean b/server/nng/NNG/Levels/AdvProposition/Level_2.lean
index 0e95056..105b5b3 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_2.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_2.lean
@@ -1,48 +1,49 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
 Level 2
-Title "the `cases` tactic"
+Title "the `rcases` tactic"
 
 open MyNat
 
 Introduction
 "
-If `P ∧ Q` is in the goal, then we can make progress with `split`.
-But what if `P ∧ Q` is a hypothesis? In this case, the `cases` tactic will enable
+If `P ∧ Q` is in the goal, then we can make progress with `constructor`.
+But what if `P ∧ Q` is a hypothesis? In this case, the `rcases` tactic will enable
 us to extract proofs of `P` and `Q` from this hypothesis.
+"
 
-The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,
-symmetry of the \"and\" relation. The obvious first move is
-
-`intro h,`
+Statement -- and_symm
+"If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. "
+    (P Q : Prop) : P ∧ Q → Q ∧ P :=  by
+  Hint "The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,
+  symmetry of the \"and\" relation. The obvious first move is
 
-because the goal is an implication and this tactic is guaranteed
-to make progress. Now `h : P ∧ Q` is a hypothesis, and
+  ```
+  intro h
+  ```
 
-`cases h with p q,`
+  because the goal is an implication and this tactic is guaranteed
+  to make progress."
+  intro h
+  Hint "Now `{h} : P ∧ Q` is a hypothesis, and
 
-will change `h`, the proof of `P ∧ Q`, into two proofs `p : P`
-and `q : Q`. From there, `split` and `exact` will get you home.
-"
+  ```
+  rcases {h} with ⟨p, q⟩
+  ```
 
-set_option tactic.hygienic false
+  will change `{h}`, the proof of `P ∧ Q`, into two proofs `p : P`
+  and `q : Q`.
 
-Statement --and_symm
-"If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. "
-    (P Q : Prop) : P ∧ Q → Q ∧ P :=  by
-  intro h
+  You can write `⟨p, q⟩` with `\\<>` or `\\<` and `\\>`. Note that `rcases h` by itself will just
+  automatically name the new assumptions."
   rcases h with ⟨p, q⟩
+  Hint "Now a combination of `constructor` and `exact` will get you home."
   constructor
   exact q
   exact p
 
 NewTactic rcases
 
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_3.lean b/server/nng/NNG/Levels/AdvProposition/Level_3.lean
index 05955ff..bf03cd1 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_3.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_3.lean
@@ -1,6 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
@@ -11,16 +10,31 @@ open MyNat
 
 Introduction
 "
-
+Here is another exercise to `rcases` and `constructor`.
 "
 
 Statement --and_trans
 "If $P$, $Q$ and $R$ are true/false statements, then $P\\land Q$ and
 $Q\\land R$ together imply $P\\land R$."
     (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by
+  Hint "Here's a trick:
+  
+  Your first steps would probably be
+  ```
+  intro h
+  rcases h with ⟨p, q⟩
+  ```
+  i.e. introducing a new assumption and then immediately take it appart.
+
+  In that case you could do that in a single step:
+
+  ```
+  intro ⟨p, q⟩
+  ```
+  "
   intro hpq
-  intro hqr
   rcases hpq with ⟨p, q⟩
+  intro hqr
   rcases hqr with ⟨q', r⟩
   constructor
   assumption
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_4.lean b/server/nng/NNG/Levels/AdvProposition/Level_4.lean
index efa59ed..6e8d07f 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_4.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_4.lean
@@ -1,6 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
@@ -11,10 +10,9 @@ open MyNat
 
 Introduction
 "
-The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `cases`
-and `split` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need
-to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to. After an initial
-`intro h,` you can type `cases h with hpq hqp` to break `h : P ↔ Q` into its constituent parts.
+The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `rcases`
+and `constructor` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need
+to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to.
 
 "
 
@@ -22,15 +20,26 @@ Statement --iff_trans
 "If $P$, $Q$ and $R$ are true/false statements, then
 $P\\iff Q$ and $Q\\iff R$ together imply $P\\iff R$."
     (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
-  intro hpq
-  intro hqr
-  rcases hpq with ⟨hpq, hqp⟩
-  rcases hqr with ⟨hqr, hrq⟩
+  Hint "Similar to \"and\", you can use `intro` and `rcases` to add the `P ↔ Q` to your
+  assumptions and split it into its constituent parts."
+  Branch
+    intro hpq
+    intro hqr
+    Hint "Now you want to use `rcases {hpq} with ⟨pq, qp⟩`."
+    rcases hpq with ⟨hpq, hqp⟩
+    rcases hqr with ⟨hqr, hrq⟩
+  intro ⟨pq, qp⟩
+  intro ⟨qr, rq⟩
+  Hint "If you want to prove an iff-statement, you can use `constructor` to split it
+  into its two implications."
   constructor
-  exact fun x => hqr (hpq x) -- cc
-  exact fun x => hqp (hrq x) -- cc
+  · intro p
+    apply qr
+    apply pq
+    exact p
+  · intro r
+    apply qp
+    apply rq
+    exact r
 
-Conclusion
-"
-
-"
+NewDefinition Iff
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_5.lean b/server/nng/NNG/Levels/AdvProposition/Level_5.lean
index fe11353..fbedbc5 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_5.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_5.lean
@@ -1,50 +1,65 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
 Level 5
-Title "`iff_trans` easter eggs."
+Title "Easter eggs."
 
 open MyNat
 
 Introduction
 "
-Let's try `iff_trans` again. Try proving it in other ways.
+Let's try this again. Try proving it in other ways. (Note that `rcases` is temporarily disabled.)
 
 ### A trick.
 
-Instead of using `cases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P`
+Instead of using `rcases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P`
 directly with `h.1` and `h.2`. So you can solve this level with
 
 ```
-intros hpq hqr, 
-split,
-intro p,
-apply hqr.1,
-...
+intro hpq hqr
+constructor
+intro p
+apply hqr.1
+…
 ```
 
 ### Another trick
 
-Instead of using `cases` on `h : P ↔ Q`, you can just `rw h`, and this will change all `P`s to `Q`s
+Instead of using `rcases` on `h : P ↔ Q`, you can just `rw [h]`, and this will change all `P`s to `Q`s
 in the goal. You can use this to create a much shorter proof. Note that
-this is an argument for *not* running the `cases` tactic on an iff statement;
+this is an argument for *not* running the `rcases` tactic on an iff statement;
 you cannot rewrite one-way implications, but you can rewrite two-way implications.
 
-### Another trick
 
-`cc` works on this sort of goal too.
 "
+-- TODO
+-- ### Another trick
+-- `cc` works on this sort of goal too.
 
 Statement --iff_trans
 "If $P$, $Q$ and $R$ are true/false statements, then `P ↔ Q` and `Q ↔ R` together imply `P ↔ R`.
 "
     (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
   intro hpq hqr
+  Hint "Make a choice and continue either with `constructor` or `rw`.
+
+  * if you use `constructor`, you will use `{hqr}.1, {hqr}.2, …` later.
+  * if you use `rw`, you can replace all `P`s with `Q`s using `rw [{hpq}]`"
+  Branch
+    rw [hpq]
+    Branch
+      exact hqr
+    rw [hqr]
+    Hint "Now `rfl` can close this goal.
+
+    TODO: Note that the current modification of `rfl` is too weak to prove this. For now, you can
+    use `simp` instead (which calls the \"real\" `rfl` internally)."
+    simp
   constructor
   intro p
+  Hint "Now you can directly `apply {hqr}.1`"
   apply hqr.1
   apply hpq.1
   assumption
@@ -53,6 +68,8 @@ Statement --iff_trans
   apply hqr.2
   assumption
 
+DisabledTactic rcases
+
 Conclusion
 "
 
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_6.lean b/server/nng/NNG/Levels/AdvProposition/Level_6.lean
index 7fda5db..0a7123a 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_6.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_6.lean
@@ -1,8 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
---import Mathlib.Logic.Basic
 
 Game "NNG"
 World "AdvProposition"
@@ -15,25 +12,28 @@ Introduction
 "
 `P ∨ Q` means \"$P$ or $Q$\". So to prove it, you
 need to choose one of `P` or `Q`, and prove that one.
-If `⊢ P ∨ Q` is your goal, then `left` changes this
-goal to `⊢ P`, and `right` changes it to `⊢ Q`.
-Note that you can take a wrong turn here. Let's
-start with trying to prove $Q\\implies (P\\lor Q)$.
-After the `intro`, one of `left` and `right` leads
-to an impossible goal, the other to an easy finish.
+If `P ∨ Q` is your goal, then `left` changes this
+goal to `P`, and `right` changes it to `Q`.
 "
+-- Note that you can take a wrong turn here. Let's
+-- start with trying to prove $Q\\implies (P\\lor Q)$.
+-- After the `intro`, one of `left` and `right` leads
+-- to an impossible goal, the other to an easy finish.
 
 Statement
-"If $P$ and $Q$ are true/false statements, then
-$$Q\\implies(P\\lor Q).$$ "
+"If $P$ and $Q$ are true/false statements, then $Q\\implies(P\\lor Q)$."
     (P Q : Prop) : Q → (P ∨ Q) := by
+  Hint (hidden := true) "Let's start with an initial `intro` again."
   intro q
+  Hint "Now you need to choose if you want to prove the `left` or `right` side of the goal."
+  Branch
+    left
+    -- TODO: This message is also shown on the correct track. Need strict hints.
+    -- Hint "That was an unfortunate choice, you entered a dead end that cannot be proved anymore.
+    -- Hit \"Undo\"!"
   right
-  assumption
+  exact q
 
 NewTactic left right
+NewDefinition Or
 
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_7.lean b/server/nng/NNG/Levels/AdvProposition/Level_7.lean
index 250c2cc..adca207 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_7.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_7.lean
@@ -1,7 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvProposition"
@@ -13,27 +11,45 @@ open MyNat
 Introduction
 "
 Proving that $(P\\lor Q)\\implies(Q\\lor P)$ involves an element of danger.
-`intro h,` is the obvious start. But now,
-even though the goal is an `∨` statement, both `left` and `right` put
-you in a situation with an impossible goal. Fortunately, after `intro h,`
-you can do `cases h with p q`. Then something new happens: because
-there are two ways to prove `P ∨ Q` (namely, proving `P` or proving `Q`),
-the `cases` tactic turns one goal into two, one for each case. You should
-be able to make it home from there. 
 "
 
 Statement --or_symm
 "If $P$ and $Q$ are true/false statements, then
 $$P\\lor Q\\implies Q\\lor P.$$ "
     (P Q : Prop) : P ∨ Q → Q ∨ P := by
+  Hint "`intro h` is the obvious start."
   intro h
+  Branch
+    left
+    Hint "This is a dead end that is not provable anymore. Hit \"undo\"."
+  Branch
+    right
+    Hint "This is a dead end that is not provable anymore. Hit \"undo\"."
+  Hint "But now, even though the goal is an `∨` statement, both `left` and `right` put
+  you in a situation with an impossible goal. Fortunately,
+  you can do `rcases h with p | q`. (that is a normal vertical slash)
+  "
   rcases h with p | q
+  Hint " Something new just happened: because
+  there are two ways to prove the assumption `P ∨ Q` (namely, proving `P` or proving `Q`),
+  the `rcases` tactic turns one goal into two, one for each case.
+
+  So now you proof the goal under the assumption that `P` is true, and waiting under \"Other Goals\"
+  there is the same goal but under the assumption that `Q` is true.
+
+  You should be able to make it home from there. "
   right
   exact p
+  Hint "Note how now you finished the first goal and jumped to the one, where you assume `Q`."
   left
   exact q
 
 Conclusion
 "
+Well done! Note that the syntax for `rcases` is different whether it's an \"or\" or an \"and\".
 
+* `rcases h with ⟨p, q⟩` splits an \"and\" in the assumptions into two parts. You get two assumptions
+but still only one goal.
+* `rcases h with p | q` splits an \"or\" in the assumptions. You get **two goals** which have different
+assumptions, once assumping the lefthand-side of the dismantled \"or\"-assumption, once the righthand-side.
 "
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_8.lean b/server/nng/NNG/Levels/AdvProposition/Level_8.lean
index b44f820..b9e9a83 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_8.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_8.lean
@@ -1,7 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvProposition"
@@ -12,7 +10,7 @@ open MyNat
 
 Introduction
 "
-We know that `x(y+z)=xy+xz` for numbers, and this
+We know that $x(y+z)=xy+xz$ for numbers, and this
 is called distributivity of multiplication over addition.
 The same is true for `∧` and `∨` -- in fact `∧` distributes
 over `∨` and `∨` distributes over `∧`. Let's prove one of these.
@@ -28,34 +26,28 @@ $$P\\land(Q\\lor R)\\iff(P\\land Q)\\lor (P\\land R).$$ "
   rcases hqr with q | r
   left
   constructor
-  assumption
-  assumption
+  exact hp
+  exact q
   right
   constructor
-  assumption
-  assumption
+  exact hp
+  exact r
   intro h
   rcases h with hpq | hpr
   rcases hpq with ⟨p, q⟩
   constructor
-  assumption
+  exact p
   left
-  assumption
+  exact q
   rcases hpr with ⟨hp, hr⟩
   constructor
-  assumption
+  exact hp
   right
-  assumption
+  exact hr
+
 
 Conclusion
 "
-## Pro tip
-
-Did you spot the import? What do you think it does?
-
-If you follow the instructions at
-<a href=\"https://github.com/leanprover-community/mathlib#installation\" target=\"blank\">the mathlib github page</a>
-you will be able to install Lean and mathlib on your own system, and then you can create a new project
-and experiment with such imports yourself.
-
+You already know enough to embark on advanced addition world. But the next two levels comprise
+just a couple more things.
 "
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_9.lean b/server/nng/NNG/Levels/AdvProposition/Level_9.lean
index 6ffa620..d2c2e29 100644
--- a/server/nng/NNG/Levels/AdvProposition/Level_9.lean
+++ b/server/nng/NNG/Levels/AdvProposition/Level_9.lean
@@ -1,9 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import NNG.MyNat.Theorems.Proposition
-
-
 
 Game "NNG"
 World "AdvProposition"
@@ -14,58 +10,43 @@ open MyNat
 
 Introduction
 "
-You already know enough to embark on advanced addition world. But here are just a couple
-more things.
-
-## Level 9: `exfalso` and proof by contradiction. 
-
 It's certainly true that $P\\land(\\lnot P)\\implies Q$ for any propositions $P$
 and $Q$, because the left hand side of the implication is false. But how do
-we prove that `false` implies any proposition $Q$? A cheap way of doing it in
-Lean is using the `exfalso` tactic, which changes any goal at all to `false`. 
+we prove that `False` implies any proposition $Q$? A cheap way of doing it in
+Lean is using the `exfalso` tactic, which changes any goal at all to `False`.
 You might think this is a step backwards, but if you have a hypothesis `h : ¬ P`
-then after `rw not_iff_imp_false at h,` you can `apply h,` to make progress. 
+then after `rw not_iff_imp_false at h,` you can `apply h,` to make progress.
 Try solving this level without using `cc` or `tauto`, but using `exfalso` instead.
-
 "
 
 Statement --contra
 "If $P$ and $Q$ are true/false statements, then
 $$(P\\land(\\lnot P))\\implies Q.$$"
   (P Q : Prop) : (P ∧ ¬ P) → Q := by
+  Hint "Start as usual with `intro ⟨p, np⟩`."
+  Branch
+    exfalso
+    -- TODO: This hint needs to be strict
+    -- Hint "Not so quick! Now you just threw everything away."
   intro h
+  Hint "You should also call `rcases` on your assumption `{h}`."
   rcases h with ⟨p, np ⟩
-  contradiction
-  -- rw [not_iff_imp_false] at np
-  -- exfalso
-  -- apply np
-  -- exact p
-
-NewTactic exfalso contradiction
-
-Conclusion
-"
-## Pro tip.
-
-`¬ P` is actually `P → false` *by definition*. Try
-commenting out `rw not_iff_imp_false at ...` by putting two minus signs `--`
-before the `rw`. Does it still compile?
--/
-
-/- Tactic : exfalso
-
-## Summary
-
-`exfalso` changes your goal to `false`. 
-
-## Details
-
-We know that `false` implies `P` for any proposition `P`, and so if your goal is `P`
-then you should be able to `apply` `false → P` and reduce your goal to `false`. This
-is what the `exfalso` tactic does. The theorem that `false → P` is called `false.elim`
-so one can achieve the same effect with `apply false.elim`. 
-
-This tactic can be used in a proof by contradiction, where the hypotheses are enough
-to deduce a contradiction and the goal happens to be some random statement (possibly
-a false one) which you just want to simplify to `false`.
-"
+  -- TODO: This hint should before the last `exact p` step again.
+  Hint "Now you can call `exfalso` to throw away your goal `Q`. It will be replaced with `False` and
+  which means you will have to prove a contradiction."
+  Branch
+    -- TODO: Would `contradiction` not be more useful to introduce than `exfalso`?
+    contradiction
+  exfalso
+  Hint "Recall that `{np} : ¬ P` means `np : P → False`, which means you can simply `apply {np}` now.
+
+  You can also first call `rw [Not] at {np}` to make this step more explicit."
+  Branch
+    rw [Not] at np
+  apply np
+  exact p
+
+-- TODO: `contradiction`?
+NewTactic exfalso
+-- DisabledTactic cc
+LemmaTab "Prop"
diff --git a/server/nng/NNG/Levels/Function/Level_1.lean b/server/nng/NNG/Levels/Function/Level_1.lean
index cd19937..bfef063 100644
--- a/server/nng/NNG/Levels/Function/Level_1.lean
+++ b/server/nng/NNG/Levels/Function/Level_1.lean
@@ -1,6 +1,6 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
+
+-- TODO: Cannot import level from different world.
 
 Game "NNG"
 World "Function"
@@ -64,7 +64,7 @@ Statement
   "
   exact h p
 
-NewTactic exact
+NewTactic exact simp
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/Function/Level_2.lean b/server/nng/NNG/Levels/Function/Level_2.lean
index 0082d4f..20b4e7a 100644
--- a/server/nng/NNG/Levels/Function/Level_2.lean
+++ b/server/nng/NNG/Levels/Function/Level_2.lean
@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
 import NNG.MyNat.Multiplication
 
 Game "NNG"
@@ -37,14 +36,14 @@ Statement
   `intro n`"
   intro n
   Hint "Our job now is to construct a natural number, which is
-  allowed to depend on $n$. We can do this using `exact` and
+  allowed to depend on ${n}$. We can do this using `exact` and
   writing a formula for the function we want to define. For example
   we imported addition and multiplication at the top of this file,
   so
 
-  `exact 3*n+2,`
+  `exact 3 * {n} + 2`
 
-  will close the goal, ultimately defining the function $f(n)=3n+2$."
+  will close the goal, ultimately defining the function $f({n})=3{n}+2$."
   exact 3 * n + 2
 
 NewTactic intro
diff --git a/server/nng/NNG/Levels/Function/Level_3.lean b/server/nng/NNG/Levels/Function/Level_3.lean
index c2d6e04..d637942 100644
--- a/server/nng/NNG/Levels/Function/Level_3.lean
+++ b/server/nng/NNG/Levels/Function/Level_3.lean
@@ -1,6 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "Function"
@@ -28,8 +26,8 @@ functions looks like this pictorially:
 $$
 \\begin{CD}
   P  @>{h}>> Q       @>{i}>> R \\\\
-  @.         @V{j}VV           \\\\
-  S  @>{k}>> T       @>{l}>> U \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
 \\end{CD}
 $$
 
@@ -42,19 +40,26 @@ Statement
     U := by
   Hint "Indeed, we could solve this level in one move by typing
 
-  `exact l (j (h p))`
+  ```
+  exact l (j (h p))
+  ```
 
   But let us instead stroll more lazily through the level.
   We can start by using the `have` tactic to make an element of $Q$:
 
-  have q := h p"
+  ```
+  have q := h p
+  ```
+  "
   Branch
     exact l (j (h p))
   have q := h p
   Hint "
   and now we note that $j(q)$ is an element of $T$
 
-  `have t : T := j q`
+  ```
+  have t : T := j q
+  ```
 
   (notice how we can explicitly tell Lean
   what set we thought $t$ was in, with that `: T` thing before the `:=`.
@@ -64,7 +69,9 @@ Statement
   Hint "
   Now we could even define $u$ to be $l(t)$:
 
-  `have u : U := l t`
+  ```
+  have u : U := l t
+  ```
   "
   have u : U := l t
   Hint "…and then finish the level with `exact u`."
diff --git a/server/nng/NNG/Levels/Function/Level_4.lean b/server/nng/NNG/Levels/Function/Level_4.lean
index 01fc51f..37015d1 100644
--- a/server/nng/NNG/Levels/Function/Level_4.lean
+++ b/server/nng/NNG/Levels/Function/Level_4.lean
@@ -1,6 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "Function"
@@ -15,8 +13,8 @@ Introduction
 $$
 \\begin{CD}
   P  @>{h}>> Q       @>{i}>> R \\\\
-  @.         @V{j}VV           \\\\
-  S  @>{k}>> T       @>{l}>> U \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
 \\end{CD}
 $$
 
@@ -41,10 +39,13 @@ by
   a function, so it would suffice to construct an element of $T$. Tell
   Lean this by starting the proof below with
 
-  `apply l`"
+  ```
+  apply l
+  ```
+  "
   apply l
   Hint "Notice that our assumptions don't change but *the goal changes*
-  from `Goal: U` to `Goal: T`.
+  from `U` to `T`.
 
   Keep `apply`ing functions until your goal is `P`, and try not
   to get lost!"
@@ -61,8 +62,3 @@ by
 
 NewTactic apply
 DisabledTactic «have»
-
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/Function/Level_5.lean b/server/nng/NNG/Levels/Function/Level_5.lean
index 3ca4ce7..8ef30f7 100644
--- a/server/nng/NNG/Levels/Function/Level_5.lean
+++ b/server/nng/NNG/Levels/Function/Level_5.lean
@@ -1,6 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "Function"
@@ -31,7 +29,9 @@ Statement
   `intro` tactic from level 2, Lean's version of \"let $p\\in P$ be arbitrary.\"
   So let's start with
 
-  `intro p`"
+  ```
+  intro p
+  ```"
   intro p
   Hint "
   We now have an arbitrary element $p\\in P$ and we are supposed to be constructing
@@ -39,11 +39,15 @@ Statement
   sends everything to $p$?
   This will work. So let $q\\in Q$ be arbitrary:
 
-  `intro q`"
+  ```
+  intro q
+  ```"
   intro q
   Hint "and then let's output `p`.
 
-  `exact p`"
+  ```
+  exact p
+  ```"
   exact p
 
 Conclusion
diff --git a/server/nng/NNG/Levels/Function/Level_6.lean b/server/nng/NNG/Levels/Function/Level_6.lean
index 5e97dd9..f0848f8 100644
--- a/server/nng/NNG/Levels/Function/Level_6.lean
+++ b/server/nng/NNG/Levels/Function/Level_6.lean
@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
@@ -14,21 +13,13 @@ You can solve this level completely just using `intro`, `apply` and `exact`,
 but if you want to argue forwards instead of backwards then don't forget
 that you can do things like
 
-`have j : Q → R := f p`
+```
+have j : Q → R := f p
+```
 
 if `f : P → (Q → R)` and `p : P`. Remember the trick with the colon in `have`:
 we could just write `have j := f p,` but this way we can be sure that `j` is
 what we actually expect it to be.
-
-I recommend that you start with `intro f` rather than `intro p`
-because even though the goal starts `P → ...`, the brackets mean that
-the goal is not a function from `P` to anything, it's a function from
-`P → (Q → R)` to something. In fact you can save time by starting
-with `intros f h p`, which introduces three variables at once, although you'd
-better then look at your tactic state to check that you called all those new
-terms sensible things.
-
-After all the intros, you find that your your goal is `Goal: R`…
 "
 
 Statement
@@ -36,6 +27,13 @@ Statement
 make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,\\operatorname{Hom}(Q,R)),
 \\operatorname{Hom}(\\operatorname{Hom}(P,Q),\\operatorname{Hom}(P,R)))$."
     (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) := by
+  Hint "I recommend that you start with `intro f` rather than `intro p`
+  because even though the goal starts `P → _`, the brackets mean that
+  the goal is not a function from `P` to anything, it's a function from
+  `P → (Q → R)` to something. In fact you can save time by starting
+  with `intro f h p`, which introduces three variables at once, although you'd
+  better then look at your tactic state to check that you called all those new
+  terms sensible things. "
   intro f
   intro h
   intro p
@@ -47,14 +45,17 @@ make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,\\operatorname{Hom
 
   What happens if you just try `apply {f}`?
   "
-  Branch
-    apply f
-    Hint "Can you figure out what just happened? This is a little
-    `apply` easter egg. Why is it mathematically valid?"
-    Hint (hidden := true) "Note that there are two goals now, first you need to
-    provide an element in ${P}$ which you did not provide before."
+  -- TODO: This hint needs strictness to make sense
+  -- Branch
+  --   apply f
+  --   Hint "Can you figure out what just happened? This is a little
+  --   `apply` easter egg. Why is it mathematically valid?"
+  --   Hint (hidden := true) "Note that there are two goals now, first you need to
+  --   provide an element in ${P}$ which you did not provide before."
   have j : Q → R := f p
   apply j
+  Hint (hidden := true) "Is there something you could apply? something of the form
+  `_ → Q`?"
   apply h
   exact p
 
diff --git a/server/nng/NNG/Levels/Function/Level_7.lean b/server/nng/NNG/Levels/Function/Level_7.lean
index 2c51127..de8f1f4 100644
--- a/server/nng/NNG/Levels/Function/Level_7.lean
+++ b/server/nng/NNG/Levels/Function/Level_7.lean
@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
diff --git a/server/nng/NNG/Levels/Function/Level_8.lean b/server/nng/NNG/Levels/Function/Level_8.lean
index 02f4837..0ee4864 100644
--- a/server/nng/NNG/Levels/Function/Level_8.lean
+++ b/server/nng/NNG/Levels/Function/Level_8.lean
@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
@@ -13,31 +12,6 @@ Introduction
 Level 8 is the same as level 7, except we have replaced the
 set $F$ with the empty set $\\emptyset$. The same proof will work (after all, our
 previous proof worked for all sets, and the empty set is a set).
-But note that if you start with `intro f, intro h, intro p,`
-(which can incidentally be shortened to `intros f h p`),
-then the local context looks like this:
-
-```
-P Q : Type,
-f : P → Q,
-h : Q → empty,
-p : P
-⊢ empty
-```
-
-and your job is to construct an element of the empty set!
-This on the face of it seems hard, but what is going on is that
-our hypotheses (we have an element of $P$, and functions $P\\to Q$
-and $Q\\to\\emptyset$) are themselves contradictory, so
-I guess we are doing some kind of proof by contradiction at this point? However,
-if your next line is `apply h` then all of a sudden the goal
-seems like it might be possible again. If this is confusing, note
-that the proof of the previous world worked for all sets $F$, so in particular
-it worked for the empty set, you just probably weren't really thinking about
-this case explicitly beforehand. [Technical note to constructivists: I know
-that we are not doing a proof by contradiction. But how else do you explain
-to a classical mathematician that their goal is to prove something false
-and this is OK because their hypotheses don't add up?]
 "
 
 Statement
@@ -45,6 +19,7 @@ Statement
 make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
 \\operatorname{Hom}(\\operatorname{Hom}(Q,\\emptyset),\\operatorname{Hom}(P,\\emptyset)))$."
     (P Q : Type) : (P → Q) → ((Q → Empty) → (P → Empty)) := by
+  Hint (hidden := true) "Maybe start again with `intro`."
   intros f h p
   Hint "
   Note that now your job is to construct an element of the empty set!
@@ -52,9 +27,11 @@ make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
   our hypotheses (we have an element of $P$, and functions $P\\to Q$
   and $Q\\to\\emptyset$) are themselves contradictory, so
   I guess we are doing some kind of proof by contradiction at this point? However,
-  if your next line is 
+  if your next line is
 
-  `apply {h}`
+  ```
+  apply {h}
+  ```
 
   then all of a sudden the goal
   seems like it might be possible again. If this is confusing, note
@@ -69,7 +46,4 @@ make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
   apply f
   exact p
 
-Conclusion
-"
-
-"
+Conclusion ""
diff --git a/server/nng/NNG/Levels/Function/Level_9.lean b/server/nng/NNG/Levels/Function/Level_9.lean
index 18eed2f..7545c65 100644
--- a/server/nng/NNG/Levels/Function/Level_9.lean
+++ b/server/nng/NNG/Levels/Function/Level_9.lean
@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
@@ -24,7 +23,9 @@ Statement
     (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
     (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
     (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by
+  Hint "In any case, start with `intro a`!"
   intro a
+  Hint "Now use a combination of `have` and `apply`."
   apply f15
   apply f11
   apply f9
diff --git a/server/nng/NNG/Levels/Inequality.lean b/server/nng/NNG/Levels/Inequality.lean
index 4ffeb5c..8f5ce6f 100644
--- a/server/nng/NNG/Levels/Inequality.lean
+++ b/server/nng/NNG/Levels/Inequality.lean
@@ -1,20 +1,20 @@
 import NNG.Levels.Inequality.Level_1
-import NNG.Levels.Inequality.Level_2
-import NNG.Levels.Inequality.Level_3
-import NNG.Levels.Inequality.Level_4
-import NNG.Levels.Inequality.Level_5
-import NNG.Levels.Inequality.Level_6
-import NNG.Levels.Inequality.Level_7
-import NNG.Levels.Inequality.Level_8
-import NNG.Levels.Inequality.Level_9
-import NNG.Levels.Inequality.Level_10
-import NNG.Levels.Inequality.Level_11
-import NNG.Levels.Inequality.Level_12
-import NNG.Levels.Inequality.Level_13
-import NNG.Levels.Inequality.Level_14
-import NNG.Levels.Inequality.Level_15
-import NNG.Levels.Inequality.Level_16
-import NNG.Levels.Inequality.Level_17
+-- import NNG.Levels.Inequality.Level_2
+-- import NNG.Levels.Inequality.Level_3
+-- import NNG.Levels.Inequality.Level_4
+-- import NNG.Levels.Inequality.Level_5
+-- import NNG.Levels.Inequality.Level_6
+-- import NNG.Levels.Inequality.Level_7
+-- import NNG.Levels.Inequality.Level_8
+-- import NNG.Levels.Inequality.Level_9
+-- import NNG.Levels.Inequality.Level_10
+-- import NNG.Levels.Inequality.Level_11
+-- import NNG.Levels.Inequality.Level_12
+-- import NNG.Levels.Inequality.Level_13
+-- import NNG.Levels.Inequality.Level_14
+-- import NNG.Levels.Inequality.Level_15
+-- import NNG.Levels.Inequality.Level_16
+-- import NNG.Levels.Inequality.Level_17
 
 Game "NNG"
 World "Inequality"
diff --git a/server/nng/NNG/Levels/Multiplication.lean b/server/nng/NNG/Levels/Multiplication.lean
index 4ff6d8c..023734f 100644
--- a/server/nng/NNG/Levels/Multiplication.lean
+++ b/server/nng/NNG/Levels/Multiplication.lean
@@ -15,4 +15,23 @@ Title "Multiplication World"
 
 Introduction
 "
+In this world you start with the definition of multiplication on `ℕ`. It is
+defined by recursion, just like addition was. So you get two new axioms:
+
+  * `mul_zero (a : ℕ) : a * 0 = 0`
+  * `mul_succ (a b : ℕ) : a * succ b = a * b + a`
+
+In words, we define multiplication by \"induction on the second variable\",
+with `a * 0` defined to be `0` and, if we know `a * b`, then `a` times
+the number after `b` is defined to be `a * b + a`.
+
+You can keep all the theorems you proved about addition, but
+for multiplication, those two results above are what you've got right now.
+
+So what's going on in multiplication world? Like addition, we need to go
+for the proofs that multiplication
+is commutative and associative, but as well as that we will
+need to prove facts about the relationship between multiplication
+and addition, for example `a * (b + c) = a * b + a * c`, so now
+there is a lot more to do. Good luck!
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Multiplication/Level_1.lean b/server/nng/NNG/Levels/Multiplication/Level_1.lean
index c2ad14a..8b4184b 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_1.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_1.lean
@@ -1,24 +1,35 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.Multiplication
+import NNG.Levels.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 1
-Title ""
+Title "zero_mul"
 
 open MyNat
 
 Introduction
 "
+As a side note, the lemmas about addition are still available in your inventory
+in the lemma tab \"Add\" while the new lemmas about multiplication appear in the
+tab \"Mul\".
 
+We are given `mul_zero`, and the first thing to prove is `zero_mul`.
+Like `zero_add`, we of course prove it by induction.
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.zero_mul
+"For all natural numbers $m$, we have $ 0 \\cdot m = 0$."
+    (m : ℕ) : 0 * m = 0 := by
+  induction m
+  rw [mul_zero]
+  rfl
+  rw [mul_succ]
+  rw [n_ih]
+  rw [add_zero]
+  rfl
 
-Conclusion
-"
-
-"
+NewTactic simp
+NewLemma MyNat.mul_zero MyNat.mul_succ
+NewDefinition Mul
+LemmaTab "Mul"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_2.lean b/server/nng/NNG/Levels/Multiplication/Level_2.lean
index 502e4f6..3068a30 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_2.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_2.lean
@@ -1,24 +1,31 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_1
 
 Game "NNG"
 World "Multiplication"
 Level 2
-Title ""
+Title "mul_one"
 
 open MyNat
 
 Introduction
 "
+In this level we'll need to use
 
-"
-
-Statement
-""
-    : true := by
-  trivial
+* `one_eq_succ_zero : 1 = succ 0 `
 
-Conclusion
+which was mentioned back in Addition World  (see \"Add\" tab in your inventory) and
+which will be a useful thing to rewrite right now, as we
+begin to prove a couple of lemmas about how `1` behaves
+with respect to multiplication.
 "
 
-"
+Statement MyNat.mul_one
+"For any natural number $m$, we have $ m \\cdot 1 = m$."
+    (m : ℕ) : m * 1 = m := by
+rw [one_eq_succ_zero]
+rw [mul_succ]
+rw [mul_zero]
+rw [zero_add]
+rfl
+
+LemmaTab "Mul"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_3.lean b/server/nng/NNG/Levels/Multiplication/Level_3.lean
index ca45877..8501ef9 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_3.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_3.lean
@@ -1,24 +1,38 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_2
 
 Game "NNG"
 World "Multiplication"
 Level 3
-Title ""
+Title "one_mul"
 
 open MyNat
 
 Introduction
 "
+These proofs from addition world might be useful here:
 
+* `one_eq_succ_zero : 1 = succ 0`
+* `succ_eq_add_one a : succ a = a + 1`
+
+We just proved `mul_one`, now let's prove `one_mul`.
+Then we will have proved, in fancy terms,
+that 1 is a \"left and right identity\"
+for multiplication (just like we showed that
+0 is a left and right identity for addition
+with `add_zero` and `zero_add`).
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.one_mul
+"For any natural number $m$, we have $ 1 \\cdot m = m$."
+    (m : ℕ): 1 * m = m := by
+  induction m with d hd
+  · rw [mul_zero]
+    rfl
+  · rw [mul_succ]
+    rw [hd]
+    rw [succ_eq_add_one]
+    rfl
 
-Conclusion
-"
+LemmaTab "Mul"
 
-"
+Conclusion ""
diff --git a/server/nng/NNG/Levels/Multiplication/Level_4.lean b/server/nng/NNG/Levels/Multiplication/Level_4.lean
index e692704..37cb86c 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_4.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_4.lean
@@ -1,24 +1,44 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_3
 
 Game "NNG"
 World "Multiplication"
 Level 4
-Title ""
+Title "mul_add"
 
 open MyNat
 
 Introduction
 "
+Where are we going? Well we want to prove `mul_comm`
+and `mul_assoc`, i.e. that `a * b = b * a` and
+`(a * b) * c = a * (b * c)`. But we *also* want to
+establish the way multiplication interacts with addition,
+i.e. we want to prove that we can \"expand out the brackets\"
+and show `a * (b + c) = (a * b) + (a * c)`.
+The technical term for this is \"left distributivity of
+multiplication over addition\" (there is also right distributivity,
+which we'll get to later).
 
+Note the name of this proof -- `mul_add`. And note the left
+hand side -- `a * (b + c)`, a multiplication and then an addition.
+I think `mul_add` is much easier to remember than \"`left_distrib`\",
+an alternative name for the proof of this lemma.
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.mul_add
+"Multiplication is distributive over addition.
+In other words, for all natural numbers $a$, $b$ and $t$, we have
+$t(a + b) = ta + tb$."
+    (t a b : ℕ) : t * (a + b) = t * a + t * b := by
+  induction b with d hd
+  · rw [add_zero, mul_zero, add_zero]
+    rfl
+  · rw [add_succ]
+    rw [mul_succ]
+    rw [hd]
+    rw [mul_succ]
+    rw [add_assoc]
+    rfl
 
-Conclusion
-"
+LemmaTab "Mul"
 
-"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_5.lean b/server/nng/NNG/Levels/Multiplication/Level_5.lean
index 01e06dc..518218a 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_5.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_5.lean
@@ -1,22 +1,41 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_4
 
 Game "NNG"
 World "Multiplication"
 Level 5
-Title ""
+Title "mul_assoc"
 
 open MyNat
 
 Introduction
 "
+We now have enough to prove that multiplication is associative.
+
+## Random tactic hint
+
+You can do `repeat rw [mul_succ]` to repeat a tactic as often as possible.
 
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.mul_assoc
+"Multiplication is associative.
+In other words, for all natural numbers $a$, $b$ and $c$, we have
+$(ab)c = a(bc)$."
+    (a b c : ℕ) : (a * b) * c = a * (b * c)  := by
+  induction c with d hd
+  · repeat rw [mul_zero]
+    rfl
+  · rw [mul_succ]
+    rw [mul_succ]
+    rw [hd]
+    rw [mul_add]
+    rfl
+
+NewTactic «repeat»
+LemmaTab "Mul"
+
+-- TODO: old version introduced `rwa` here, but it would need to be modified
+-- as our `rw` does not call `rfl` at the end.
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/Multiplication/Level_6.lean b/server/nng/NNG/Levels/Multiplication/Level_6.lean
index 4eeba03..900fedb 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_6.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_6.lean
@@ -1,22 +1,50 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_5
 
 Game "NNG"
 World "Multiplication"
 Level 6
-Title ""
+Title "succ_mul"
 
 open MyNat
 
 Introduction
 "
+We now begin our journey to `mul_comm`, the proof that `a * b = b * a`.
+We'll get there in level 8. Until we're there, it is frustrating
+but true that we cannot assume commutativity. We have `mul_succ`
+but we're going to need `succ_mul` (guess what it says -- maybe you
+are getting the hang of Lean's naming conventions).
 
+Remember also that we have tools like
+
+* `add_right_comm a b c : a + b + c = a + c + b`
+
+These things are the tools we need to slowly build up the results
+which we will need to do mathematics \"normally\".
+We also now have access to Lean's `simp` tactic,
+which will solve any goal which just needs a bunch
+of rewrites of `add_assoc` and `add_comm`. Use if
+you're getting lazy!
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.succ_mul
+"For all natural numbers $a$ and $b$, we have
+$\\operatorname{succ}(a) \\cdot b = ab + b$."
+    (a b : ℕ) : succ a * b = a * b + b := by
+  induction b with d hd
+  · rw [mul_zero]
+    rw [mul_zero]
+    rw [add_zero]
+    rfl
+  · rw [mul_succ]
+    rw [mul_succ]
+    rw [hd]
+    rw [add_succ]
+    rw [add_succ]
+    rw [add_right_comm]
+    rfl
+
+LemmaTab "Mul"
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/Multiplication/Level_7.lean b/server/nng/NNG/Levels/Multiplication/Level_7.lean
index 746f3c9..9a242d6 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_7.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_7.lean
@@ -1,22 +1,44 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_6
 
 Game "NNG"
 World "Multiplication"
 Level 7
-Title ""
+Title "add_mul"
 
 open MyNat
 
 Introduction
 "
-
+We proved `mul_add` already, but because we don't have commutativity yet
+we also need to prove `add_mul`. We have a bunch of tools now, so this won't
+be too hard. You know what -- you can do this one by induction on any of
+the variables. Try them all! Which works best? If you can't face
+doing all the commutativity and associativity, remember the high-powered
+`simp` tactic mentioned at the bottom of Addition World level 6,
+which will solve any puzzle which needs only commutativity
+and associativity. If your goal looks like `a + (b + c) = c + b + a` or something,
+don't mess around doing it explicitly with `add_comm` and `add_assoc`,
+just try `simp`.
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.add_mul
+"Addition is distributive over multiplication.
+In other words, for all natural numbers $a$, $b$ and $t$, we have
+$(a + b) \times t = at + bt$."
+    (a b t : ℕ) : (a + b) * t = a * t + b * t := by
+  induction b with d hd
+  · rw [zero_mul]
+    rw [add_zero]
+    rw [add_zero]
+    rfl
+  · rw [add_succ]
+    rw [succ_mul]
+    rw [hd]
+    rw [succ_mul]
+    rw [add_assoc]
+    rfl
+
+LemmaTab "Mul"
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/Multiplication/Level_8.lean b/server/nng/NNG/Levels/Multiplication/Level_8.lean
index 369d554..08dcdfd 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_8.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_8.lean
@@ -1,24 +1,46 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_7
 
 Game "NNG"
 World "Multiplication"
 Level 8
-Title ""
+Title "mul_comm"
 
 open MyNat
 
 Introduction
 "
-
+Finally, the boss level of multiplication world. But (assuming you
+didn't cheat) you are well-prepared for it -- you have `zero_mul`
+and `mul_zero`, as well as `succ_mul` and `mul_succ`. After this
+level you can of course throw away one of each pair if you like,
+but I would recommend you hold on to them, sometimes it's convenient
+to have exactly the right tools to do a job.
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.mul_comm
+"Multiplication is commutative."
+    (a b : ℕ) : a * b = b * a := by
+  induction b with d hd
+  · rw [zero_mul]
+    rw [mul_zero]
+    rfl
+  · rw [succ_mul]
+    rw [← hd]
+    rw [mul_succ]
+    rfl
+
+LemmaTab "Mul"
 
 Conclusion
 "
+You've now proved that the natural numbers are a commutative semiring!
+That's the last collectible in Multiplication World.
 
+* `CommSemiring ℕ`
+
+But don't leave multiplication just yet -- prove `mul_left_comm`, the last
+level of the world, and then we can beef up the power of `simp`.
 "
+
+-- TODO: collectible
+-- instance mynat.comm_semiring : comm_semiring mynat := by structure_helper
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Multiplication/Level_9.lean b/server/nng/NNG/Levels/Multiplication/Level_9.lean
index 20fb8eb..e1fc48a 100644
--- a/server/nng/NNG/Levels/Multiplication/Level_9.lean
+++ b/server/nng/NNG/Levels/Multiplication/Level_9.lean
@@ -1,24 +1,57 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Multiplication.Level_8
 
 Game "NNG"
 World "Multiplication"
 Level 9
-Title ""
+Title "mul_left_comm"
 
 open MyNat
 
 Introduction
 "
+You are equipped with
+
+* `mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c)`
+* `mul_comm (a b : ℕ) : a * b = b * a`
+
+Re-read the docs for `rw` so you know all the tricks.
+You can see them in your inventory on the right.
 
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.mul_left_comm
+"For all natural numbers $a$ $b$ and $c$, we have $a(bc)=b(ac)$."
+    (a b c : ℕ) : a * (b * c) = b * (a * c) := by
+  rw [← mul_assoc]
+  rw [mul_comm a]
+  rw [mul_assoc]
+  rfl
+
+LemmaTab "Mul"
+
+-- TODO: make simp work:
+-- attribute [simp] mul_assoc mul_comm mul_left_comm
 
 Conclusion
 "
+And now I whisper a magic incantation
+
+```
+attribute [simp] mul_assoc mul_comm mul_left_comm
+```
+
+and all of a sudden Lean can automatically do levels which are
+very boring for a human, for example
+
+```
+example (a b c d e : ℕ) :
+    (((a * b) * c) * d) * e = (c * ((b * e) * a)) * d := by
+  simp
+```
 
+If you feel like attempting Advanced Multiplication world
+you'll have to do Function World and the Proposition Worlds first.
+These worlds assume a certain amount of mathematical maturity
+(perhaps 1st year undergraduate level).
+Your other possibility is Power World, with the \"final boss\".
 "
diff --git a/server/nng/NNG/Levels/Power.lean b/server/nng/NNG/Levels/Power.lean
index 1199c78..fb37bdb 100644
--- a/server/nng/NNG/Levels/Power.lean
+++ b/server/nng/NNG/Levels/Power.lean
@@ -1,10 +1,3 @@
-import NNG.Levels.Power.Level_1
-import NNG.Levels.Power.Level_2
-import NNG.Levels.Power.Level_3
-import NNG.Levels.Power.Level_4
-import NNG.Levels.Power.Level_5
-import NNG.Levels.Power.Level_6
-import NNG.Levels.Power.Level_7
 import NNG.Levels.Power.Level_8
 
 Game "NNG"
@@ -18,17 +11,15 @@ This import gives you the power to make powers of your
 natural numbers. It is defined by recursion, just like addition and multiplication.
 Here are the two new axioms:
 
-  * `pow_zero (a : mynat) : a ^ 0 = 1`
-  * `pow_succ (a b : mynat) : a ^ succ(b) = a ^ b * a`
+  * `pow_zero (a : ℕ) : a ^ 0 = 1`
+  * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`
 
 The power function has various relations to addition and multiplication.
 If you have gone through levels 1--6 of addition world and levels 1--9 of
 multiplication world, you should have no trouble with this world:
-The usual tactics `induction`, `rw` and `refl` should see you through.
-You might want to fiddle with the
-drop-down menus on the left so you can see which theorems of Power World
-you have proved at any given time. Addition and multiplication -- we
-have a solid API for them now, i.e. if you need something about addition
+The usual tactics `induction`, `rw` and `rfl` should see you through.
+You should probably look at your inverntory again: addition and multiplication
+have a solid API by now, i.e. if you need something about addition
 or multiplication, it's probably already in the library we have built.
 Collectibles are indication that we are proving the right things.
 
diff --git a/server/nng/NNG/Levels/Power/Level_1.lean b/server/nng/NNG/Levels/Power/Level_1.lean
index b75c7d5..b6e0688 100644
--- a/server/nng/NNG/Levels/Power/Level_1.lean
+++ b/server/nng/NNG/Levels/Power/Level_1.lean
@@ -1,5 +1,5 @@
-import NNG.Metadata
---import NNG.MyNat.Power
+import NNG.Levels.Multiplication
+import NNG.MyNat.Power
 
 Game "NNG"
 World "Power"
@@ -8,18 +8,12 @@ Title "zero_pow_zero"
 
 open MyNat
 
-Introduction
-"
-
-"
-
-Statement
+Statement MyNat.zero_pow_zero
 "$0 ^ 0 = 1$"
-    : (0 : ℕ) ^ 0 = (1 : ℕ) := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by
-  trivial
-
-Conclusion
-"
-
-"
+    : (0 : ℕ) ^ 0  = 1 := by
+  rw [pow_zero]
+  rfl
 
+NewLemma MyNat.pow_zero MyNat.pow_succ
+NewDefinition Pow
+LemmaTab "Pow"
diff --git a/server/nng/NNG/Levels/Power/Level_2.lean b/server/nng/NNG/Levels/Power/Level_2.lean
index fe6698a..cf4b1ba 100644
--- a/server/nng/NNG/Levels/Power/Level_2.lean
+++ b/server/nng/NNG/Levels/Power/Level_2.lean
@@ -1,24 +1,17 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_1
 
 Game "NNG"
 World "Power"
 Level 2
-Title ""
+Title "zero_pow_succ"
 
 open MyNat
 
-Introduction
-"
+Statement MyNat.zero_pow_succ
+"For all naturals $m$, $0 ^{\\operatorname{succ} (m)} = 0$."
+    (m : ℕ) : (0 : ℕ) ^ (succ m) = 0 := by
+  rw [pow_succ]
+  rw [mul_zero]
+  rfl
 
-"
-
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
-
-"
+LemmaTab "Pow"
diff --git a/server/nng/NNG/Levels/Power/Level_3.lean b/server/nng/NNG/Levels/Power/Level_3.lean
index 7cf3d38..ee44e4c 100644
--- a/server/nng/NNG/Levels/Power/Level_3.lean
+++ b/server/nng/NNG/Levels/Power/Level_3.lean
@@ -1,24 +1,19 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_2
 
 Game "NNG"
 World "Power"
 Level 3
-Title ""
+Title "pow_one"
 
 open MyNat
 
-Introduction
-"
+Statement MyNat.pow_one
+"For all naturals $a$, $a ^ 1 = a$."
+    (a : ℕ) : a ^ 1 = a  := by
+  rw [one_eq_succ_zero]
+  rw [pow_succ]
+  rw [pow_zero]
+  rw [one_mul]
+  rfl
 
-"
-
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
-
-"
+LemmaTab "Pow"
diff --git a/server/nng/NNG/Levels/Power/Level_4.lean b/server/nng/NNG/Levels/Power/Level_4.lean
index 812dca0..0bde842 100644
--- a/server/nng/NNG/Levels/Power/Level_4.lean
+++ b/server/nng/NNG/Levels/Power/Level_4.lean
@@ -1,25 +1,22 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_3
+
 
 Game "NNG"
 World "Power"
 Level 4
-Title ""
+Title "one_pow"
 
 open MyNat
 
-Introduction
-"
-
-"
-
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
+Statement MyNat.one_pow
+"For all naturals $m$, $1 ^ m = 1$."
+    (m : ℕ) : (1 : ℕ) ^ m = 1 := by
+  induction m with t ht
+  · rw [pow_zero]
+    rfl
+  · rw [pow_succ]
+    rw [ht]
+    rw [mul_one]
+    rfl
 
-"
-  
\ No newline at end of file
+LemmaTab "Pow"
diff --git a/server/nng/NNG/Levels/Power/Level_5.lean b/server/nng/NNG/Levels/Power/Level_5.lean
index e9f6dc0..750e4d2 100644
--- a/server/nng/NNG/Levels/Power/Level_5.lean
+++ b/server/nng/NNG/Levels/Power/Level_5.lean
@@ -1,24 +1,20 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_4
+
 
 Game "NNG"
 World "Power"
 Level 5
-Title ""
+Title "pow_add"
 
 open MyNat
 
-Introduction
-"
-
-"
-
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
+Statement MyNat.pow_add
+"For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m  a ^ n$."
+    (a m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n := by
+  induction n with t ht
+  · rw [add_zero, pow_zero, mul_one]
+    rfl
+  · rw [add_succ, pow_succ, pow_succ, ht, mul_assoc]
+    rfl
 
-"
+LemmaTab "Pow"
diff --git a/server/nng/NNG/Levels/Power/Level_6.lean b/server/nng/NNG/Levels/Power/Level_6.lean
index eaf97a0..fa5d3d8 100644
--- a/server/nng/NNG/Levels/Power/Level_6.lean
+++ b/server/nng/NNG/Levels/Power/Level_6.lean
@@ -1,24 +1,30 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_5
 
 Game "NNG"
 World "Power"
 Level 6
-Title ""
+Title "mul_pow"
 
 open MyNat
 
 Introduction
 "
-
+You might find the tip at the end of level 9 of Multiplication World
+useful in this one. You can go to the main menu and pop back into
+Multiplication World and take a look -- you won't lose any of your
+proofs.
 "
 
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
+Statement MyNat.mul_pow
+"For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$."
+    (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by
+  induction n with t Ht
+  · rw [pow_zero, pow_zero, pow_zero, mul_one]
+    rfl
+  · rw [pow_succ, pow_succ, pow_succ, Ht]
+    -- simp
+    repeat rw [mul_assoc]
+    rw [mul_comm a (_ * b), mul_assoc, mul_comm b a]
+    rfl
 
-"
+LemmaTab "Pow"
diff --git a/server/nng/NNG/Levels/Power/Level_7.lean b/server/nng/NNG/Levels/Power/Level_7.lean
index f5b1949..1a14059 100644
--- a/server/nng/NNG/Levels/Power/Level_7.lean
+++ b/server/nng/NNG/Levels/Power/Level_7.lean
@@ -1,24 +1,35 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_6
 
 Game "NNG"
 World "Power"
 Level 7
-Title ""
+Title "pow_pow"
 
 open MyNat
 
 Introduction
 "
-
+Boss level! What will the collectible be?
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.pow_pow
+"For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$."
+    (a m n : ℕ) : (a ^ m) ^ n = a ^ (m * n) := by
+  induction n with t Ht
+  · rw [mul_zero, pow_zero, pow_zero]
+    rfl
+  · rw [pow_succ, Ht, mul_succ, pow_add]
+    rfl
+
+LemmaTab "Pow"
 
 Conclusion
 "
+Apparently Lean can't find a collectible, even though you feel like you
+just finished power world so you must have proved *something*. What should the
+collectible for this level be called?
 
+But what is this? It's one of those twists where there's another
+boss after the boss you thought was the final boss! Go to the next
+level!
 "
diff --git a/server/nng/NNG/Levels/Power/Level_8.lean b/server/nng/NNG/Levels/Power/Level_8.lean
index 0240bfd..2bc3d20 100644
--- a/server/nng/NNG/Levels/Power/Level_8.lean
+++ b/server/nng/NNG/Levels/Power/Level_8.lean
@@ -1,22 +1,49 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.Levels.Power.Level_7
+-- import Mathlib.Tactic.Ring
 
 Game "NNG"
 World "Power"
 Level 8
-Title ""
+Title "add_squared"
 
 open MyNat
 
 Introduction
 "
+[final boss music] 
 
+You see something written on the stone dungeon wall:
+```
+by
+  rw [two_eq_succ_one]
+  rw [one_eq_succ_zero]
+  repeat rw [pow_succ]
+  …
+```
+
+and you can't make out the last two lines because there's a kind
+of thing in the way that will magically disappear
+but only when you've beaten the boss.
 "
 
-Statement
-""
-    : true := by
-  trivial
+Statement MyNat.add_squared
+"For all naturals $a$ and $b$, we have
+$$(a+b)^2=a^2+b^2+2ab.$$"
+  (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
+  rw [two_eq_succ_one]
+  rw [one_eq_succ_zero]
+  repeat rw [pow_succ]
+  repeat rw [pow_zero]
+  --ring
+  repeat rw [one_mul]
+  rw [add_mul, mul_add, mul_add, mul_comm b a]
+  rw [succ_mul, succ_mul, zero_mul, zero_add, add_mul]
+  repeat rw [add_assoc]
+  rw [add_comm _ (b * b), ← add_assoc _ (b*b), add_comm _ (b*b), add_assoc]
+  rfl
+
+NewLemma MyNat.two_eq_succ_one
+LemmaTab "Pow"
 
 Conclusion
 "
diff --git a/server/nng/NNG/Levels/Proposition.lean b/server/nng/NNG/Levels/Proposition.lean
index 9dc768a..5a05778 100644
--- a/server/nng/NNG/Levels/Proposition.lean
+++ b/server/nng/NNG/Levels/Proposition.lean
@@ -6,7 +6,7 @@ import NNG.Levels.Proposition.Level_5
 import NNG.Levels.Proposition.Level_6
 import NNG.Levels.Proposition.Level_7
 import NNG.Levels.Proposition.Level_8
--- import NNG.Levels.Proposition.Level_9 -- `cc` is not ported
+import NNG.Levels.Proposition.Level_9 -- `cc` is not ported
 
 
 Game "NNG"
@@ -15,4 +15,34 @@ Title "Proposition World"
 
 Introduction
 "
+A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`.
+Just like we can have concrete sets in Lean like `mynat`, and abstract
+sets called things like `X`, we can also have concrete propositions like
+`2 + 2 = 5` and abstract propositions called things like `P`.
+
+Mathematicians are very good at conflating a theorem with its proof.
+They might say \"now use theorem 12 and we're done\". What they really
+mean is \"now use the proof of theorem 12...\" (i.e. the fact that we proved
+it already). Particularly problematic is the fact that mathematicians
+use the word Proposition to mean \"a relatively straightforward statement
+which is true\" and computer scientists use it to mean \"a statement of
+arbitrary complexity, which might be true or false\". Computer scientists
+are far more careful about distinguishing between a proposition and a proof.
+For example: `x + 0 = x` is a proposition, and `add_zero x`
+is its proof. The convention we'll use is capital letters for propositions
+and small letters for proofs.
+
+In this world you will see the local context in the following kind of state:
+
+```
+Objects:
+  P : Prop
+Assumptions:
+  p : P
+```
+
+Here `P` is the true/false statement (the statement of proposition), and `p` is its proof.
+It's like `P` being the set and `p` being the element. In fact computer scientists
+sometimes think about the following analogy: propositions are like sets,
+and their proofs are like their elements.
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Proposition/Level_1.lean b/server/nng/NNG/Levels/Proposition/Level_1.lean
index 09dfcc1..b5eb3fc 100644
--- a/server/nng/NNG/Levels/Proposition/Level_1.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_1.lean
@@ -10,35 +10,7 @@ open MyNat
 
 Introduction
 "
-A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`.
-Just like we can have concrete sets in Lean like `ℕ`, and abstract
-sets called things like `X`, we can also have concrete propositions like
-`2 + 2 = 5` and abstract propositions called things like `P`. 
-
-Mathematicians are very good at conflating a theorem with its proof.
-They might say \"now use theorem 12 and we're done\". What they really
-mean is \"now use the proof of theorem 12...\" (i.e. the fact that we proved
-it already). Particularly problematic is the fact that mathematicians
-use the word Proposition to mean \"a relatively straightforward statement
-which is true\" and computer scientists use it to mean \"a statement of
-arbitrary complexity, which might be true or false\". Computer scientists
-are far more careful about distinguishing between a proposition and a proof.
-For example: `x + 0 = x` is a proposition, and `add_zero x`
-is its proof. The convention we'll use is capital letters for propositions
-and small letters for proofs. 
-"
-
-Statement
-"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true."
-    (P Q : Prop) (p : P) (h : P → Q) : Q := by
-Hint
-"
-Here `P` is the true/false statement (the statement of proposition), and `p` is its proof.
-It's like `P` being the set and `p` being the element. In fact computer scientists
-sometimes think about the following analogy: propositions are like sets,
-and their proofs are like their elements. 
-
-## What's going on in this world? 
+What's going on in this world?
 
 We're going to learn about manipulating propositions and proofs.
 Fortunately, we don't need to learn a bunch of new tactics -- the
@@ -46,9 +18,13 @@ ones we just learnt (`exact`, `intro`, `have`, `apply`) will be perfect.
 
 The levels in proposition world are \"back to normal\", we're proving
 theorems, not constructing elements of sets. Or are we?
+"
 
-If you delete the sorry below then your local context will look like this:
-
+Statement
+"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true."
+    (P Q : Prop) (p : P) (h : P → Q) : Q := by
+Hint
+"
 In this situation, we have true/false statements $P$ and $Q$,
 a proof $p$ of $P$, and $h$ is the hypothesis that $P\\implies Q$.
 Our goal is to construct a proof of $Q$. It's clear what to do
@@ -59,20 +35,17 @@ Adopting a point of view wholly unfamiliar to many mathematicians,
 Lean interprets the hypothesis $h$ as a function from proofs
 of $P$ to proofs of $Q$, so the rather surprising approach
 
-`exact h p`
+```
+exact h p
+```
 
 works to close the goal.
 
 Note that `exact h P` (with a capital P) won't work;
 this is a common error I see from beginners. \"We're trying to solve `P`
 so it's exactly `P`\". The goal states the *theorem*, your job is to
-construct the *proof*. $P$ is not a proof of $P$, it's $p$ that is a proof of $P$. 
+construct the *proof*. $P$ is not a proof of $P$, it's $p$ that is a proof of $P$.
 
 In Lean, Propositions, like sets, are types, and proofs, like elements of sets, are terms.
 "
 exact h p
-
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/Proposition/Level_2.lean b/server/nng/NNG/Levels/Proposition/Level_2.lean
index bfca35b..7bf92e7 100644
--- a/server/nng/NNG/Levels/Proposition/Level_2.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_2.lean
@@ -45,14 +45,16 @@ Statement
   To solve this goal, you have to come up with a function from
   `P` (thought of as the set of proofs of $P$!) to itself. Start with
 
-  `intro p`
+  ```
+  intro p
+  ```
   "
   intro p
   Hint "
-  Our job now is to construct a proof of $P$. But $p$ is a proof of $P$.
+  Our job now is to construct a proof of $P$. But ${p}$ is a proof of $P$.
   So
 
-  `exact p`
+  `exact {p}`
 
   will close the goal. Note that `exact P` will not work -- don't
   confuse a true/false statement (which could be false!) with a proof.
@@ -60,8 +62,3 @@ Statement
   and small letters for proofs.
   "
   exact p
-
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/Proposition/Level_3.lean b/server/nng/NNG/Levels/Proposition/Level_3.lean
index 29008b0..33071af 100644
--- a/server/nng/NNG/Levels/Proposition/Level_3.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_3.lean
@@ -25,42 +25,55 @@ of $U$; during the proof we will construct proofs of
 of some of the other propositions involved. The diagram of
 propositions and implications looks like this pictorially:
 
-![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg)
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
+\\end{CD}
+$$
 
 and so it's clear how to deduce $U$ from $P$.
-Indeed, we could solve this level in one move by typing
 
-`exact l(j(h(p))),`
-
-But let us instead stroll more lazily through the level.
-We can start by using the `have` tactic to make a proof of $Q$:
-
-`have q := h(p),`
-
-and then we note that $j(q)$ is a proof of $T$:
-
-`have t : T := j(q),`
-
-(note how we explicitly told Lean what proposition we thought $t$ was
-a proof of, with that `: T` thing before the `:=`) 
-and we could even define $u$ to be $l(t)$:
-
-`have u : U := l(t),`
-
-and then finish the level with
-
-`exact u,`
-
-. 
 "
 
 Statement
 "In the maze of logical implications above, if $P$ is true then so is $U$."
     (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R)
     (j : Q → T) (k : S → T) (l : T → U) : U := by
+  Hint "Indeed, we could solve this level in one move by typing
+
+  ```
+  exact l (j (h p))
+  ```
+
+  But let us instead stroll more lazily through the level.
+  We can start by using the `have` tactic to make a proof of $Q$:
+
+  ```
+  have q := h p
+  ```
+  "
   have q := h p
+  Hint "
+  and then we note that $j {q}$ is a proof of $T$:
+
+  ```
+  have t : T := j {q}
+  ```
+  "
   have t := j q
+  Hint "
+  (note how we explicitly told Lean what proposition we thought ${t}$ was
+  a proof of, with that `: T` thing before the `:=`)
+  and we could even define $u$ to be $l {t}$:
+
+  ```
+  have u : U := l {t}
+  ```
+  "
   have u := l t
+  Hint " and now finish the level with `exact {u}`."
   exact u
 
 DisabledTactic apply
@@ -73,17 +86,20 @@ and explore your proof, right?) and note that the local context at that point
 is in something like the following mess:
 
 ```
-P Q R S T U : Prop,
-p : P,
-h : P → Q,
-i : Q → R,
-j : Q → T,
-k : S → T,
-l : T → U,
-q : Q,
-t : T,
-u : U
-⊢ U
+Objects:
+  P Q R S T U : Prop
+Assumptions:
+  p : P
+  h : P → Q
+  i : Q → R
+  j : Q → T
+  k : S → T
+  l : T → U
+  q : Q
+  t : T
+  u : U
+Goal :
+  U
 ```
 
 It was already bad enough to start with, and we added three more
diff --git a/server/nng/NNG/Levels/Proposition/Level_4.lean b/server/nng/NNG/Levels/Proposition/Level_4.lean
index 45f0197..d5b2469 100644
--- a/server/nng/NNG/Levels/Proposition/Level_4.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_4.lean
@@ -12,42 +12,48 @@ Introduction
 "
 Let's do the same level again:
 
-![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg)
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
+\\end{CD}
+$$
 
 We are given a proof $p$ of $P$ and our goal is to find a proof of $U$, or
 in other words to find a path through the maze that links $P$ to $U$.
 In level 3 we solved this by using `have`s to move forward, from $P$
 to $Q$ to $T$ to $U$. Using the `apply` tactic we can instead construct
 the path backwards, moving from $U$ to $T$ to $Q$ to $P$.
-
-Our goal is to prove $U$. But $l:T\\implies U$ is
-an implication which we are assuming, so it would suffice to prove $T$.
-Tell Lean this by starting the proof below with
-
-`apply l,`
-
-and notice that our assumptions don't change but *the goal changes*
-from `⊢ U` to `⊢ T`. 
-
-Keep `apply`ing implications until your goal is `P`, and try not
-to get lost! Now solve this goal
-with `exact p`. Note: you will need to learn the difference between
-`exact p` (which works) and `exact P` (which doesn't, because $P$ is
-not a proof of $P$).
 "
 
 Statement
 "We can solve a maze."
     (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R)
     (j : Q → T) (k : S → T) (l : T → U) : U := by
+  Hint "Our goal is to prove $U$. But $l:T\\implies U$ is
+  an implication which we are assuming, so it would suffice to prove $T$.
+  Tell Lean this by starting the proof below with
+
+  ```
   apply l
+  ```
+  "
+  apply l
+  Hint "Notice that our assumptions don't change but *the goal changes*
+  from `U` to `T`.
+
+  Keep `apply`ing implications until your goal is `P`, and try not
+  to get lost!"
+  Branch
+    apply k
+    Hint "Looks like you got lost. \"Undo\" the last step."
   apply j
   apply h
+  Hint "Now solve this goal
+  with `exact p`. Note: you will need to learn the difference between
+  `exact p` (which works) and `exact P` (which doesn't, because $P$ is
+  not a proof of $P$)."
   exact p
 
-DisabledTactic «have» 
-
-Conclusion
-"
-
-"
+DisabledTactic «have»
diff --git a/server/nng/NNG/Levels/Proposition/Level_5.lean b/server/nng/NNG/Levels/Proposition/Level_5.lean
index e2418e0..0ca2569 100644
--- a/server/nng/NNG/Levels/Proposition/Level_5.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_5.lean
@@ -13,47 +13,44 @@ Introduction
 In this level, our goal is to construct an implication, like in level 2.
 
 ```
-⊢ P → (Q → P)
+P → (Q → P)
 ```
 
 So $P$ and $Q$ are propositions, and our goal is to prove
 that $P\\implies(Q\\implies P)$.
 We don't know whether $P$, $Q$ are true or false, so initially
-this seems like a bit of a tall order. But let's give it a go. Delete
-the `sorry` and let's think about how to proceed.
-
-Our goal is `P → X` for some true/false statement $X$, and if our
-goal is to construct an implication then we almost always want to use the
-`intro` tactic from level 2, Lean's version of \"assume $P$\", or more precisely
-\"assume $p$ is a proof of $P$\". So let's start with
-
-`intro p,`
-
-and we then find ourselves in this state:
-
-```
-P Q : Prop,
-p : P
-⊢ Q → P
-```
-
-We now have a proof $p$ of $P$ and we are supposed to be constructing
-a proof of $Q\\implies P$. So let's assume that $Q$ is true and try
-and prove that $P$ is true. We assume $Q$ like this:
-
-`intro q,`
-
-and now we have to prove $P$, but have a proof handy:
-
-`exact p,`
+this seems like a bit of a tall order. But let's give it a go.
 "
 
 Statement
 "For any propositions $P$ and $Q$, we always have
 $P\\implies(Q\\implies P)$."
     (P Q : Prop) : P → (Q → P) := by
+  Hint "Our goal is `P → X` for some true/false statement $X$, and if our
+  goal is to construct an implication then we almost always want to use the
+  `intro` tactic from level 2, Lean's version of \"assume $P$\", or more precisely
+  \"assume $p$ is a proof of $P$\". So let's start with
+
+  ```
+  intro p
+  ```
+  "
   intro p
+  Hint "We now have a proof $p$ of $P$ and we are supposed to be constructing
+  a proof of $Q\\implies P$. So let's assume that $Q$ is true and try
+  and prove that $P$ is true. We assume $Q$ like this:
+
+  ```
+  intro q
+  ```
+  "
   intro q
+  Hint "Now we have to prove $P$, but have a proof handy:
+
+  ```
+  exact {p}
+  ```
+  "
   exact p
 
 Conclusion
@@ -75,6 +72,6 @@ propositions, they would rather work with concrete ones such as Fermat's Last Th
 so they do not have a convention for where the brackets go. It's important to
 remember Lean's convention though, or else you will get confused. If your goal
 is `P → Q → R` then you need to know whether `intro h` will create `h : P` or `h : P → Q`. 
-Make sure you understand which one. 
+Make sure you understand which one.
 
 "
diff --git a/server/nng/NNG/Levels/Proposition/Level_6.lean b/server/nng/NNG/Levels/Proposition/Level_6.lean
index c824303..e90f73c 100644
--- a/server/nng/NNG/Levels/Proposition/Level_6.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_6.lean
@@ -13,35 +13,43 @@ Introduction
 You can solve this level completely just using `intro`, `apply` and `exact`,
 but if you want to argue forwards instead of backwards then don't forget
 that you can do things like `have j : Q → R := f p` if `f : P → (Q → R)`
-and `p : P`. I recommend that you start with `intro f` rather than `intro p`
-because even though the goal starts `P → ...`, the brackets mean that
-the goal is not the statement that `P` implies anything, it's the statement that
-$P\\implies (Q\\implies R)$ implies something. In fact I'd recommend that you started
-with `intros f h p`, which introduces three variables at once.
-You then find that your your goal is `⊢ R`. If you try `have j : Q → R := f p`
-now then you can `apply j`. Alternatively you can `apply (f p)` directly.
-What happens if you just try `apply f`? Can you figure out what just happened? This is a little
-`apply` easter egg. Why is it mathematically valid?
--/
-
-/- Lemma : no-side-bar
-If $P$ and $Q$ and $R$ are true/false statements, then
-$$(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).$$
-
+and `p : P`.
 "
 
 Statement
-""
+"If $P$ and $Q$ and $R$ are true/false statements, then
+$$
+(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).
+$$"
     (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) := by
+  Hint "I recommend that you start with `intro f` rather than `intro p`
+  because even though the goal starts `P → ...`, the brackets mean that
+  the goal is not the statement that `P` implies anything, it's the statement that
+  $P\\implies (Q\\implies R)$ implies something. In fact you can save time by starting
+  with `intro f h p`, which introduces three variables at once, although you'd
+  better then look at your tactic state to check that you called all those new
+  terms sensible things. "
   intro f
   intro h
   intro p
+  Hint "
+  If you try `have j : {Q} → {R} := {f} {p}`
+  now then you can `apply j`.
+
+  Alternatively you can `apply ({f} {p})` directly.
+
+  What happens if you just try `apply {f}`?
+  "
+  -- TODO: This hint needs strictness to make sense
+  -- Branch
+  --   apply f
+  --   Hint "Can you figure out what just happened? This is a little
+  --   `apply` easter egg. Why is it mathematically valid?"
+  --   Hint (hidden := true) "Note that there are two goals now, first you need to
+  --   provide an element in ${P}$ which you did not provide before."
   have j : Q → R := f p
   apply j
+  Hint (hidden := true) "Is there something you could apply? something of the form
+  `_ → Q`?"
   apply h
   exact p
-
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/Proposition/Level_7.lean b/server/nng/NNG/Levels/Proposition/Level_7.lean
index 8637a15..4805f06 100644
--- a/server/nng/NNG/Levels/Proposition/Level_7.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_7.lean
@@ -8,30 +8,20 @@ Title "(P → Q) → ((Q → R) → (P → R))"
 
 open MyNat
 
-Introduction
-"
-If you start with `intro hpq` and then `intro hqr`
-the dust will clear a bit and the level will look like this:
-```
-P Q R : Prop,
-hpq : P → Q,
-hqr : Q → R
-⊢ P → R
-```
-So this level is really about showing transitivity of $\\implies$,
-if you like that sort of language.
-"
+Introduction ""
 
 Statement
 "From $P\\implies Q$ and $Q\\implies R$ we can deduce $P\\implies R$."
     (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) := by
-  intro hpq hqr
+  Hint (hidden := true)"If you start with `intro hpq` and then `intro hqr`
+  the dust will clear a bit."
+  intro hpq
+  Hint (hidden := true) "Now try `intro hqr`."
+  intro hqr
+  Hint "So this level is really about showing transitivity of $\\implies$,
+  if you like that sort of language."
   intro p
   apply hqr
   apply hpq
   exact p
 
-Conclusion
-"
-
-"
diff --git a/server/nng/NNG/Levels/Proposition/Level_8.lean b/server/nng/NNG/Levels/Proposition/Level_8.lean
index 8235534..29c7fb8 100644
--- a/server/nng/NNG/Levels/Proposition/Level_8.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_8.lean
@@ -1,7 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import NNG.MyNat.Theorems.Proposition
-
 
 Game "NNG"
 World "Proposition"
@@ -12,39 +10,63 @@ open MyNat
 
 Introduction
 "
-There is a false proposition `false`, with no proof. It is
-easy to check that $\\lnot Q$ is equivalent to $Q\\implies {\tt false}$,
-and in the natural number game we call this
-
-`not_iff_imp_false (P : Prop) : ¬ P ↔ (P → false)`
-
-So you can start the proof of the contrapositive below with
+There is a false proposition `False`, with no proof. It is
+easy to check that $\\lnot Q$ is equivalent to $Q\\implies {\\tt False}$.
 
-`repeat {rw not_iff_imp_false},`
-
-to get rid of the two occurences of `¬`, and I'm sure you can
-take it from there (note that we just added `not_iff_imp_false` to the
-theorem statements in the menu on the left). At some point your goal might be to prove `false`.
-At that point I guess you must be proving something by contradiction.
-Or are you? 
+In lean, this is true *by definition*, so you can view and treat `¬A` as an implication
+`A → False`.
 "
 
 Statement
 "If $P$ and $Q$ are propositions, and $P\\implies Q$, then
 $\\lnot Q\\implies \\lnot P$. "
     (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) := by
-  rw [not_iff_imp_false]
-  rw [not_iff_imp_false]
+  Hint "However, if you would like to *see* `¬ Q` as `Q → False` because it makes you help
+  understanding, you can call
+
+  ```
+  repeat rw [Not]
+  ```
+
+  to get rid of the two occurences of `¬`. (`Not` is the name of `¬`)
+
+  I'm sure you can take it from there."
+  Branch
+    repeat rw [Not]
+    Hint "Note that this did not actually change anything internally. Once you're done, you
+    could delete the `rw [Not]` and your proof would still work."
+    intro f
+    intro h
+    intro p
+    -- TODO: It is somewhat cumbersome to have these hints several times.
+    -- defeq option in hints would help
+    Hint "Now you have to prove `False`. I guess that means you must be proving something by
+    contradiction. Or are you?"
+    Hint (hidden := true) "If you `apply {h}` the `False` magically dissappears again. Can you make
+    mathematical sense of these two steps?"
+    apply h
+    apply f
+    exact p
   intro f
   intro h
+  Hint "Note that `¬ P` should be read as `P → False`, so you can directly call `intro p` on it, even
+  though it might not look like an implication."
   intro p
+  Hint "Now you have to prove `False`. I guess that means you must be proving something by
+  contradiction. Or are you?"
+  Hint "If you're stuck, you could do `rw [Not] at {h}`. Maybe that helps."
+  Branch
+    rw [Not] at h
+    Hint "If you `apply {h}` the `False` magically dissappears again. Can you make
+    mathematical sense of these two steps?"
   apply h
   apply f
   exact p
 
-NewLemma not_iff_imp_false
+-- TODO: It this the right place? `repeat` is also introduced in `Multiplication World` so it might be
+-- nice to introduce it earlier on the `Function world`-branch.
+NewTactic «repeat»
+NewDefinition False Not
 
-Conclusion
-"
-
-"
+Conclusion "If you used `rw [Not]` or `rw [Not] at h` anywhere, go through your proof in
+the \"Editor Mode\" and delete them all. Observe that your proof still works."
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Proposition/Level_9.lean b/server/nng/NNG/Levels/Proposition/Level_9.lean
index 64d4e96..4e95741 100644
--- a/server/nng/NNG/Levels/Proposition/Level_9.lean
+++ b/server/nng/NNG/Levels/Proposition/Level_9.lean
@@ -1,6 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import NNG.MyNat.Theorems.Proposition
 
 Game "NNG"
 World "Proposition"
@@ -11,16 +10,16 @@ open MyNat
 
 Introduction
 "
-Now move onto advanced proposition world, where you will see
-how to prove goals such as `P ∧ Q` ($P$ and $Q$), `P ∨ Q` ($P$ or $Q$),
-`P ↔ Q` ($P\\iff Q$).
-You will need to learn five more tactics: `split`, `cases`,
-`left`, `right`, and `exfalso`,
-but they are all straightforward, and furthermore they are
-essentially the last tactics you
-need to learn in order to complete all the levels of the Natural Number Game,
-including all the 17 levels of Inequality World. 
+In Lean3 there was a tactic `cc` which stands for \"congruence closure\"
+which could solve all these mazes automatically. Currently this tactic has
+not been ported to Lean4, but it will eventually be available!
+
+For now, you can try to do this final level manually to apprechiate the use of such
+automatisation ;)
 "
+-- TODO:
+-- "Lean's "congruence closure" tactic `cc` is good at mazes. You might want to try it now.
+-- Perhaps I should have mentioned it earlier."
 
 Statement
 "There is a way through the following maze."
@@ -28,10 +27,30 @@ Statement
     (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
     (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
     (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by
-  -- cc -- TODO: `cc` is not ported yet.
-  sorry
+  Hint (hidden := true) "You should, once again, start with `intro a`."
+  intro a
+  Hint "Use a mixture of `apply` and `have` calls to find your way through the maze."
+  apply f15
+  apply f11
+  apply f9
+  apply f8
+  apply f5
+  apply f2
+  apply f1
+  exact a
+
+-- TODO: Once `cc` is implemented,
+-- NewTactic cc
 
 Conclusion
 "
-
+Now move onto advanced proposition world, where you will see
+how to prove goals such as `P ∧ Q` ($P$ and $Q$), `P ∨ Q` ($P$ or $Q$),
+`P ↔ Q` ($P\\iff Q$).
+You will need to learn five more tactics: `constructor`, `rcases`,
+`left`, `right`, and `exfalso`,
+but they are all straightforward, and furthermore they are
+essentially the last tactics you
+need to learn in order to complete all the levels of the Natural Number Game,
+including all the 17 levels of Inequality World.
 "
diff --git a/server/nng/NNG/Levels/Tutorial/Level_1.lean b/server/nng/NNG/Levels/Tutorial/Level_1.lean
index 7c0749e..ca79fcc 100644
--- a/server/nng/NNG/Levels/Tutorial/Level_1.lean
+++ b/server/nng/NNG/Levels/Tutorial/Level_1.lean
@@ -28,7 +28,7 @@ Statement
   Hint "In order to use the tactic `rfl` you can enter it above and hit \"Execute\"."
   rfl
 
-NewTactic rfl
+NewTactic rfl simp -- TODO
 NewDefinition MyNat
 
 Conclusion
diff --git a/server/nng/NNG/Levels/Tutorial/Level_3.lean b/server/nng/NNG/Levels/Tutorial/Level_3.lean
index 77abf68..d3f426c 100644
--- a/server/nng/NNG/Levels/Tutorial/Level_3.lean
+++ b/server/nng/NNG/Levels/Tutorial/Level_3.lean
@@ -56,9 +56,11 @@ Statement
   writing a small `←` (`\\l`, i.e. backslash + small letter L + space)
   before `h` like this: `rw [← h]`."
   Branch
-    rewrite [← h]
+    simp? -- TODO: `simp` should not make progress.
+  Branch
+    rw [← h]
     Hint (hidden := true) "Now both sides are identical…"
-  rewrite [h]
+  rw [h]
   Hint (hidden := true) "Now both sides are identical…"
   rfl
 
diff --git a/server/nng/NNG/Levels/Tutorial/Level_4.lean b/server/nng/NNG/Levels/Tutorial/Level_4.lean
index b0e55bf..3723f8a 100644
--- a/server/nng/NNG/Levels/Tutorial/Level_4.lean
+++ b/server/nng/NNG/Levels/Tutorial/Level_4.lean
@@ -50,6 +50,8 @@ Statement
   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
diff --git a/server/nng/NNG/Metadata.lean b/server/nng/NNG/Metadata.lean
index faf9e98..a7a450a 100644
--- a/server/nng/NNG/Metadata.lean
+++ b/server/nng/NNG/Metadata.lean
@@ -1,5 +1,18 @@
 import GameServer.Commands
-import NNG.Doc.Tactics
-import NNG.Doc.Lemmas
+
+import NNG.MyNat.Definition
+
 import NNG.Doc.Definitions
-import NNG.Modifications.Tactics
+import NNG.Doc.Lemmas
+import NNG.Doc.Tactics
+
+import NNG.Tactic.Induction
+import NNG.Tactic.Rfl
+import NNG.Tactic.Rw
+import Std.Tactic.RCases
+import Mathlib.Tactic.Have
+import Mathlib.Tactic.LeftRight
+
+-- TODO: Why does this not work here??
+-- We do not want `simp` to be able to do anything unless we unlock it manually.
+attribute [-simp] MyNat.succ.injEq
\ No newline at end of file
diff --git a/server/nng/NNG/MyNat/AddCommMonoid.lean b/server/nng/NNG/MyNat/AddCommMonoid.lean
new file mode 100644
index 0000000..27c36c3
--- /dev/null
+++ b/server/nng/NNG/MyNat/AddCommMonoid.lean
@@ -0,0 +1,15 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+namespace MyNat
+
+-- TODO: Do we need these instances?
+
+-- instance addSemigroup : AddSemigroup ℕ :=
+-- {
+--   zero := 0
+
+-- }
+-- MyNat.addMonoid        -- (after level 2)
+-- MyNat.addCommSemigroup -- (after level 4)
+-- MyNat.addCommMonoid    -- (after level 4)
\ No newline at end of file
diff --git a/server/nng/NNG/MyNat/Addition.lean b/server/nng/NNG/MyNat/Addition.lean
index 46be116..a16c40b 100644
--- a/server/nng/NNG/MyNat/Addition.lean
+++ b/server/nng/NNG/MyNat/Addition.lean
@@ -14,13 +14,9 @@ instance : Add MyNat where
 /--
 This theorem proves that if you add zero to a MyNat you get back the same number.
 -/
-
 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.
 -/
 theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
-
--- TODO: testing. Remove me
-axiom zero_add (n : ℕ) : 0 + n = n
diff --git a/server/nng/NNG/MyNat/AdvAddition.lean b/server/nng/NNG/MyNat/AdvAddition.lean
index 898705c..661425b 100644
--- a/server/nng/NNG/MyNat/AdvAddition.lean
+++ b/server/nng/NNG/MyNat/AdvAddition.lean
@@ -1,13 +1,14 @@
-import NNG.Levels.Addition.Level_6
+import NNG.MyNat.Addition
 
 namespace MyNat
-open MyNat
 
-axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
+attribute [-simp] MyNat.succ.injEq
+example (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
+  simp
+  sorry
 
-axiom zero_ne_succ (a : ℕ) : zero ≠ succ a
+axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
 
-axiom add_right_cancel (a t b : ℕ) : a + t = b + t → a = b
+axiom zero_ne_succ (a : ℕ) : 0 ≠ succ a
 
-axiom add_left_cancel (a b c : ℕ) : a + b = a + c → b = c
 
diff --git a/server/nng/NNG/MyNat/Definition.lean b/server/nng/NNG/MyNat/Definition.lean
index f567b27..bd68ddf 100644
--- a/server/nng/NNG/MyNat/Definition.lean
+++ b/server/nng/NNG/MyNat/Definition.lean
@@ -1,11 +1,8 @@
---import Mathlib.Tactic.Basic
---import Mathlib.Tactic.Cases 
-
 /-- Our copy of the natural numbers called `MyNat`. -/
 inductive MyNat where
 | zero : MyNat
 | succ : MyNat → MyNat
-deriving BEq, DecidableEq, Inhabited
+-- deriving BEq, DecidableEq, Inhabited
 
 @[inherit_doc]
 notation "ℕ" => MyNat
@@ -35,3 +32,7 @@ instance : ToString MyNat where
 theorem zero_eq_0 : MyNat.zero = 0 := rfl
 
 def one : MyNat := MyNat.succ 0
+
+-- TODO: Why does this not work here??
+-- We do not want `simp` to be able to do anything unless we unlock it manually.
+attribute [-simp] MyNat.succ.injEq
diff --git a/server/nng/NNG/MyNat/Multiplication.lean b/server/nng/NNG/MyNat/Multiplication.lean
index d92ac54..4444615 100644
--- a/server/nng/NNG/MyNat/Multiplication.lean
+++ b/server/nng/NNG/MyNat/Multiplication.lean
@@ -14,6 +14,3 @@ instance : Mul MyNat where
 axiom mul_zero (a : MyNat) : a * 0 = 0
 
 axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a
-
--- ToDO
-axiom succ_ne_zero (a : ℕ) : succ a ≠ 0
diff --git a/server/nng/NNG/MyNat/Power.lean b/server/nng/NNG/MyNat/Power.lean
index 7ade13f..6585962 100644
--- a/server/nng/NNG/MyNat/Power.lean
+++ b/server/nng/NNG/MyNat/Power.lean
@@ -1,4 +1,5 @@
 import NNG.MyNat.Multiplication
+
 namespace MyNat
 open MyNat
 
@@ -11,11 +12,15 @@ instance : Pow ℕ ℕ where
 
 -- notation a ^ b := pow a b
 
-example : (1 : ℕ) ^ (1 : ℕ) = 1 := rfl
+-- Important note: This here is the real `rfl`, not the weaker game version
+
+example : (1 : ℕ) ^ 1 = 1 := by rfl
+
+theorem pow_zero (m : ℕ) : m ^ 0 = 1 := by rfl
 
-lemma pow_zero (m : ℕ) : m ^ (0 : ℕ) = 1 := rfl
+theorem pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := by rfl
 
-lemma pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := rfl
+def two_eq_succ_one : (2 : ℕ) = succ 1 := by rfl
 
 end MyNat
 
diff --git a/server/nng/NNG/MyNat/Theorems/Proposition.lean b/server/nng/NNG/MyNat/Theorems/Proposition.lean
deleted file mode 100644
index 9901853..0000000
--- a/server/nng/NNG/MyNat/Theorems/Proposition.lean
+++ /dev/null
@@ -1 +0,0 @@
-theorem not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := by simp only
diff --git a/server/nng/NNG/Modifications/Tactics.lean b/server/nng/NNG/Tactic/Induction.lean
similarity index 67%
rename from server/nng/NNG/Modifications/Tactics.lean
rename to server/nng/NNG/Tactic/Induction.lean
index 72be45b..2f244c2 100644
--- a/server/nng/NNG/Modifications/Tactics.lean
+++ b/server/nng/NNG/Tactic/Induction.lean
@@ -1,33 +1,9 @@
 import Mathlib.Lean.Expr.Basic
-import NNG.MyNat.Addition
 import Lean.Elab.Tactic.Basic
-
-/-!
-# Modified `rw`
-
-Modify `rw` to work like `rewrite`.
-
-This is mainly a copy of the implementation of `rewrite` in Lean core.
--/
+import NNG.MyNat.Definition
 
 namespace MyNat
 
-open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic
-
-/--
-Modified `rw` tactic. For this game, `rw` works exactly like `rewrite`.
--/
-syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic
-
-@[tactic MyNat.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
-  let cfg ← elabRewriteConfig stx[1]
-  let loc   := expandOptLocation stx[3]
-  withRWRulesSeq stx[0] stx[2] fun symm term => do
-    withLocation loc
-      (rewriteLocalDecl term symm · cfg)
-      (rewriteTarget term symm cfg)
-      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
-
 /-!
 # Modified `induction` tactic
 
@@ -103,29 +79,4 @@ elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+)
 end Lean.Parser.Tactic
 
 
-/-! # `rfl` tactic
-
-Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
--/
-
-namespace MyNat
-
-open Lean Meta Elab Tactic
-
--- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
-
-/-- Modified `rfl` tactic.
 
-`rfl` closes goals of the form `A = A`.
-
-Note that teh version for this game is somewhat weaker than the real one. -/
-syntax (name := rfl) "rfl" : tactic
-
-@[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
-  liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure []
-
--- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
---   liftMetaTactic fun mvarId => do mvarId.refl; pure []
--- (with_reducible rfl)
-
-end MyNat
diff --git a/server/nng/NNG/Tactic/Rfl.lean b/server/nng/NNG/Tactic/Rfl.lean
new file mode 100644
index 0000000..b119a3f
--- /dev/null
+++ b/server/nng/NNG/Tactic/Rfl.lean
@@ -0,0 +1,31 @@
+import Mathlib.Lean.Expr.Basic
+import Lean.Elab.Tactic.Basic
+
+/-! # `rfl` tactic
+
+Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
+-/
+
+namespace MyNat
+
+open Lean Meta Elab Tactic
+
+-- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
+
+/-- Modified `rfl` tactic.
+
+`rfl` closes goals of the form `A = A`.
+
+Note that teh version for this game is somewhat weaker than the real one. -/
+syntax (name := rfl) "rfl" : tactic
+
+@[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
+  liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure []
+-- TODO: `rfl` should be able to prove `R ↔ R`!
+
+
+-- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
+--   liftMetaTactic fun mvarId => do mvarId.refl; pure []
+-- (with_reducible rfl)
+
+end MyNat
diff --git a/server/nng/NNG/Tactic/Rw.lean b/server/nng/NNG/Tactic/Rw.lean
new file mode 100644
index 0000000..29f83ff
--- /dev/null
+++ b/server/nng/NNG/Tactic/Rw.lean
@@ -0,0 +1,28 @@
+import Mathlib.Lean.Expr.Basic
+import Lean.Elab.Tactic.Basic
+
+/-!
+# Modified `rw`
+
+Modify `rw` to work like `rewrite`.
+
+This is mainly a copy of the implementation of `rewrite` in Lean core.
+-/
+
+namespace MyNat
+
+open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic
+
+/--
+Modified `rw` tactic. For this game, `rw` works exactly like `rewrite`.
+-/
+syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic
+
+@[tactic MyNat.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
+  let cfg ← elabRewriteConfig stx[1]
+  let loc   := expandOptLocation stx[3]
+  withRWRulesSeq stx[0] stx[2] fun symm term => do
+    withLocation loc
+      (rewriteLocalDecl term symm · cfg)
+      (rewriteTarget term symm cfg)
+      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
diff --git a/server/nng/NNG/Tactic/Simp.lean b/server/nng/NNG/Tactic/Simp.lean
new file mode 100644
index 0000000..2716d23
--- /dev/null
+++ b/server/nng/NNG/Tactic/Simp.lean
@@ -0,0 +1,51 @@
+import Mathlib.Lean.Expr.Basic
+import Lean.Elab.Tactic.Basic
+import NNG.Tactic.Rfl
+
+/-! # `simp` tactic
+
+Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
+-/
+
+namespace MyNat
+
+open Lean Meta Elab Tactic
+
+-- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
+
+/--
+The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
+non-dependent hypotheses. It has many variants:
+- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
+- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
+  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.
+  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with
+  `f` are used. This provides a convenient way to unfold `f`.
+- `simp [*]` simplifies the main goal target using the lemmas tagged with the
+  attribute `[simp]` and all hypotheses.
+- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
+- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
+  with the attribute `[simp]`, but removes the ones named `idᵢ`.
+- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
+  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
+  `hᵢ` is introduced, but the old one remains in the local context.
+- `simp at *` simplifies all the hypotheses and the target.
+- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
+  other hypotheses.
+-/
+syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic
+
+/-
+  "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
+-/
+@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
+  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+  let usedSimps ← dischargeWrapper.with fun discharge? =>
+    simpLocation ctx discharge? (expandOptLocation stx[5])
+  if tactic.simp.trace.get (← getOptions) then
+    traceSimpCall stx usedSimps
+
+end MyNat
+
+