initial commit

.gitignore

@@ -0,0 +1,2 @@
+build/
+lake-packages/

NNG.lean

@@ -0,0 +1,64 @@
+import GameServer.Commands
+
+import NNG.Levels.Tutorial
+import NNG.Levels.Addition
+import NNG.Levels.Multiplication
+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
+
+Game "NNG"
+Title "Natural Number Game"
+Introduction
+"
+# Natural Number Game
+
+##### version 3.0.1
+
+Welcome to the natural number game -- a game which shows the power of induction.
+
+In this game, you get own version of the natural numbers, in an interactive
+theorem prover called Lean. Your version of the natural numbers satisfies something called
+the principle of mathematical induction, and a couple of other things too (Peano's axioms).
+Unfortunately, nobody has proved any theorems about these
+natural numbers yet! For example, addition will be defined for you,
+but nobody has proved that `x + y = y + x` yet. This is your job. You're going to
+prove mathematical theorems using the Lean theorem prover. In other words, you're going to solve
+levels in a computer game.
+
+You're going to prove these theorems using *tactics*. The introductory world, Tutorial World,
+will take you through some of these tactics. During your proofs, the assistant shows your
+\"goal\" (i.e. what you're supposed to be proving) and keeps track of the state of your proof.
+
+Click on the blue \"Tutorial World\" to start your journey!
+
+## Save progress
+
+The game stores your progress locally in your browser storage.
+If you delete it, your progress will be lost!
+
+(usually the *website data* gets deleted together with cookies.)
+
+## Credits
+
+* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar
+* **Content adaptation**: Jon Eugster
+* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot
+
+## Resources
+
+* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum
+* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
+* [A textbook-style (lean4) version of the NN-game](https://lovettsoftware.com/NaturalNumbers/TutorialWorld/Level1.lean.html)
+
+"
+
+Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition → AdvMultiplication
+Path Addition → Multiplication → AdvMultiplication -- → Inequality
+Path Multiplication → Power
+
+MakeGame

NNG/Doc/Definitions.lean

@@ -0,0 +1,88 @@
+import GameServer.Commands
+
+DefinitionDoc MyNat as "ℕ"
+"
+The Natural Numbers. These are constructed through:
+
+* `(0 : ℕ)`, an element called zero.
+* `(succ : ℕ → ℕ)`, the successor function , i.e. one is `succ 0` and two is `succ (succ 0)`.
+* `induction` (or `rcases`), tactics to treat the cases $n = 0$ and `n = m + 1` seperately.
+
+## Game Modifications
+
+This notation is for our own version of the natural numbers, called `MyNat`.
+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 "+" "
+Addition on `ℕ` is defined through two axioms:
+
+* `add_zero (a : ℕ) : a + 0 = a`
+* `add_succ (a d : ℕ) : a + succ d = succ (a + d)`
+"
+
+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 "≠" ""

NNG/Doc/Lemmas.lean

@@ -0,0 +1,168 @@
+import GameServer.Commands
+
+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 "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 "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_assoc as "add_assoc" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.succ_add as "succ_add" in "Add"
+"(missing)"
+
+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 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"
+"(missing)"
+
+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)"
+

NNG/Doc/Tactics.lean

@@ -0,0 +1,186 @@
+import GameServer.Commands
+
+TacticDoc rfl
+"
+## Summary
+
+`rfl` proves goals of the form `X = X`.
+
+## Details
+
+The `rfl` tactic will close any goal of the form `A = B`
+where `A` and `B` are *exactly the same thing*.
+
+## Example:
+If it looks like this in the top right hand box:
+```
+Objects:
+  a b c d : ℕ
+Goal:
+  (a + b) * (c + d) = (a + b) * (c + d)
+```
+
+then `rfl` will close the goal and solve the level.
+
+## Game modifications
+`rfl` in this game is weakened.
+
+The real `rfl` could also proof goals of the form `A = B` where the
+two sides are not *exactly identical* but merely
+*\"definitionally equal\"*. That means the real `rfl`
+could prove things like `a + 0 = a`.
+
+"
+
+
+TacticDoc rw
+"
+## Summary
+
+If `h` is a proof of `X = Y`, then `rw [h]` will change
+all `X`s in the goal to `Y`s.
+
+### Variants
+
+* `rw [← h#` (changes `Y` to `X`)
+* `rw [h] at h2` (changes `X` to `Y` in hypothesis `h2` instead of the goal)
+* `rw [h] at *` (changes `X` to `Y` in the goal and all hypotheses)
+
+## Details
+
+The `rw` tactic is a way to do \"substituting in\". There
+are two distinct situations where use this tactics.
+
+1) If `h : A = B` is a hypothesis (i.e., a proof of `A = B`)
+in your local context (the box in the top right)
+and if your goal contains one or more `A`s, then `rw [h]`
+will change them all to `B`'s.
+
+2) The `rw` tactic will also work with proofs of theorems
+which are equalities (look for them in the drop down
+menu on the left, within Theorem Statements).
+For example, in world 1 level 4
+we learn about `add_zero x : x + 0 = x`, and `rw [add_zero]`
+will change `x + 0` into `x` in your goal (or fail with
+an error if Lean cannot find `x + 0` in the goal).
+
+Important note: if `h` is not a proof of the form `A = B`
+or `A ↔ B` (for example if `h` is a function, an implication,
+or perhaps even a proposition itself rather than its proof),
+then `rw` is not the tactic you want to use. For example,
+`rw (P = Q)` is never correct: `P = Q` is the true-false
+statement itself, not the proof.
+If `h : P = Q` is its proof, then `rw [h]` will work.
+
+Pro tip 1: If `h : A = B` and you want to change
+`B`s to `A`s instead, try `rw ←h` (get the arrow with `\\l` and
+note that this is a small letter L, not a number 1).
+
+### Example:
+If it looks like this in the top right hand box:
+
+```
+Objects:
+  x y : ℕ
+Assumptions:
+  h : x = y + y
+Goal:
+  succ (x + 0) = succ (y + y)
+```
+
+then
+
+`rw [add_zero]`
+
+will change the goal into `succ x = succ (y + y)`, and then
+
+`rw [h]`
+
+will change the goal into `succ (y + y) = succ (y + y)`, which
+can be solved with `rfl`.
+
+### Example:
+
+You can use `rw` to change a hypothesis as well.
+For example, if your local context looks like this:
+
+```
+Objects:
+  x y : ℕ
+Assumptions:
+  h1 : x = y + 3
+  h2 : 2 * y = x
+Goal:
+  y = 3
+```
+then `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.
+
+## Game modifications
+
+The real `rw` tactic does automatically try to call `rfl` afterwards. We disabled this
+feature for the game.
+"
+
+TacticDoc induction
+"
+"
+
+TacticDoc exact
+"
+"
+
+TacticDoc apply
+"
+"
+
+TacticDoc intro
+"
+"
+
+TacticDoc «have»
+"
+"
+
+TacticDoc constructor
+"
+"
+
+TacticDoc rcases
+"
+"
+
+TacticDoc left
+"
+"
+
+TacticDoc revert
+"
+"
+
+TacticDoc tauto
+"
+"
+
+TacticDoc right
+"
+"
+
+TacticDoc by_cases
+"
+"
+
+TacticDoc contradiction
+"
+"
+
+TacticDoc exfalso
+"
+"
+
+TacticDoc simp
+"
+"
+
+TacticDoc «repeat»
+"
+"

NNG/Levels/Addition.lean

@@ -0,0 +1,36 @@
+import NNG.Levels.Addition.Level_6
+
+Game "NNG"
+World "Addition"
+Title "Addition World"
+
+Introduction
+"
+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:
+
+  * 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:
+
+  * `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:
+
+  * `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.
+"

NNG/Levels/Addition/Level_1.lean

@@ -0,0 +1,95 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Addition"
+Level 1
+Title "the induction tactic."
+
+open MyNat
+
+Introduction
+"
+OK so let's see induction in action. We're going to prove
+
+```
+zero_add (n : ℕ) : 0 + n = n
+```
+
+Wait… what is going on here? Didn't we already prove that adding zero to $n$ gave us $n$?
+
+No we didn't! We proved $n + 0 = n$, and that proof was called `add_zero`. We're now
+trying to establish `zero_add`, the proof that $0 + n = n$.
+
+But aren't these two theorems the same?
+
+No they're not! It is *true* that `x + y = y + x`, but we haven't *proved* it yet,
+and in fact we will need both `add_zero` and `zero_add` in order
+to prove this. In fact `x + y = y + x` is the boss level for addition world,
+and `induction` is the only other tactic you'll need to beat it.
+
+Now `add_zero` is one of Peano's axioms, so we don't need to prove it, we already have it.
+To prove `0 + n = n` we need to use induction on $n$. While we're here,
+note that `zero_add` is about zero add something, and `add_zero` is about something add zero.
+The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`.
+"
+
+Statement MyNat.zero_add
+"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:
+  `induction n with d hd`.
+
+  If you use the `with` part, you can name your variable and induction hypothesis, otherwise
+  they get default names."
+  induction n with n hn
+  · Hint "Now you have two goals. Once you proved the first, you will jump to the second one.
+    This first goal is the base case $n = 0$.
+
+    Recall that you can use all lemmas that are visible in your inventory."
+    Hint (hidden := true) "try using `add_zero`."
+    rw [add_zero]
+    rfl
+  · Hint "Now you jumped to the second goal. Here you have the induction hypothesis
+    `{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:
+
+* `induction n with d hd`
+* `rw [h]`
+* `rfl`
+
+will get you quite a long way through this game. Using only these tactics
+you can beat Addition World level 4 (the boss level of Addition World),
+all of Multiplication World including the boss level `a * b = b * a`,
+and even all of Power World including the fiendish final boss. This route will
+give you a good grounding in these three basic tactics; after that, if you
+are still interested, there are other worlds to master, where you can learn
+more tactics.
+
+But we're getting ahead of ourselves, you still have to beat the rest of Addition World. 
+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). Any of the people there might be able to help.
+
+Good luck! Click on \"Next\" to solve some levels on your own.
+"

NNG/Levels/Addition/Level_2.lean

@@ -0,0 +1,58 @@
+import NNG.Levels.Addition.Level_1
+
+Game "NNG"
+World "Addition"
+Level 2
+Title "add_assoc (associativity of addition)"
+
+open MyNat
+
+Introduction
+"
+It's well-known that $(1 + 2) + 3 = 1 + (2 + 3)$; if we have three numbers
+to add up, it doesn't matter which of the additions we do first. This fact
+is called *associativity of addition* by mathematicians, and it is *not*
+obvious. For example, subtraction really is not associative: $(6 - 2) - 1$
+is really not equal to $6 - (2 - 1)$. We are going to have to prove
+that addition, as defined the way we've defined it, is associative.
+
+See if you can prove associativity of addition.
+"
+
+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
+  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!).
+
+  Note that when Lean writes `a + b + c`, it means `(a + b) + c`. If it wants to talk
+  about `a + (b + c)` it will put the brackets in explictly."
+  Branch
+    induction a
+    Hint "Good luck with that…"
+    simp?
+    --rw [zero_add, zero_add]
+    --rfl
+  Branch
+    induction b
+    Hint "Good luck with that…"
+  induction c with c hc
+  Hint (hidden := true) "look at the lemma `add_zero`."
+  rw [add_zero]
+  Hint "`rw [add_zero]` only rewrites one term of the form `… + 0`, so you might to
+  use it multiple times."
+  rw [add_zero]
+  rfl
+  Hint (hidden := true) "`add_succ` might help here."
+  rw [add_succ]
+  rw [add_succ]
+  rw [add_succ]
+  Hint (hidden := true) "Now you can use the induction hypothesis."
+  rw [hc]
+  rfl
+
+NewLemma MyNat.zero_add
+LemmaTab "Add"

NNG/Levels/Addition/Level_3.lean

@@ -0,0 +1,53 @@
+import NNG.Levels.Addition.Level_2
+
+Game "NNG"
+World "Addition"
+Level 3
+Title "succ_add"
+
+open MyNat
+
+Introduction
+"
+Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add`
+is the proof that `succ(a) + b = succ(a + b)` for `a` and `b` in your
+natural number type. We need to prove this now, because we will need
+to use this result in our proof that `a + b = b + a` in the next level.
+
+NB: think about why computer scientists called this result `succ_add` .
+There is a logic to all the names.
+
+Note that if you want to be more precise about exactly where you want
+to rewrite something like `add_succ` (the proof you already have),
+you can do things like `rw [add_succ (succ a)]` or
+`rw [add_succ (succ a) d]`, telling Lean explicitly what to use for
+the input variables for the function `add_succ`. Indeed, `add_succ`
+is a function: it takes as input two variables `a` and `b` and outputs a proof
+that `a + succ(b) = succ(a + b)`. The tactic `rw [add_succ]` just says to Lean \"guess
+what the variables are\".
+"
+
+Statement MyNat.succ_add
+"For all natural numbers $a, b$, we have
+$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$."
+    (a b : ℕ) : succ a + b = succ (a + b)  := by
+  Hint (hidden := true) "You might again want to start by induction
+  on the right-most variable."
+  Branch
+    induction a
+    Hint "Induction on `a` will not work."
+  induction b with d hd
+  · rw [add_zero]
+    rw [add_zero]
+    rfl
+  · rw [add_succ]
+    rw [hd]
+    rw [add_succ]
+    rfl
+
+LemmaTab "Add"
+
+Conclusion
+"
+
+"

NNG/Levels/Addition/Level_4.lean

@@ -0,0 +1,50 @@
+import NNG.Levels.Addition.Level_3
+
+Game "NNG"
+World "Addition"
+Level 4
+Title "`add_comm` (boss level)"
+
+open MyNat
+
+Introduction
+"
+[boss battle music]
+
+Look in your inventory to see the proofs you have available.
+These should be enough.
+"
+
+Statement MyNat.add_comm
+"On the set of natural numbers, addition is commutative.
+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]
+      rw [add_zero]
+      rfl
+    · rw [succ_add]
+      rw [hd]
+      rw [add_succ]
+      rfl
+  induction b with d hd
+  · rw [zero_add]
+    rw [add_zero]
+    rfl
+  · rw [add_succ]
+    rw [hd]
+    rw [succ_add]
+    rfl
+
+LemmaTab "Add"
+
+Conclusion
+"
+If you got this far -- nice! You're nearly ready to make a choice:
+Multiplication World or Function World. But there are just a couple
+more useful lemmas in Addition World which you should prove first.
+Press on to level 5.
+"

NNG/Levels/Addition/Level_5.lean

@@ -0,0 +1,43 @@
+import NNG.Levels.Addition.Level_4
+
+Game "NNG"
+World "Addition"
+Level 5
+Title "succ_eq_add_one"
+
+open MyNat
+
+axiom MyNat.one_eq_succ_zero : (1 : ℕ) = succ 0
+
+Introduction
+"
+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.
+
+Levels 5 and 6 are the two last levels in Addition World.
+Level 5 involves the number $1$. When you see a $1$ in your goal,
+you can write `rw [one_eq_succ_zero]` to get back
+to something which only mentions `0`. This is a good move because $0$ is easier for us to
+manipulate than $1$ right now, because we have
+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
+"For any natural number $n$, we have
+$ \\operatorname{succ}(n) = n+1$ ."
+    (n : ℕ) : succ n = n + 1 := by
+  rw [one_eq_succ_zero]
+  rw [add_succ]
+  rw [add_zero]
+  rfl
+
+NewLemma MyNat.one_eq_succ_zero
+NewDefinition One
+LemmaTab "Add"
+
+Conclusion
+"
+Well done! On to the last level!
+"

NNG/Levels/Addition/Level_6.lean

@@ -0,0 +1,114 @@
+import NNG.Levels.Addition.Level_5
+
+Game "NNG"
+World "Addition"
+Level 6
+Title "add_right_comm"
+
+open MyNat
+
+Introduction
+"
+Lean sometimes writes `a + b + c`. What does it mean? The convention is
+that if there are no brackets displayed in an addition formula, the brackets
+are around the left most `+` (Lean's addition is \"left associative\").
+So the goal in this level is `(a + b) + c = (a + c) + b`. This isn't
+quite `add_assoc` or `add_comm`, it's something you'll have to prove
+by putting these two theorems together.
+
+If you hadn't picked up on this already, `rw [add_assoc]` will
+change `(x + y) + z` to `x + (y + z)`, but to change it back
+you will need `rw [← add_assoc]`. Get the left arrow by typing `\\l`
+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.
+
+
+"
+
+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

NNG/Levels/AdvAddition.lean

@@ -0,0 +1,28 @@
+import NNG.Levels.AdvAddition.Level_13
+
+Game "NNG"
+World "AdvAddition"
+Title "Advanced Addition World"
+
+Introduction
+"
+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.
+"

NNG/Levels/AdvAddition/Level_1.lean

@@ -0,0 +1,46 @@
+import NNG.Metadata
+import NNG.MyNat.AdvAddition
+import NNG.Levels.Addition
+
+Game "NNG"
+World "AdvAddition"
+Level 1
+Title "`succ_inj`. A function."
+
+open MyNat
+
+Introduction
+"
+Let's finally learn how 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 $\\operatorname{succ}(a)=\\operatorname{succ}(b)$,
+then we can deduce $a=b$."
+    {a b : ℕ} (hs : succ a = succ b) :  a = b := by
+  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
+LemmaTab "Nat"
+
+Conclusion
+"
+**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*
+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.
+"

NNG/Levels/AdvAddition/Level_10.lean

@@ -0,0 +1,77 @@
+import NNG.Levels.AdvAddition.Level_9
+import Std.Tactic.RCases
+
+Game "NNG"
+World "AdvAddition"
+Level 10
+Title "add_left_eq_zero"
+
+open MyNat
+
+Introduction
+"
+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*.
+
+The following lemma, $a+b=0\\implies b=0$, will be useful in inequality world.
+"
+
+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
+  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
+  · 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
+"
+
+"

NNG/Levels/AdvAddition/Level_11.lean

@@ -0,0 +1,30 @@
+import NNG.Levels.AdvAddition.Level_10
+
+Game "NNG"
+World "AdvAddition"
+Level 11
+Title "add_right_eq_zero"
+
+open MyNat
+
+Introduction
+"
+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 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
+
+LemmaTab "Add"
+
+Conclusion
+"
+
+"

NNG/Levels/AdvAddition/Level_12.lean

@@ -0,0 +1,34 @@
+import NNG.Levels.AdvAddition.Level_11
+
+
+Game "NNG"
+World "AdvAddition"
+Level 12
+Title "add_one_eq_succ"
+
+open MyNat
+
+Introduction
+"
+We have
+
+```
+succ_eq_add_one (n : ℕ) : succ n = n + 1
+```
+
+but sometimes the other way is also convenient.
+"
+
+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
+"
+
+"

NNG/Levels/AdvAddition/Level_13.lean

@@ -0,0 +1,38 @@
+import NNG.Levels.AdvAddition.Level_12
+
+Game "NNG"
+World "AdvAddition"
+Level 13
+Title "ne_succ_self"
+
+open MyNat
+
+Introduction
+"
+The last level in Advanced Addition World is the statement
+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
+  · 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).
+"

NNG/Levels/AdvAddition/Level_2.lean

@@ -0,0 +1,56 @@
+import NNG.Levels.AdvAddition.Level_1
+
+
+Game "NNG"
+World "AdvAddition"
+Level 2
+Title "succ_succ_inj"
+
+open MyNat
+
+Introduction
+"
+In the below theorem, we need to apply `succ_inj` twice. Once to prove
+$\\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
+$\\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.
+
+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 : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
+  apply succ_inj
+  apply succ_inj
+  exact h
+
+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)
+```
+"

NNG/Levels/AdvAddition/Level_3.lean

@@ -0,0 +1,28 @@
+import NNG.Levels.AdvAddition.Level_2
+
+
+Game "NNG"
+World "AdvAddition"
+Level 3
+Title "succ_eq_succ_of_eq"
+
+open MyNat
+
+Introduction
+"
+We are going to prove something completely obvious: if $a=b$ then
+$\\operatorname{succ}(a)=\\operatorname{succ}(b)$. This is *not* `succ_inj`!
+"
+
+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
+
+LemmaTab "Nat"

NNG/Levels/AdvAddition/Level_4.lean

@@ -0,0 +1,44 @@
+import NNG.Levels.AdvAddition.Level_3
+
+Game "NNG"
+World "AdvAddition"
+Level 4
+Title "eq_iff_succ_eq_succ"
+
+open MyNat
+
+Introduction
+"
+Here is an `iff` goal. You can split it into two goals (the implications in both
+directions) using the `constructor` tactic, which is how you're going to have to start.
+"
+
+Statement
+"Two natural numbers are equal if and only if their successors are equal.
+"
+    (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
+  ```
+  "
+  · 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
+"
+
+"

NNG/Levels/AdvAddition/Level_5.lean

@@ -0,0 +1,44 @@
+import NNG.Levels.AdvAddition.Level_4
+
+
+Game "NNG"
+World "AdvAddition"
+Level 5
+Title "add_right_cancel"
+
+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`. 
+"
+
+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
+  exact h
+  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
+"
+
+"

NNG/Levels/AdvAddition/Level_6.lean

@@ -0,0 +1,37 @@
+import NNG.Levels.AdvAddition.Level_5
+
+Game "NNG"
+World "AdvAddition"
+Level 6
+Title "add_left_cancel"
+
+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`.
+"
+
+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
+"
+
+"

NNG/Levels/AdvAddition/Level_7.lean

@@ -0,0 +1,30 @@
+import NNG.Levels.AdvAddition.Level_6
+
+Game "NNG"
+World "AdvAddition"
+Level 7
+Title "add_right_cancel_iff"
+
+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 `constructor`
+to split an `↔` goal into the `→` goal and the `←` goal.
+"
+
+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
+  · 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"
+

NNG/Levels/AdvAddition/Level_8.lean

@@ -0,0 +1,34 @@
+import NNG.Levels.AdvAddition.Level_7
+
+
+Game "NNG"
+World "AdvAddition"
+Level 8
+Title "eq_zero_of_add_right_eq_self"
+
+open MyNat
+
+Introduction
+"
+The lemma you're about to prove will be useful when we want to prove that $\\leq$ is antisymmetric.
+There are some wrong paths that you can take with this one.
+"
+
+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
+"
+
+"

NNG/Levels/AdvAddition/Level_9.lean

@@ -0,0 +1,53 @@
+import NNG.Levels.AdvAddition.Level_8
+
+Game "NNG"
+World "AdvAddition"
+Level 9
+Title "succ_ne_zero"
+
+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`.
+
+```
+zero_ne_succ (a : ¬) : 0 ≠ 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 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
+"
+
+"

NNG/Levels/AdvMultiplication.lean

@@ -0,0 +1,17 @@
+import NNG.Levels.AdvMultiplication.Level_1
+import NNG.Levels.AdvMultiplication.Level_2
+import NNG.Levels.AdvMultiplication.Level_3
+import NNG.Levels.AdvMultiplication.Level_4
+
+
+Game "NNG"
+World "AdvMultiplication"
+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.
+"

NNG/Levels/AdvMultiplication/Level_1.lean

@@ -0,0 +1,51 @@
+import NNG.Levels.Multiplication
+import NNG.Levels.AdvAddition
+
+Game "NNG"
+World "AdvMultiplication"
+Level 1
+Title "mul_pos"
+
+open MyNat
+
+Introduction
+"
+## 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
+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`,
+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."
+    (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 := by
+  intro ha hb
+  intro hab
+  induction b with b
+  apply hb
+  rfl
+  rw [mul_succ] at hab
+  apply ha
+  induction a with a
+  rfl
+  rw [add_succ] at hab
+  exfalso
+  exact succ_ne_zero _ hab
+
+Conclusion
+"
+
+"

NNG/Levels/AdvMultiplication/Level_2.lean

@@ -0,0 +1,33 @@
+import NNG.Levels.AdvMultiplication.Level_1
+
+Game "NNG"
+World "AdvMultiplication"
+Level 2
+Title "eq_zero_or_eq_zero_of_mul_eq_zero"
+
+open MyNat
+
+Introduction
+"
+A variant on the previous level.
+"
+
+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
+  right
+  rfl
+  exfalso
+  rw [mul_succ] at h
+  rw [add_succ] at h
+  exact succ_ne_zero _ h
+
+Conclusion
+"
+
+"

NNG/Levels/AdvMultiplication/Level_3.lean

@@ -0,0 +1,36 @@
+import NNG.Levels.AdvMultiplication.Level_2
+
+
+Game "NNG"
+World "AdvMultiplication"
+Level 3
+Title "mul_eq_zero_iff"
+
+open MyNat
+
+Introduction
+"
+Now you have `eq_zero_or_eq_zero_of_mul_eq_zero` this is pretty straightforward.
+"
+
+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
+  constructor
+  intro h
+  exact eq_zero_or_eq_zero_of_mul_eq_zero a b h
+  intro hab
+  rcases hab with hab | hab
+  rw [hab]
+  rw [zero_mul]
+  rfl
+  rw [hab]
+  rw [mul_zero]
+  rfl
+
+
+Conclusion
+"
+
+"

NNG/Levels/AdvMultiplication/Level_4.lean

@@ -0,0 +1,99 @@
+import NNG.Levels.AdvMultiplication.Level_3
+
+Game "NNG"
+World "AdvMultiplication"
+Level 4
+Title "mul_left_cancel"
+
+open MyNat
+
+Introduction
+"
+This is the last of the bonus multiplication levels.
+`mul_left_cancel` will be useful in inequality world.
+
+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
+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,
+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
+be to show $ab=a(d+1) \\implies b=d+1$. When you also assume $ab=a(d+1)$
+you will realise that your inductive hypothesis is *useless*, because
+$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\\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.
+
+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`
+tactic; it replaces the `b` in the hypotheses with \"for all $b$\" in the goal.
+
+[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 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
+  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
+"
+
+"
+
+

NNG/Levels/AdvProposition.lean

@@ -0,0 +1,23 @@
+import NNG.Levels.AdvProposition.Level_1
+import NNG.Levels.AdvProposition.Level_2
+import NNG.Levels.AdvProposition.Level_3
+import NNG.Levels.AdvProposition.Level_4
+import NNG.Levels.AdvProposition.Level_5
+import NNG.Levels.AdvProposition.Level_6
+import NNG.Levels.AdvProposition.Level_7
+import NNG.Levels.AdvProposition.Level_8
+import NNG.Levels.AdvProposition.Level_9
+import NNG.Levels.AdvProposition.Level_10
+
+
+Game "NNG"
+World "AdvProposition"
+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.
+"

NNG/Levels/AdvProposition/Level_1.lean

@@ -0,0 +1,40 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 1
+Title "the `split` tactic"
+
+open MyNat
+
+Introduction
+"
+The logical symbol `∧` means \"and\". If $P$ and $Q$ are propositions, then
+$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
+"
+"

NNG/Levels/AdvProposition/Level_10.lean

@@ -0,0 +1,65 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 10
+Title "The law of the excluded middle."
+
+open MyNat
+
+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).
+
+"
+
+Statement
+"If $P$ and $Q$ are true/false statements, then
+$$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$ 
+"
+    (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by
+  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.
+"
+
+-- 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. You'll be
+-- able to use it from now on.
+

NNG/Levels/AdvProposition/Level_2.lean

@@ -0,0 +1,49 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 2
+Title "the `rcases` tactic"
+
+open MyNat
+
+Introduction
+"
+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.
+"
+
+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
+
+  ```
+  intro h
+  ```
+
+  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
+
+  ```
+  rcases {h} with ⟨p, q⟩
+  ```
+
+  will change `{h}`, the proof of `P ∧ Q`, into two proofs `p : P`
+  and `q : Q`.
+
+  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
+

NNG/Levels/AdvProposition/Level_3.lean

@@ -0,0 +1,46 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 3
+Title "and_trans"
+
+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
+  rcases hpq with ⟨p, q⟩
+  intro hqr
+  rcases hqr with ⟨q', r⟩
+  constructor
+  assumption
+  assumption
+
+Conclusion
+"
+
+"

NNG/Levels/AdvProposition/Level_4.lean

@@ -0,0 +1,45 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 4
+Title ""
+
+open MyNat
+
+Introduction
+"
+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.
+
+"
+
+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
+  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
+  · intro p
+    apply qr
+    apply pq
+    exact p
+  · intro r
+    apply qp
+    apply rq
+    exact r
+
+NewDefinition Iff

NNG/Levels/AdvProposition/Level_5.lean

@@ -0,0 +1,76 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 5
+Title "Easter eggs."
+
+open MyNat
+
+Introduction
+"
+Let's try this again. Try proving it in other ways. (Note that `rcases` is temporarily disabled.)
+
+### A trick.
+
+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
+
+```
+intro hpq hqr
+constructor
+intro p
+apply hqr.1
+…
+```
+
+### Another trick
+
+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 `rcases` tactic on an iff statement;
+you cannot rewrite one-way implications, but you can rewrite two-way implications.
+
+
+"
+-- 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
+  intro r
+  apply hpq.2
+  apply hqr.2
+  assumption
+
+DisabledTactic rcases
+
+Conclusion
+"
+
+"

NNG/Levels/AdvProposition/Level_6.lean

@@ -0,0 +1,39 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 6
+Title "Or, and the `left` and `right` tactics."
+
+open MyNat
+
+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.
+
+Statement
+"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
+  exact q
+
+NewTactic left right
+NewDefinition Or
+

NNG/Levels/AdvProposition/Level_7.lean

@@ -0,0 +1,55 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 7
+Title "`or_symm`"
+
+open MyNat
+
+Introduction
+"
+Proving that $(P\\lor Q)\\implies(Q\\lor P)$ involves an element of danger.
+"
+
+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.
+"

NNG/Levels/AdvProposition/Level_8.lean

@@ -0,0 +1,53 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 8
+Title "`and_or_distrib_left`"
+
+open MyNat
+
+Introduction
+"
+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.
+"
+
+Statement --and_or_distrib_left
+"If $P$. $Q$ and $R$ are true/false statements, then
+$$P\\land(Q\\lor R)\\iff(P\\land Q)\\lor (P\\land R).$$ "
+    (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
+  constructor
+  intro h
+  rcases h with ⟨hp, hqr⟩
+  rcases hqr with q | r
+  left
+  constructor
+  exact hp
+  exact q
+  right
+  constructor
+  exact hp
+  exact r
+  intro h
+  rcases h with hpq | hpr
+  rcases hpq with ⟨p, q⟩
+  constructor
+  exact p
+  left
+  exact q
+  rcases hpr with ⟨hp, hr⟩
+  constructor
+  exact hp
+  right
+  exact hr
+
+
+Conclusion
+"
+You already know enough to embark on advanced addition world. But the next two levels comprise
+just a couple more things.
+"

NNG/Levels/AdvProposition/Level_9.lean

@@ -0,0 +1,52 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "AdvProposition"
+Level 9
+Title "`exfalso` and proof by contradiction. "
+
+open MyNat
+
+Introduction
+"
+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`.
+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.
+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 ⟩
+  -- 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"

NNG/Levels/Function.lean

@@ -0,0 +1,41 @@
+import NNG.Levels.Function.Level_1
+import NNG.Levels.Function.Level_2
+import NNG.Levels.Function.Level_3
+import NNG.Levels.Function.Level_4
+import NNG.Levels.Function.Level_5
+import NNG.Levels.Function.Level_6
+import NNG.Levels.Function.Level_7
+import NNG.Levels.Function.Level_8
+import NNG.Levels.Function.Level_9
+
+
+Game "NNG"
+World "Function"
+Title "Function World"
+
+Introduction
+"
+If you have beaten Addition World, then you have got
+quite good at manipulating equalities in Lean using the `rw` tactic.
+But there are plenty of levels later on which will require you
+to manipulate functions, and `rw` is not the tool for you here.
+
+To manipulate functions effectively, we need to learn about a new collection
+of tactics, namely `exact`, `intro`, `have` and `apply`. These tactics
+are specially designed for dealing with functions. Of course we are
+ultimately interested in using these tactics to prove theorems
+about the natural numbers – but in this
+world there is little point in working with specific sets like `mynat`,
+everything works for general sets.
+
+So our notation for this level is: $P$, $Q$, $R$ and so on denote general sets,
+and $h$, $j$, $k$ and so on denote general
+functions between them. What we will learn in this world is how to use functions
+in Lean to push elements from set to set. A word of warning –
+even though there's no harm at all in thinking of $P$ being a set and $p$
+being an element, you will not see Lean using the notation $p\\in P$, because
+internally Lean stores $P$ as a \"Type\" and $p$ as a \"term\", and it uses `p : P`
+to mean \"$p$ is a term of type $P$\", Lean's way of expressing the idea that $p$
+is an element of the set $P$. You have seen this already – Lean has
+been writing `n : ℕ` to mean that $n$ is a natural number.
+"

NNG/Levels/Function/Level_1.lean

@@ -0,0 +1,72 @@
+import NNG.Metadata
+
+-- TODO: Cannot import level from different world.
+
+Game "NNG"
+World "Function"
+Level 1
+Title "the `exact` tactic"
+
+open MyNat
+
+Introduction
+"
+## A new kind of goal.
+
+All through addition world, our goals have been theorems,
+and it was our job to find the proofs.
+**The levels in function world aren't theorems**. This is the only world where
+the levels aren't theorems in fact. In function world the object of a level
+is to create an element of the set in the goal. The goal will look like `Goal: X`
+with $X$ a set and you get rid of the goal by constructing an element of $X$.
+I don't know if you noticed this, but you finished
+essentially every goal of Addition World (and Multiplication World and Power World,
+if you played them) with `rfl`.
+This tactic is no use to us here.
+We are going to have to learn a new way of solving goals – the `exact` tactic.
+
+
+## The `exact` tactic
+
+If you can explicitly see how to make an element of your goal set,
+i.e. you have a formula for it, then you can just write `exact <formula>`
+and this will close the goal.
+"
+
+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 sets $P$ and $Q$ (but Lean calls them types),
+  and an element $p$ of $P$ (written `p : P`
+  but meaning $p\\in P$). We also have a function $h$ from $P$ to $Q$,
+  and our goal is to construct an
+  element of the set $Q$. It's clear what to do *mathematically* to solve
+  this goal -- we can
+  make an element of $Q$ by applying the function $h$ to
+  the element $p$. But how to do it in Lean? There are at least two ways
+  to explain this idea to Lean,
+  and here we will learn about one of them, namely the method which
+  uses the `exact` tactic.
+
+  Concretely, `h p` is an element of type `Q`, so you can use `exact h p` to use it.
+
+  Note that while in mathematics you might write $h(p)$, in Lean you always avoid brackets
+  for function application: `h p`. Brackets are only used for grouping elements, for
+  example for repeated funciton application, you could write `g (h p)`.
+  "
+  Hint (hidden := true) "
+  **Important note**: Note that `exact h P,` won't work (with a capital $P$);
+  this is a common error I see from beginners.
+  $P$ is not an element of $P$, it's $p$ that is an element of $P$.
+
+  So try `exact h p`.
+  "
+  exact h p
+
+NewTactic exact simp
+
+Conclusion
+"
+
+"

NNG/Levels/Function/Level_2.lean

@@ -0,0 +1,56 @@
+import NNG.Metadata
+import NNG.MyNat.Multiplication
+
+Game "NNG"
+World "Function"
+Level 2
+Title "the intro tactic"
+
+open MyNat
+
+Introduction
+"
+Let's make a function. Let's define the function on the natural
+numbers which sends a natural number $n$ to $3n+2$. You
+see that the goal is `ℕ → ℕ`. A mathematician
+might denote this set with some exotic name such as
+$\\operatorname{Hom}(\\mathbb{N},\\mathbb{N})$,
+but computer scientists use notation `X → Y` to denote the set of
+functions from `X` to `Y` and this name definitely has its merits.
+In type theory, `X → Y` is a type (the type of all functions from $X$ to $Y$),
+and `f : X → Y` means that `f` is a term
+of this type, i.e., $f$ is a function from $X$ to $Y$.
+
+To define a function $X\\to Y$ we need to choose an arbitrary
+element $x\\in X$ and then, perhaps using $x$, make an element of $Y$.
+The Lean tactic for \"let $x\\in X$ be arbitrary\" is `intro x`.
+"
+
+Statement
+"We define a function from ℕ to ℕ."
+    : ℕ → ℕ := by
+  Hint "To solve this goal,
+  you have to come up with a function from `ℕ`
+  to `ℕ`. Start with
+
+  `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
+  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`
+
+  will close the goal, ultimately defining the function $f({n})=3{n}+2$."
+  exact 3 * n + 2
+
+NewTactic intro
+
+Conclusion
+"
+## Rule of thumb:
+
+If your goal is `P → Q` then `intro p` will make progress.
+"

NNG/Levels/Function/Level_3.lean

@@ -0,0 +1,93 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 3
+Title "the have tactic"
+
+open MyNat
+
+Introduction
+"
+Say you have a whole bunch of sets and functions between them,
+and your goal is to build a certain element of a certain set.
+If it helps, you can build intermediate elements of other sets
+along the way, using the `have` command. `have` is the Lean analogue
+of saying \"let's define an element $q\\in Q$ by...\" in the middle of a calculation.
+It is often not logically necessary, but on the other hand
+it is very convenient, for example it can save on notation, or
+it can break proofs or calculations up into smaller steps.
+
+In the level below, we have an element of $P$ and we want an element
+of $U$; during the proof we will make several intermediate elements
+of some of the other sets involved. The diagram of sets and
+functions looks like this pictorially:
+
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
+\\end{CD}
+$$
+
+and so it's clear how to make the element of $U$ from the element of $P$.
+"
+
+Statement
+"Given an element of $P$ we can define an element of $U$."
+    (P Q R S T U: Type) (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 an element of $Q$:
+
+  ```
+  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
+  ```
+
+  (notice how we can explicitly tell Lean
+  what set we thought $t$ was in, with that `: T` thing before the `:=`.
+  This is optional unless Lean can not figure it out by itself.)
+  "
+  have t : T := j q
+  Hint "
+  Now we could even define $u$ to be $l(t)$:
+
+  ```
+  have u : U := l t
+  ```
+  "
+  have u : U := l t
+  Hint "…and then finish the level with `exact u`."
+  exact u
+
+NewTactic «have»
+
+Conclusion
+"
+If you solved the level using `have`, then you might have observed
+that before the final step the context got quite messy by all the intermediate
+variables we introduced. You can click \"Toggle Editor\" and then move the cursor
+around to see the proof you created.
+
+The context was already bad enough to start with, and we added three more
+terms to it. In level 4 we will learn about the `apply` tactic
+which solves the level using another technique, without leaving
+so much junk behind.
+"

NNG/Levels/Function/Level_4.lean

@@ -0,0 +1,64 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 4
+Title "the `apply` tactic"
+
+open MyNat
+
+Introduction
+"Let's do the same level again:
+
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
+\\end{CD}
+$$
+
+We are given $p \\in P$ and our goal is to find an element 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$.
+"
+
+Statement
+"Given an element of $P$ we can define an element of $U$."
+    (P Q R S T U: Type)
+(p : P)
+(h : P → Q)
+(i : Q → R)
+(j : Q → T)
+(k : S → T)
+(l : T → U) : U :=
+by
+  Hint "Our goal is to construct an element of the set $U$. But $l:T\\to U$ is
+  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
+  Hint "Notice that our assumptions don't change but *the goal changes*
+  from `U` to `T`.
+
+  Keep `apply`ing functions 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 an element of $P$)."
+  exact p
+
+NewTactic apply
+DisabledTactic «have»

NNG/Levels/Function/Level_5.lean

@@ -0,0 +1,56 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 5
+Title "P → (Q → P)"
+
+open MyNat
+
+Introduction
+"
+In this level, our goal is to construct a function, like in level 2.
+
+```
+P → (Q → P)
+```
+
+So $P$ and $Q$ are sets, and our goal is to construct a function
+which takes an element of $P$ and outputs a function from $Q$ to $P$.
+We don't know anything at all about the sets $P$ and $Q$, so initially
+this seems like a bit of a tall order. But let's give it a go.
+"
+
+Statement
+"We define an element of $\\operatorname{Hom}(P,\\operatorname{Hom}(Q,P))$."
+    (P Q : Type) : P → (Q → P) := by
+  Hint "Our goal is `P → X` for some set $X=\\operatorname\{Hom}(Q,P)$, and if our
+  goal is to construct a function then we almost always want to use the
+  `intro` tactic from level 2, Lean's version of \"let $p\\in P$ be arbitrary.\"
+  So let's start with
+
+  ```
+  intro p
+  ```"
+  intro p
+  Hint "
+  We now have an arbitrary element $p\\in P$ and we are supposed to be constructing
+  a function $Q\to P$. Well, how about the constant function, which
+  sends everything to $p$?
+  This will work. So let $q\\in Q$ be arbitrary:
+
+  ```
+  intro q
+  ```"
+  intro q
+  Hint "and then let's output `p`.
+
+  ```
+  exact p
+  ```"
+  exact p
+
+Conclusion
+"
+
+"

NNG/Levels/Function/Level_6.lean

@@ -0,0 +1,65 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 6
+Title "(P → (Q → R)) → ((P → Q) → (P → R))"
+
+open MyNat
+
+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`. 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.
+"
+
+Statement
+"Whatever the sets $P$ and $Q$ and $R$ are, we
+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
+  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
+"
+
+"

NNG/Levels/Function/Level_7.lean

@@ -0,0 +1,37 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 7
+Title "(P → Q) → ((Q → F) → (P → F))"
+
+open MyNat
+
+Introduction
+"
+Have you noticed that, in stark contrast to earlier worlds,
+we are not amassing a large collection of useful theorems?
+We really are just constructing abstract levels with sets and
+functions, and then solving them and never using the results
+ever again. Here's another one, which should hopefully be
+very easy for you now. Advanced mathematician viewers will
+know it as contravariance of $\\operatorname{Hom}(\\cdot,F)$
+functor.
+"
+
+Statement
+"Whatever the sets $P$ and $Q$ and $F$ are, we 
+make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
+\\operatorname{Hom}(\\operatorname{Hom}(Q,F),\\operatorname{Hom}(P,F)))$."
+    (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := by
+  intro f
+  intro h
+  intro p
+  apply h
+  apply f
+  exact p
+
+Conclusion
+"
+
+"

NNG/Levels/Function/Level_8.lean

@@ -0,0 +1,49 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 8
+Title "(P → Q) → ((Q → empty) → (P → empty))"
+
+open MyNat
+
+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).
+"
+
+Statement
+"Whatever the sets $P$ and $Q$ are, we
+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!
+  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?]
+  "
+  apply h
+  apply f
+  exact p
+
+Conclusion ""

NNG/Levels/Function/Level_9.lean

@@ -0,0 +1,43 @@
+import NNG.Metadata
+
+Game "NNG"
+World "Function"
+Level 9
+Title ""
+
+open MyNat
+
+Introduction
+"
+I asked around on Zulip and apparently there is not a tactic for this, perhaps because
+this level is rather artificial. In world 6 we will see a variant of this example
+which can be solved by a tactic. It would be an interesting project to make a tactic
+which could solve this sort of level in Lean.
+
+You can of course work both forwards and backwards, or you could crack and draw a picture.
+"
+
+Statement
+"Given a bunch of functions, we can define another one."
+    (A B C D E F G H I J K L : Type)
+    (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
+  apply f8
+  apply f5
+  apply f2
+  apply f1
+  exact a
+
+
+Conclusion
+"
+That's the end of Function World! Next it's Proposition world, and the tactics you've learnt in Function World are enough
+to solve all nine levels! In fact, the levels in Proposition world might look strangely familiar$\\ldots$.
+"

NNG/Levels/Inequality.lean

@@ -0,0 +1,50 @@
+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
+
+Game "NNG"
+World "Inequality"
+Title "Inequality World"
+
+Introduction
+"
+A new import, giving us a new definition. If `a` and `b` are naturals,
+`a ≤ b` is *defined* to mean
+
+`∃ (c : mynat), b = a + c`
+
+The upside-down E means \"there exists\". So in words, $a\\le b$
+if and only if there exists a natural $c$ such that $b=a+c$. 
+
+If you really want to change an `a ≤ b` to `∃ c, b = a + c` then
+you can do so with `rw le_iff_exists_add`:
+
+```
+le_iff_exists_add (a b : mynat) :
+  a ≤ b ↔ ∃ (c : mynat), b = a + c
+```
+
+But because `a ≤ b` is *defined as* `∃ (c : mynat), b = a + c`, you
+do not need to `rw le_iff_exists_add`, you can just pretend when you see `a ≤ b`
+that it says `∃ (c : mynat), b = a + c`. You will see a concrete
+example of this below.
+
+A new construction like `∃` means that we need to learn how to manipulate it.
+There are two situations. Firstly we need to know how to solve a goal
+of the form `⊢ ∃ c, ...`, and secondly we need to know how to use a hypothesis
+of the form `∃ c, ...`. 
+"

NNG/Levels/Inequality/Level_1.lean

@@ -0,0 +1,62 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+--import Mathlib.Tactic.Ring
+
+Game "NNG"
+World "Inequality"
+Level 1
+Title "the `use` tactic"
+
+open MyNat
+
+Introduction
+"
+The goal below is to prove $x\\le 1+x$ for any natural number $x$. 
+First let's turn the goal explicitly into an existence problem with
+
+`rw le_iff_exists_add,`
+
+and now the goal has become `∃ c : mynat, 1 + x = x + c`. Clearly
+this statement is true, and the proof is that $c=1$ will work (we also
+need the fact that addition is commutative, but we proved that a long
+time ago). How do we make progress with this goal?
+
+The `use` tactic can be used on goals of the form `∃ c, ...`. The idea
+is that we choose which natural number we want to use, and then we use it.
+So try
+
+`use 1,`
+
+and now the goal becomes `⊢ 1 + x = x + 1`. You can solve this by
+`exact add_comm 1 x`, or if you are lazy you can just use the `ring` tactic,
+which is a powerful AI which will solve any equality in algebra which can
+be proved using the standard rules of addition and multiplication. Now
+look at your proof. We're going to remove a line.
+
+## Important
+
+An important time-saver here is to note that because `a ≤ b` is *defined*
+as `∃ c : mynat, b = a + c`, you *do not need to write* `rw le_iff_exists_add`.
+The `use` tactic will work directly on a goal of the form `a ≤ b`. Just
+use the difference `b - a` (note that we have not defined subtraction so
+this does not formally make sense, but you can do the calculation in your head).
+If you have written `rw le_iff_exists_add` below, then just put two minus signs `--`
+before it and comment it out. See that the proof still compiles.
+"
+
+axiom add_comm (a b : ℕ) : a + b = b + a
+
+Statement --one_add_le_self
+"If $x$ is a natural number, then $x\\le 1+x$.
+"
+    (x : ℕ) : x ≤ 1 + x := by
+  rw [le_iff_exists_add]
+  use 1
+  rw [add_comm]
+  rfl
+  
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_10.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 10
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_11.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 11
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_12.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 12
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_13.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 13
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_14.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 14
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_15.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 15
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_16.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 16
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_17.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 17
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_2.lean

@@ -0,0 +1,28 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 2
+Title "le_rfl"
+
+open MyNat
+
+Introduction
+"
+Here's a nice easy one.
+"
+
+Statement
+"The $\\le$ relation is reflexive. In other words, if $x$ is a natural number,
+then $x\\le x$."
+    (x : ℕ) : x ≤ x := by
+  use 0
+  rw [add_zero]
+  rfl
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_3.lean

@@ -0,0 +1,59 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+import Std.Tactic.RCases
+
+Game "NNG"
+World "Inequality"
+Level 3
+Title "le_succ_of_le"
+
+open MyNat
+
+Introduction
+"
+We have seen how the `use` tactic makes progress on goals of the form `⊢ ∃ c, ...`.
+But what do we do when we have a *hypothesis* of the form `h : ∃ c, ...`?
+The hypothesis claims that there exists some natural number `c` with some
+property. How are we going to get to that natural number `c`? It turns out
+that the `cases` tactic can be used (just like it was used to extract
+information from `∧` and `∨` and `↔` hypotheses). Let me talk you through
+the proof of $a\\le b\\implies a\\le\\operatorname{succ}(b)$.
+
+The goal is an implication so we clearly want to start with 
+
+`intro h,`
+
+. After this, if you *want*, you can do something like
+
+`rw le_iff_exists_add at h ⊢,`
+
+(get the sideways T with `\\|-` then space). This changes the `≤` into
+its `∃` form in `h` and the goal -- but if you are happy with just
+*imagining* the `∃` whenever you read a `≤` then you don't need to do this line.
+
+Our hypothesis `h` is now `∃ (c : mynat), b = a + c` (or `a ≤ b` if you
+elected not to do the definitional rewriting) so
+
+`cases h with c hc,`
+
+gives you the natural number `c` and the hypothesis `hc : b = a + c`.
+Now use `use` wisely and you're home.
+
+"
+
+Statement
+"For all naturals $a$, $b$, if $a\\leq b$ then $a\\leq \\operatorname{succ}(b)$. 
+"
+    (a b : ℕ) : a ≤ b → a ≤ (succ b) := by
+  intro h
+  rcases h with ⟨c, hc⟩
+  rw [hc]
+  use c + 1
+  sorry
+  --rfl
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_4.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 4
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_5.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 5
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_6.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 6
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_7.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 7
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_8.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 8
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Inequality/Level_9.lean

@@ -0,0 +1,25 @@
+import NNG.Metadata
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+
+Game "NNG"
+World "Inequality"
+Level 9
+Title ""
+
+open MyNat
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : true := by
+  trivial
+
+Conclusion
+"
+
+"

NNG/Levels/Multiplication.lean

@@ -0,0 +1,37 @@
+import NNG.Levels.Multiplication.Level_1
+import NNG.Levels.Multiplication.Level_2
+import NNG.Levels.Multiplication.Level_3
+import NNG.Levels.Multiplication.Level_4
+import NNG.Levels.Multiplication.Level_5
+import NNG.Levels.Multiplication.Level_6
+import NNG.Levels.Multiplication.Level_7
+import NNG.Levels.Multiplication.Level_8
+import NNG.Levels.Multiplication.Level_9
+
+
+Game "NNG"
+World "Multiplication"
+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!
+"

NNG/Levels/Multiplication/Level_1.lean

@@ -0,0 +1,35 @@
+import NNG.MyNat.Multiplication
+import NNG.Levels.Addition
+
+Game "NNG"
+World "Multiplication"
+Level 1
+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 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
+
+NewTactic simp
+NewLemma MyNat.mul_zero MyNat.mul_succ
+NewDefinition Mul
+LemmaTab "Mul"

NNG/Levels/Multiplication/Level_2.lean

@@ -0,0 +1,31 @@
+import NNG.Levels.Multiplication.Level_1
+
+Game "NNG"
+World "Multiplication"
+Level 2
+Title "mul_one"
+
+open MyNat
+
+Introduction
+"
+In this level we'll need to use
+
+* `one_eq_succ_zero : 1 = succ 0 `
+
+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"

NNG/Levels/Multiplication/Level_3.lean

@@ -0,0 +1,38 @@
+import NNG.Levels.Multiplication.Level_2
+
+Game "NNG"
+World "Multiplication"
+Level 3
+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 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
+
+LemmaTab "Mul"
+
+Conclusion ""

NNG/Levels/Multiplication/Level_4.lean

@@ -0,0 +1,44 @@
+import NNG.Levels.Multiplication.Level_3
+
+Game "NNG"
+World "Multiplication"
+Level 4
+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 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
+
+LemmaTab "Mul"
+

NNG/Levels/Multiplication/Level_5.lean

@@ -0,0 +1,43 @@
+import NNG.Levels.Multiplication.Level_4
+
+Game "NNG"
+World "Multiplication"
+Level 5
+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 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
+"
+
+"

NNG/Levels/Multiplication/Level_6.lean

@@ -0,0 +1,52 @@
+import NNG.Levels.Multiplication.Level_5
+
+Game "NNG"
+World "Multiplication"
+Level 6
+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 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
+"
+
+"

NNG/Levels/Multiplication/Level_7.lean

@@ -0,0 +1,46 @@
+import NNG.Levels.Multiplication.Level_6
+
+Game "NNG"
+World "Multiplication"
+Level 7
+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 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
+"
+
+"

NNG/Levels/Multiplication/Level_8.lean

@@ -0,0 +1,46 @@
+import NNG.Levels.Multiplication.Level_7
+
+Game "NNG"
+World "Multiplication"
+Level 8
+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 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

NNG/Levels/Multiplication/Level_9.lean

@@ -0,0 +1,57 @@
+import NNG.Levels.Multiplication.Level_8
+
+Game "NNG"
+World "Multiplication"
+Level 9
+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 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\".
+"

NNG/Levels/Power.lean

@@ -0,0 +1,29 @@
+import NNG.Levels.Power.Level_8
+
+Game "NNG"
+World "Power"
+Title "Power World"
+
+Introduction
+"
+A new world with seven levels. And a new import!
+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 : ℕ) : 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 `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.
+
+The levels in this world were designed by Sian Carey, a UROP student
+at Imperial College London, funded by a Mary Lister McCammon Fellowship,
+in the summer of 2019. Thanks Sian!
+"

NNG/Levels/Power/Level_1.lean

@@ -0,0 +1,19 @@
+import NNG.Levels.Multiplication
+import NNG.MyNat.Power
+
+Game "NNG"
+World "Power"
+Level 1
+Title "zero_pow_zero"
+
+open MyNat
+
+Statement MyNat.zero_pow_zero
+"$0 ^ 0 = 1$"
+    : (0 : ℕ) ^ 0  = 1 := by
+  rw [pow_zero]
+  rfl
+
+NewLemma MyNat.pow_zero MyNat.pow_succ
+NewDefinition Pow
+LemmaTab "Pow"

NNG/Levels/Power/Level_2.lean

@@ -0,0 +1,17 @@
+import NNG.Levels.Power.Level_1
+
+Game "NNG"
+World "Power"
+Level 2
+Title "zero_pow_succ"
+
+open MyNat
+
+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
+
+LemmaTab "Pow"

NNG/Levels/Power/Level_3.lean

@@ -0,0 +1,19 @@
+import NNG.Levels.Power.Level_2
+
+Game "NNG"
+World "Power"
+Level 3
+Title "pow_one"
+
+open MyNat
+
+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
+
+LemmaTab "Pow"

NNG/Levels/Power/Level_4.lean

@@ -0,0 +1,22 @@
+import NNG.Levels.Power.Level_3
+
+
+Game "NNG"
+World "Power"
+Level 4
+Title "one_pow"
+
+open MyNat
+
+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
+
+LemmaTab "Pow"

NNG/Levels/Power/Level_5.lean

@@ -0,0 +1,20 @@
+import NNG.Levels.Power.Level_4
+
+
+Game "NNG"
+World "Power"
+Level 5
+Title "pow_add"
+
+open MyNat
+
+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"

NNG/Levels/Power/Level_6.lean

@@ -0,0 +1,30 @@
+import NNG.Levels.Power.Level_5
+
+Game "NNG"
+World "Power"
+Level 6
+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 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"

NNG/Levels/Power/Level_7.lean

@@ -0,0 +1,35 @@
+import NNG.Levels.Power.Level_6
+
+Game "NNG"
+World "Power"
+Level 7
+Title "pow_pow"
+
+open MyNat
+
+Introduction
+"
+Boss level! What will the collectible be?
+"
+
+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!
+"

NNG/Levels/Power/Level_8.lean

@@ -0,0 +1,51 @@
+import NNG.Levels.Power.Level_7
+-- import Mathlib.Tactic.Ring
+
+Game "NNG"
+World "Power"
+Level 8
+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 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
+"
+
+"

NNG/Levels/Proposition.lean

@@ -0,0 +1,48 @@
+import NNG.Levels.Proposition.Level_1
+import NNG.Levels.Proposition.Level_2
+import NNG.Levels.Proposition.Level_3
+import NNG.Levels.Proposition.Level_4
+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
+
+
+Game "NNG"
+World "Proposition"
+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.
+"

NNG/Levels/Proposition/Level_1.lean

@@ -0,0 +1,51 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 1
+Title "the `exact` tactic"
+
+open MyNat
+
+Introduction
+"
+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
+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?
+"
+
+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
+*mathematically* to solve this goal, $P$ is true and $P$ implies $Q$
+so $Q$ is true. But how to do it in Lean?
+
+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
+```
+
+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$.
+
+In Lean, Propositions, like sets, are types, and proofs, like elements of sets, are terms.
+"
+exact h p

NNG/Levels/Proposition/Level_2.lean

@@ -0,0 +1,64 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 2
+Title "intro"
+
+open MyNat
+
+Introduction
+"
+Let's prove an implication. Let $P$ be a true/false statement,
+and let's prove that $P\\implies P$. You can see that the goal of this level is
+`P → P`. Constructing a term
+of type `P → P` (which is what solving this goal *means*) in this
+case amounts to proving that $P\\implies P$, and computer scientists
+think of this as coming up with a function which sends proofs of $P$
+to proofs of $P$.
+
+To define an implication $P\\implies Q$ we need to choose an arbitrary
+proof $p : P$ of $P$ and then, perhaps using $p$, construct a proof
+of $Q$.  The Lean way to say \"let's assume $P$ is true\" is `intro p`,
+i.e., \"let's assume we have a proof of $P$\".
+
+## Note for worriers.
+
+Those of you who know
+something about the subtle differences between truth and provability
+discovered by Goedel -- these are not relevant here. Imagine we are
+working in a fixed model of mathematics, and when I say \"proof\"
+I actually mean \"truth in the model\", or \"proof in the metatheory\".
+
+## Rule of thumb: 
+
+If your goal is to prove `P → Q` (i.e. that $P\\implies Q$)
+then `intro p`, meaning \"assume $p$ is a proof of $P$\", will make progress.
+
+"
+
+Statement
+"If $P$ is a proposition then $P\\implies P$."
+    {P : Prop} : P → P := by
+  Hint "
+  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
+  Hint "
+  Our job now is to construct a proof of $P$. But ${p}$ is a proof of $P$.
+  So
+
+  `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.
+  We will stick with the convention of capital letters for propositions
+  and small letters for proofs.
+  "
+  exact p

NNG/Levels/Proposition/Level_3.lean

@@ -0,0 +1,109 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 3
+Title "have"
+
+open MyNat
+
+Introduction
+"
+Say you have a whole bunch of propositions and implications between them,
+and your goal is to build a certain proof of a certain proposition.
+If it helps, you can build intermediate proofs of other propositions
+along the way, using the `have` command. `have q : Q := ...` is the Lean analogue
+of saying \"We now see that we can prove $Q$, because...\"
+in the middle of a proof.
+It is often not logically necessary, but on the other hand
+it is very convenient, for example it can save on notation, or
+it can break proofs up into smaller steps.
+
+In the level below, we have a proof of $P$ and we want a proof
+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:
+
+$$
+\\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$.
+
+"
+
+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
+
+Conclusion
+"
+If you solved the level using `have`, then click on the last line of your proof
+(you do know you can move your cursor around with the arrow keys
+and explore your proof, right?) and note that the local context at that point
+is in something like the following mess:
+
+```
+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
+terms to it. In level 4 we will learn about the `apply` tactic
+which solves the level using another technique, without leaving
+so much junk behind.
+"

NNG/Levels/Proposition/Level_4.lean

@@ -0,0 +1,59 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 4
+Title "apply"
+
+open MyNat
+
+Introduction
+"
+Let's do the same level again:
+
+$$
+\\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$.
+"
+
+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»

NNG/Levels/Proposition/Level_5.lean

@@ -0,0 +1,77 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 5
+Title "P → (Q → P)"
+
+open MyNat
+
+Introduction
+"
+In this level, our goal is to construct an implication, like in level 2.
+
+```
+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.
+"
+
+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
+"
+A mathematician would treat the proposition $P\\implies(Q\\implies P)$
+as the same as the proposition $P\\land Q\\implies P$,
+because to give a proof of either of these is just to give a method which takes
+a proof of $P$ and a proof of $Q$, and returns a proof of $P$. Thinking of the
+goal as $P\\land Q\\implies P$ we see why it is provable.
+
+## Did you notice?
+
+I wrote `P → (Q → P)` but Lean just writes `P → Q → P`. This is because
+computer scientists adopt the convention that `→` is *right associative*,
+which is a fancy way of saying \"when we write `P → Q → R`, we mean `P → (Q → R)`.
+Mathematicians would never dream of writing something as ambiguous as
+$P\\implies Q\\implies R$ (they are not really interested in proving abstract
+propositions, they would rather work with concrete ones such as Fermat's Last Theorem),
+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.
+
+"

NNG/Levels/Proposition/Level_6.lean

@@ -0,0 +1,55 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 6
+Title "(P → (Q → R)) → ((P → Q) → (P → R))"
+
+open MyNat
+
+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`.
+"
+
+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

NNG/Levels/Proposition/Level_7.lean

@@ -0,0 +1,27 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 7
+Title "(P → Q) → ((Q → R) → (P → R))"
+
+open MyNat
+
+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
+  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
+

NNG/Levels/Proposition/Level_8.lean

@@ -0,0 +1,72 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 8
+Title "(P → Q) → (¬ Q → ¬ P)"
+
+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}$.
+
+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
+  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
+
+-- 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 "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."

NNG/Levels/Proposition/Level_9.lean

@@ -0,0 +1,56 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+Game "NNG"
+World "Proposition"
+Level 9
+Title "a big maze."
+
+open MyNat
+
+Introduction
+"
+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."
+    (A B C D E F G H I J K L : Prop)
+    (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 (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.
+"

NNG/Levels/Tutorial.lean

@@ -0,0 +1,15 @@
+import NNG.Levels.Tutorial.Level_1
+import NNG.Levels.Tutorial.Level_2
+import NNG.Levels.Tutorial.Level_3
+import NNG.Levels.Tutorial.Level_4
+
+Game "NNG"
+World "Tutorial"
+Title "Tutorial World"
+
+Introduction
+"
+In this world we start introducing the natural numbers `ℕ` and addition.
+
+Click on \"Next\" to dive right into it!
+"