diff --git a/.gitignore b/.gitignore
index 35a5ade..88be6e5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
 node_modules
 client/dist
 server/build
+server/nng
 **/lake-packages/
-
diff --git a/server/nng/.gitignore b/server/nng/.gitignore
deleted file mode 100644
index 8105d0d..0000000
--- a/server/nng/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-build/
-lake-packages/
diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean
deleted file mode 100644
index 7b7a783..0000000
--- a/server/nng/NNG.lean
+++ /dev/null
@@ -1,64 +0,0 @@
-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
diff --git a/server/nng/NNG/Doc/Definitions.lean b/server/nng/NNG/Doc/Definitions.lean
deleted file mode 100644
index 5cd0730..0000000
--- a/server/nng/NNG/Doc/Definitions.lean
+++ /dev/null
@@ -1,88 +0,0 @@
-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 "≠" ""
\ No newline at end of file
diff --git a/server/nng/NNG/Doc/Lemmas.lean b/server/nng/NNG/Doc/Lemmas.lean
deleted file mode 100644
index e861b84..0000000
--- a/server/nng/NNG/Doc/Lemmas.lean
+++ /dev/null
@@ -1,168 +0,0 @@
-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)"
-
diff --git a/server/nng/NNG/Doc/Tactics.lean b/server/nng/NNG/Doc/Tactics.lean
deleted file mode 100644
index 009fe27..0000000
--- a/server/nng/NNG/Doc/Tactics.lean
+++ /dev/null
@@ -1,186 +0,0 @@
-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»
-"
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Addition.lean b/server/nng/NNG/Levels/Addition.lean
deleted file mode 100644
index 52b5dec..0000000
--- a/server/nng/NNG/Levels/Addition.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-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.
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Addition/Level_1.lean b/server/nng/NNG/Levels/Addition/Level_1.lean
deleted file mode 100644
index 03b7d95..0000000
--- a/server/nng/NNG/Levels/Addition/Level_1.lean
+++ /dev/null
@@ -1,95 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/Addition/Level_2.lean b/server/nng/NNG/Levels/Addition/Level_2.lean
deleted file mode 100644
index 0018018..0000000
--- a/server/nng/NNG/Levels/Addition/Level_2.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Addition/Level_3.lean b/server/nng/NNG/Levels/Addition/Level_3.lean
deleted file mode 100644
index a8329ce..0000000
--- a/server/nng/NNG/Levels/Addition/Level_3.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Addition/Level_4.lean b/server/nng/NNG/Levels/Addition/Level_4.lean
deleted file mode 100644
index 8a9ad42..0000000
--- a/server/nng/NNG/Levels/Addition/Level_4.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/Addition/Level_5.lean b/server/nng/NNG/Levels/Addition/Level_5.lean
deleted file mode 100644
index 3367aaf..0000000
--- a/server/nng/NNG/Levels/Addition/Level_5.lean
+++ /dev/null
@@ -1,43 +0,0 @@
-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!
-"
diff --git a/server/nng/NNG/Levels/Addition/Level_6.lean b/server/nng/NNG/Levels/Addition/Level_6.lean
deleted file mode 100644
index 70fdb5c..0000000
--- a/server/nng/NNG/Levels/Addition/Level_6.lean
+++ /dev/null
@@ -1,114 +0,0 @@
-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
diff --git a/server/nng/NNG/Levels/AdvAddition.lean b/server/nng/NNG/Levels/AdvAddition.lean
deleted file mode 100644
index 6be2f2b..0000000
--- a/server/nng/NNG/Levels/AdvAddition.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-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.
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_1.lean b/server/nng/NNG/Levels/AdvAddition/Level_1.lean
deleted file mode 100644
index e1aee09..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_1.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_10.lean b/server/nng/NNG/Levels/AdvAddition/Level_10.lean
deleted file mode 100644
index 8e92bb8..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_10.lean
+++ /dev/null
@@ -1,77 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_11.lean b/server/nng/NNG/Levels/AdvAddition/Level_11.lean
deleted file mode 100644
index ffde445..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_11.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_12.lean b/server/nng/NNG/Levels/AdvAddition/Level_12.lean
deleted file mode 100644
index 8995e0f..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_12.lean
+++ /dev/null
@@ -1,34 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_13.lean b/server/nng/NNG/Levels/AdvAddition/Level_13.lean
deleted file mode 100644
index d664492..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_13.lean
+++ /dev/null
@@ -1,38 +0,0 @@
-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).
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_2.lean b/server/nng/NNG/Levels/AdvAddition/Level_2.lean
deleted file mode 100644
index 97937fd..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_2.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-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)
-```
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_3.lean b/server/nng/NNG/Levels/AdvAddition/Level_3.lean
deleted file mode 100644
index 2ed3998..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_3.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_4.lean b/server/nng/NNG/Levels/AdvAddition/Level_4.lean
deleted file mode 100644
index 42e3afd..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_4.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_5.lean b/server/nng/NNG/Levels/AdvAddition/Level_5.lean
deleted file mode 100644
index 98b09b3..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_5.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_6.lean b/server/nng/NNG/Levels/AdvAddition/Level_6.lean
deleted file mode 100644
index 3004e97..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_6.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_7.lean b/server/nng/NNG/Levels/AdvAddition/Level_7.lean
deleted file mode 100644
index 15d1c7d..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_7.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-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"
-
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_8.lean b/server/nng/NNG/Levels/AdvAddition/Level_8.lean
deleted file mode 100644
index 53d0cee..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_8.lean
+++ /dev/null
@@ -1,34 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvAddition/Level_9.lean b/server/nng/NNG/Levels/AdvAddition/Level_9.lean
deleted file mode 100644
index 1dd69d2..0000000
--- a/server/nng/NNG/Levels/AdvAddition/Level_9.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvMultiplication.lean b/server/nng/NNG/Levels/AdvMultiplication.lean
deleted file mode 100644
index b13e064..0000000
--- a/server/nng/NNG/Levels/AdvMultiplication.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-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.
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean
deleted file mode 100644
index 0f87b1c..0000000
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean
deleted file mode 100644
index 5f0c945..0000000
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean
+++ /dev/null
@@ -1,33 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean
deleted file mode 100644
index 42bca60..0000000
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean
deleted file mode 100644
index edf732d..0000000
--- a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean
+++ /dev/null
@@ -1,99 +0,0 @@
-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
-"
-
-"
-
-
diff --git a/server/nng/NNG/Levels/AdvProposition.lean b/server/nng/NNG/Levels/AdvProposition.lean
deleted file mode 100644
index f9a2e46..0000000
--- a/server/nng/NNG/Levels/AdvProposition.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-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.
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_1.lean b/server/nng/NNG/Levels/AdvProposition/Level_1.lean
deleted file mode 100644
index 3dd7aa0..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_1.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-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
-"
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_10.lean b/server/nng/NNG/Levels/AdvProposition/Level_10.lean
deleted file mode 100644
index f543a3c..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_10.lean
+++ /dev/null
@@ -1,65 +0,0 @@
-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.
-
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_2.lean b/server/nng/NNG/Levels/AdvProposition/Level_2.lean
deleted file mode 100644
index 105b5b3..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_2.lean
+++ /dev/null
@@ -1,49 +0,0 @@
-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
-
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_3.lean b/server/nng/NNG/Levels/AdvProposition/Level_3.lean
deleted file mode 100644
index bf03cd1..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_3.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_4.lean b/server/nng/NNG/Levels/AdvProposition/Level_4.lean
deleted file mode 100644
index 6e8d07f..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_4.lean
+++ /dev/null
@@ -1,45 +0,0 @@
-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
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_5.lean b/server/nng/NNG/Levels/AdvProposition/Level_5.lean
deleted file mode 100644
index fbedbc5..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_5.lean
+++ /dev/null
@@ -1,76 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_6.lean b/server/nng/NNG/Levels/AdvProposition/Level_6.lean
deleted file mode 100644
index 0a7123a..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_6.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-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
-
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_7.lean b/server/nng/NNG/Levels/AdvProposition/Level_7.lean
deleted file mode 100644
index adca207..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_7.lean
+++ /dev/null
@@ -1,55 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_8.lean b/server/nng/NNG/Levels/AdvProposition/Level_8.lean
deleted file mode 100644
index b9e9a83..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_8.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/AdvProposition/Level_9.lean b/server/nng/NNG/Levels/AdvProposition/Level_9.lean
deleted file mode 100644
index d2c2e29..0000000
--- a/server/nng/NNG/Levels/AdvProposition/Level_9.lean
+++ /dev/null
@@ -1,52 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Function.lean b/server/nng/NNG/Levels/Function.lean
deleted file mode 100644
index 5556be2..0000000
--- a/server/nng/NNG/Levels/Function.lean
+++ /dev/null
@@ -1,41 +0,0 @@
-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 &ndash; 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 &ndash;
-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 &ndash; Lean has
-been writing `n : ℕ` to mean that $n$ is a natural number.
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Function/Level_1.lean b/server/nng/NNG/Levels/Function/Level_1.lean
deleted file mode 100644
index bfef063..0000000
--- a/server/nng/NNG/Levels/Function/Level_1.lean
+++ /dev/null
@@ -1,72 +0,0 @@
-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 &ndash; 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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Function/Level_2.lean b/server/nng/NNG/Levels/Function/Level_2.lean
deleted file mode 100644
index 20b4e7a..0000000
--- a/server/nng/NNG/Levels/Function/Level_2.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/Function/Level_3.lean b/server/nng/NNG/Levels/Function/Level_3.lean
deleted file mode 100644
index d637942..0000000
--- a/server/nng/NNG/Levels/Function/Level_3.lean
+++ /dev/null
@@ -1,93 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/Function/Level_4.lean b/server/nng/NNG/Levels/Function/Level_4.lean
deleted file mode 100644
index 37015d1..0000000
--- a/server/nng/NNG/Levels/Function/Level_4.lean
+++ /dev/null
@@ -1,64 +0,0 @@
-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»
diff --git a/server/nng/NNG/Levels/Function/Level_5.lean b/server/nng/NNG/Levels/Function/Level_5.lean
deleted file mode 100644
index 8ef30f7..0000000
--- a/server/nng/NNG/Levels/Function/Level_5.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Function/Level_6.lean b/server/nng/NNG/Levels/Function/Level_6.lean
deleted file mode 100644
index f0848f8..0000000
--- a/server/nng/NNG/Levels/Function/Level_6.lean
+++ /dev/null
@@ -1,65 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Function/Level_7.lean b/server/nng/NNG/Levels/Function/Level_7.lean
deleted file mode 100644
index de8f1f4..0000000
--- a/server/nng/NNG/Levels/Function/Level_7.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Function/Level_8.lean b/server/nng/NNG/Levels/Function/Level_8.lean
deleted file mode 100644
index 0ee4864..0000000
--- a/server/nng/NNG/Levels/Function/Level_8.lean
+++ /dev/null
@@ -1,49 +0,0 @@
-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 ""
diff --git a/server/nng/NNG/Levels/Function/Level_9.lean b/server/nng/NNG/Levels/Function/Level_9.lean
deleted file mode 100644
index 7545c65..0000000
--- a/server/nng/NNG/Levels/Function/Level_9.lean
+++ /dev/null
@@ -1,43 +0,0 @@
-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$.
-"
diff --git a/server/nng/NNG/Levels/Inequality.lean b/server/nng/NNG/Levels/Inequality.lean
deleted file mode 100644
index 8f5ce6f..0000000
--- a/server/nng/NNG/Levels/Inequality.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-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, ...`. 
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Inequality/Level_1.lean b/server/nng/NNG/Levels/Inequality/Level_1.lean
deleted file mode 100644
index 5779955..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_1.lean
+++ /dev/null
@@ -1,62 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_10.lean b/server/nng/NNG/Levels/Inequality/Level_10.lean
deleted file mode 100644
index f2441f8..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_10.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_11.lean b/server/nng/NNG/Levels/Inequality/Level_11.lean
deleted file mode 100644
index 95252b5..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_11.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_12.lean b/server/nng/NNG/Levels/Inequality/Level_12.lean
deleted file mode 100644
index 7bccf47..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_12.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_13.lean b/server/nng/NNG/Levels/Inequality/Level_13.lean
deleted file mode 100644
index 501a5ca..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_13.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_14.lean b/server/nng/NNG/Levels/Inequality/Level_14.lean
deleted file mode 100644
index 28edd11..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_14.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_15.lean b/server/nng/NNG/Levels/Inequality/Level_15.lean
deleted file mode 100644
index b05b988..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_15.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_16.lean b/server/nng/NNG/Levels/Inequality/Level_16.lean
deleted file mode 100644
index 1cc96a6..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_16.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_17.lean b/server/nng/NNG/Levels/Inequality/Level_17.lean
deleted file mode 100644
index 3dfc86e..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_17.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_2.lean b/server/nng/NNG/Levels/Inequality/Level_2.lean
deleted file mode 100644
index bcee184..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_2.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_3.lean b/server/nng/NNG/Levels/Inequality/Level_3.lean
deleted file mode 100644
index 32adff5..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_3.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_4.lean b/server/nng/NNG/Levels/Inequality/Level_4.lean
deleted file mode 100644
index a3a34cb..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_4.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_5.lean b/server/nng/NNG/Levels/Inequality/Level_5.lean
deleted file mode 100644
index 59159c1..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_5.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_6.lean b/server/nng/NNG/Levels/Inequality/Level_6.lean
deleted file mode 100644
index 86f83a1..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_6.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_7.lean b/server/nng/NNG/Levels/Inequality/Level_7.lean
deleted file mode 100644
index 8ff4d8d..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_7.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_8.lean b/server/nng/NNG/Levels/Inequality/Level_8.lean
deleted file mode 100644
index 4d6f744..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_8.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Inequality/Level_9.lean b/server/nng/NNG/Levels/Inequality/Level_9.lean
deleted file mode 100644
index 185f626..0000000
--- a/server/nng/NNG/Levels/Inequality/Level_9.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Multiplication.lean b/server/nng/NNG/Levels/Multiplication.lean
deleted file mode 100644
index 023734f..0000000
--- a/server/nng/NNG/Levels/Multiplication.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-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!
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Multiplication/Level_1.lean b/server/nng/NNG/Levels/Multiplication/Level_1.lean
deleted file mode 100644
index 8b4184b..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_1.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_2.lean b/server/nng/NNG/Levels/Multiplication/Level_2.lean
deleted file mode 100644
index 3068a30..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_2.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_3.lean b/server/nng/NNG/Levels/Multiplication/Level_3.lean
deleted file mode 100644
index 8501ef9..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_3.lean
+++ /dev/null
@@ -1,38 +0,0 @@
-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 ""
diff --git a/server/nng/NNG/Levels/Multiplication/Level_4.lean b/server/nng/NNG/Levels/Multiplication/Level_4.lean
deleted file mode 100644
index 37cb86c..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_4.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-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"
-
diff --git a/server/nng/NNG/Levels/Multiplication/Level_5.lean b/server/nng/NNG/Levels/Multiplication/Level_5.lean
deleted file mode 100644
index 518218a..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_5.lean
+++ /dev/null
@@ -1,43 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_6.lean b/server/nng/NNG/Levels/Multiplication/Level_6.lean
deleted file mode 100644
index 900fedb..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_6.lean
+++ /dev/null
@@ -1,52 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_7.lean b/server/nng/NNG/Levels/Multiplication/Level_7.lean
deleted file mode 100644
index 9a242d6..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_7.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Multiplication/Level_8.lean b/server/nng/NNG/Levels/Multiplication/Level_8.lean
deleted file mode 100644
index 08dcdfd..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_8.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-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
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Multiplication/Level_9.lean b/server/nng/NNG/Levels/Multiplication/Level_9.lean
deleted file mode 100644
index e1fc48a..0000000
--- a/server/nng/NNG/Levels/Multiplication/Level_9.lean
+++ /dev/null
@@ -1,57 +0,0 @@
-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\".
-"
diff --git a/server/nng/NNG/Levels/Power.lean b/server/nng/NNG/Levels/Power.lean
deleted file mode 100644
index fb37bdb..0000000
--- a/server/nng/NNG/Levels/Power.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-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!
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Power/Level_1.lean b/server/nng/NNG/Levels/Power/Level_1.lean
deleted file mode 100644
index b6e0688..0000000
--- a/server/nng/NNG/Levels/Power/Level_1.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Power/Level_2.lean b/server/nng/NNG/Levels/Power/Level_2.lean
deleted file mode 100644
index cf4b1ba..0000000
--- a/server/nng/NNG/Levels/Power/Level_2.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Power/Level_3.lean b/server/nng/NNG/Levels/Power/Level_3.lean
deleted file mode 100644
index ee44e4c..0000000
--- a/server/nng/NNG/Levels/Power/Level_3.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Power/Level_4.lean b/server/nng/NNG/Levels/Power/Level_4.lean
deleted file mode 100644
index 0bde842..0000000
--- a/server/nng/NNG/Levels/Power/Level_4.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Power/Level_5.lean b/server/nng/NNG/Levels/Power/Level_5.lean
deleted file mode 100644
index 750e4d2..0000000
--- a/server/nng/NNG/Levels/Power/Level_5.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Power/Level_6.lean b/server/nng/NNG/Levels/Power/Level_6.lean
deleted file mode 100644
index fa5d3d8..0000000
--- a/server/nng/NNG/Levels/Power/Level_6.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-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"
diff --git a/server/nng/NNG/Levels/Power/Level_7.lean b/server/nng/NNG/Levels/Power/Level_7.lean
deleted file mode 100644
index 1a14059..0000000
--- a/server/nng/NNG/Levels/Power/Level_7.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-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!
-"
diff --git a/server/nng/NNG/Levels/Power/Level_8.lean b/server/nng/NNG/Levels/Power/Level_8.lean
deleted file mode 100644
index 2bc3d20..0000000
--- a/server/nng/NNG/Levels/Power/Level_8.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-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
-"
-
-"
diff --git a/server/nng/NNG/Levels/Proposition.lean b/server/nng/NNG/Levels/Proposition.lean
deleted file mode 100644
index 5a05778..0000000
--- a/server/nng/NNG/Levels/Proposition.lean
+++ /dev/null
@@ -1,48 +0,0 @@
-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.
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Proposition/Level_1.lean b/server/nng/NNG/Levels/Proposition/Level_1.lean
deleted file mode 100644
index b5eb3fc..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_1.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-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
diff --git a/server/nng/NNG/Levels/Proposition/Level_2.lean b/server/nng/NNG/Levels/Proposition/Level_2.lean
deleted file mode 100644
index 7bf92e7..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_2.lean
+++ /dev/null
@@ -1,64 +0,0 @@
-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
diff --git a/server/nng/NNG/Levels/Proposition/Level_3.lean b/server/nng/NNG/Levels/Proposition/Level_3.lean
deleted file mode 100644
index 33071af..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_3.lean
+++ /dev/null
@@ -1,109 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/Proposition/Level_4.lean b/server/nng/NNG/Levels/Proposition/Level_4.lean
deleted file mode 100644
index d5b2469..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_4.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-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»
diff --git a/server/nng/NNG/Levels/Proposition/Level_5.lean b/server/nng/NNG/Levels/Proposition/Level_5.lean
deleted file mode 100644
index 0ca2569..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_5.lean
+++ /dev/null
@@ -1,77 +0,0 @@
-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.
-
-"
diff --git a/server/nng/NNG/Levels/Proposition/Level_6.lean b/server/nng/NNG/Levels/Proposition/Level_6.lean
deleted file mode 100644
index e90f73c..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_6.lean
+++ /dev/null
@@ -1,55 +0,0 @@
-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
diff --git a/server/nng/NNG/Levels/Proposition/Level_7.lean b/server/nng/NNG/Levels/Proposition/Level_7.lean
deleted file mode 100644
index 4805f06..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_7.lean
+++ /dev/null
@@ -1,27 +0,0 @@
-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
-
diff --git a/server/nng/NNG/Levels/Proposition/Level_8.lean b/server/nng/NNG/Levels/Proposition/Level_8.lean
deleted file mode 100644
index 29c7fb8..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_8.lean
+++ /dev/null
@@ -1,72 +0,0 @@
-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."
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Proposition/Level_9.lean b/server/nng/NNG/Levels/Proposition/Level_9.lean
deleted file mode 100644
index 4e95741..0000000
--- a/server/nng/NNG/Levels/Proposition/Level_9.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-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.
-"
diff --git a/server/nng/NNG/Levels/Tutorial.lean b/server/nng/NNG/Levels/Tutorial.lean
deleted file mode 100644
index 9efc7d0..0000000
--- a/server/nng/NNG/Levels/Tutorial.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-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!
-"
\ No newline at end of file
diff --git a/server/nng/NNG/Levels/Tutorial/Level_1.lean b/server/nng/NNG/Levels/Tutorial/Level_1.lean
deleted file mode 100644
index ca79fcc..0000000
--- a/server/nng/NNG/Levels/Tutorial/Level_1.lean
+++ /dev/null
@@ -1,42 +0,0 @@
-import NNG.Metadata
-import NNG.MyNat.Multiplication
-
-Game "NNG"
-World "Tutorial"
-Level 1
-Title "The rfl tactic"
-
-Introduction
-"
-Each level in this game involves proving a mathematical statement. In this first level
-you have three natural numbers $x, y, z$ (listed under \"Objects\") and you want to prove
-$xy + z = xy + z$ (displayed under \"Goal\").
-
-You can modify the Goal using *Tactics* until you can close it (i.e. prove it).
-
-The first tactic is called `rfl`, which stands for \"reflexivity\",
-a fancy way of saying that it will prove any goal of the form `A = A`. It doesn't matter how
-complicated `A` is, all that matters is that the left hand side is exactly equal to the right hand
-side. I really mean \"press the same buttons
-on your computer in the same order\" equal. For example, `x * y + z = x * y + z` can be proved by `rfl`,
-but `x + y = y + x` cannot.
-"
-
-Statement
-"For all natural numbers $x, y$ and $z$, we have $xy + z = xy + z$."
-    (x y z : ℕ) : x * y + z = x * y + z := by
-  Hint "In order to use the tactic `rfl` you can enter it above and hit \"Execute\"."
-  rfl
-
-NewTactic rfl simp -- TODO
-NewDefinition MyNat
-
-Conclusion
-"
-Congratulations! You completed your first verified proof!
-
-If you want to be reminded about the `rfl` tactic, your inventory on the right contains useful
-information about things you've learned.
-
-Now click on \"Next\" to continue the journey.
-"
diff --git a/server/nng/NNG/Levels/Tutorial/Level_2.lean b/server/nng/NNG/Levels/Tutorial/Level_2.lean
deleted file mode 100644
index b4992c1..0000000
--- a/server/nng/NNG/Levels/Tutorial/Level_2.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-import NNG.Metadata
-import NNG.MyNat.Multiplication
-
-Game "NNG"
-World "Tutorial"
-Level 2
-Title "the rw tactic"
-
-Introduction
-"
-In this level, you also get \"Assumptions\" about your objects. These are hypotheses of which
-you assume (or know) that they are true.
-
-The \"rewrite\" tactic `rw` is the way to \"substitute in\" the value of a variable.
-If you have a hypothesis of the form `A = B`, and your goal mentions
-the left hand side `A` somewhere,
-then the rewrite tactic will replace the `A` in your goal with a `B`.
-Here is a theorem which cannot be proved using rfl -- you need a rewrite first.
-"
-
-Statement
-"If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$."
-    (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
-  Hint "You can use `rw [h]` to replace the `{y}` with `x + 7`.
-  Note that the assumption `h` is written
-  inside square brackets: `[h]`."
-  rw [h]
-  Hint "Not all hints are directly shown. If you are stuck and need more help
-  finishing the proof, click on \"More Help\" below!"
-  Hint (hidden := true)
-  "Now both sides are identical, so you can use `rfl` to close the goal."
-  rfl
-
-NewTactic rw
-
-Conclusion
-"
-If you want to inspect the proof you created, toggle \"Editor mode\" above.
-
-There you can also move your cursor around the proof to see the \"state\" of the proof at this point.
-
-Each tactic is written on a new line and Lean is sensitive to indentation (i.e. there must be no
-spaces before any of the tactics)
-"
diff --git a/server/nng/NNG/Levels/Tutorial/Level_3.lean b/server/nng/NNG/Levels/Tutorial/Level_3.lean
deleted file mode 100644
index d3f426c..0000000
--- a/server/nng/NNG/Levels/Tutorial/Level_3.lean
+++ /dev/null
@@ -1,73 +0,0 @@
-import NNG.Metadata
-import NNG.MyNat.Definition
-
-Game "NNG"
-World "Tutorial"
-Level 3
-Title "Peano axioms"
-
-open MyNat
-
-Introduction
-"
-Now we start from the beginning, where we don't know about addition or multiplication on `ℕ`.
-
-All we get is the following data:
-
-* a term `(0 : ℕ)`, interpreted as the zero number.
-* a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after $n$\".
-* the principle of mathematical induction.
-
-These axioms are essentially the axioms isolated by Peano which uniquely characterise the natural
-numbers (we also need recursion, but we can ignore it for now).
-The first axiom says that $0$ is a natural number.
-The second says that there is a $\\operatorname{succ}$ function which eats a number and spits out
-the number after it, so $\\operatorname{succ}(0)=1$, $\\operatorname{succ}(1)=2$ and so on.
-
-Peano's last axiom is the principle of mathematical induction. This is a deeper fact.
-It says that if we have infinitely many true/false statements $P(0)$, $P(1)$, $P(2)$ and so on,
-and if $P(0)$ is true, and if for every natural number $d$ we know that $P(d)$ implies
-$P(\\operatorname{succ}(d))$, then $P(n)$ must be true for every natural number $n$.
-It's like saying that if you have a long line of dominoes, and if you knock the first
-one down, and if you know that if a domino falls down then the one after it will fall
-down too, then you can deduce that all the dominos will fall down. One can also think
-of it as saying that every natural number can be built by starting at $0$ and then applying
-$\\operatorname{succ}$ a finite number of times.
-
-Peano's insights were firstly that these axioms completely characterise the natural numbers,
-and secondly that these axioms alone can be used to build a whole bunch of other structure
-on the natural numbers, for example addition, multiplication and so on.
-
-This game is all about seeing how far these axioms of Peano can take us.
-
-Now let us practise the use of `rw` with this new function `succ`:
-"
-
-Statement
-"If $\\operatorname{succ}(a) = b$, then $\\operatorname{succ}(\\operatorname{succ}(a)) = \\operatorname{succ}(a)$."
-    (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
-  Hint "You can use `rw` and your assumption `{h}` to substitute `succ a` with `b`.
-
-  Notes:
-
-  1) We do not need brackets for function application the way we would write
-  them in mathematics: `succ b` means $\\operatorname\{succ}(b)$.
-  2) If you would want to substitute instead `b` with `succ a`, you can do that
-  writing a small `←` (`\\l`, i.e. backslash + small letter L + space)
-  before `h` like this: `rw [← h]`."
-  Branch
-    simp? -- TODO: `simp` should not make progress.
-  Branch
-    rw [← h]
-    Hint (hidden := true) "Now both sides are identical…"
-  rw [h]
-  Hint (hidden := true) "Now both sides are identical…"
-  rfl
-
-Conclusion
-"
-You may also be wondering why we keep writing `succ b` instead of `b + 1`.
-This is because we haven't defined addition yet!
-On the next level, the final level of Tutorial World,
-we will introduce addition, and then we'll be ready to enter Addition World.
-"
diff --git a/server/nng/NNG/Levels/Tutorial/Level_4.lean b/server/nng/NNG/Levels/Tutorial/Level_4.lean
deleted file mode 100644
index ac6cca1..0000000
--- a/server/nng/NNG/Levels/Tutorial/Level_4.lean
+++ /dev/null
@@ -1,71 +0,0 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
-
-Game "NNG"
-World "Tutorial"
-Level 4
-Title "addition"
-
-open MyNat
-
-Introduction
-"
-Peano defined addition $a + b$ by induction on $b$, or, more precisely, by *recursion* on $b$.
-He first explained how to add $0$ to a number: this is the base case.
-
-* `add_zero (a : ℕ) : a + 0 = a`
-
-We will call this theorem `add_zero`.
-More precisely, `add_zero` is the name of the *proof* of the
-theorem. Note the name of this proof. Mathematicians sometimes call it
-\"Lemma 2.1\" or \"Hypothesis P6\" or something.
-But computer scientists call it `add_zero` because it tells you what the answer to
-\"x add zero\" is. It's a much better name than \"Lemma 2.1\".
-Even better, you can use the `rw` tactic
-with `add_zero`. If you ever see `x + 0` in your goal,
-`rw [add_zero]` should simplify it to `x`. This is
-because `add_zero` is a proof that `x + 0 = x`
-(more precisely, `add_zero x` is a proof that `x + 0 = x` but
-Lean can figure out the `x` from the context).
-
-Now here's the inductive step. If you know how to add $d$ to $a$, then Peano
-tells you how to add $\\operatorname{succ} (d)$ to $a$. It looks like this:
-
-- `add_succ (a d : ℕ) : a + (succ d) = succ (a + d)`
-
-What's going on here is that we assume `a + d` is already defined, and we define
-`a + (succ d)` to be the number after it.
-Note the name of this proof too: `add_succ` tells you how to add a successor
-to something.
-If you ever see `… + succ …` in your goal, you should be able to use
-`rw [add_succ]` to make progress.
-"
-
-Statement
-"For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = \\operatorname{succ}(a)$."
-    (a : ℕ) : a + succ 0 = succ a := by
-  Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
-  to make progress."
-  Hint (hidden := true) "Explicitely, type `rw [add_succ]`!"
-  rw [add_succ]
-  Hint "Now you see a term of the form `… + 0`, so you can use `add_zero`."
-  Hint (hidden := true) "Explicitely, type `rw [add_zero]`!"
-  Branch
-    simp? -- TODO
-  rw [add_zero]
-  Hint (hidden := true) "Finally both sides are identical."
-  rfl
-
-NewLemma MyNat.add_succ MyNat.add_zero
-NewDefinition Add
-
-Conclusion
-"
-You have finished tutorial world! If you're happy, let's move onto Addition World,
-and learn about proof by induction.
-
-## Inspection time
-
-If you want to examine the proof, toggle \"Editor mode\" and click somewhere
-inside the proof to see the state at that point!
-"
diff --git a/server/nng/NNG/Metadata.lean b/server/nng/NNG/Metadata.lean
deleted file mode 100644
index a7a450a..0000000
--- a/server/nng/NNG/Metadata.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import GameServer.Commands
-
-import NNG.MyNat.Definition
-
-import NNG.Doc.Definitions
-import NNG.Doc.Lemmas
-import NNG.Doc.Tactics
-
-import NNG.Tactic.Induction
-import NNG.Tactic.Rfl
-import NNG.Tactic.Rw
-import Std.Tactic.RCases
-import Mathlib.Tactic.Have
-import Mathlib.Tactic.LeftRight
-
--- TODO: Why does this not work here??
--- We do not want `simp` to be able to do anything unless we unlock it manually.
-attribute [-simp] MyNat.succ.injEq
\ No newline at end of file
diff --git a/server/nng/NNG/MyNat/AddCommMonoid.lean b/server/nng/NNG/MyNat/AddCommMonoid.lean
deleted file mode 100644
index c296225..0000000
--- a/server/nng/NNG/MyNat/AddCommMonoid.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
-
-namespace MyNat
-
--- TODO: Do we need these instances?
--- (kmb) I wanted to introduce these instances as "collectibles" as
--- one went through the "main route" from addition world to power
--- world. If you could make some extra window with those collectibles
--- in, and whenever you have an instance sorry-free it awards you
--- the collectible, that would be great! These things were just
--- precisely the oddball (to my eyes) classes which nat was an instance of,
--- but I think they would make great collectibles.
-
--- instance addSemigroup : AddSemigroup ℕ :=
--- {
---   zero := 0
-
--- }
--- MyNat.addMonoid        -- (after level 2)
--- MyNat.addCommSemigroup -- (after level 4)
--- MyNat.addCommMonoid    -- (after level 4)
diff --git a/server/nng/NNG/MyNat/Addition.lean b/server/nng/NNG/MyNat/Addition.lean
deleted file mode 100644
index a16c40b..0000000
--- a/server/nng/NNG/MyNat/Addition.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-import NNG.MyNat.Definition
-
-namespace MyNat
-
-open MyNat
-
-def add : MyNat → MyNat → MyNat
-  | a, 0   => a
-  | a, MyNat.succ b => MyNat.succ (MyNat.add a b)
-
-instance : Add MyNat where
-  add := MyNat.add
-
-/--
-This theorem proves that if you add zero to a MyNat you get back the same number.
--/
-theorem add_zero (a : MyNat) : a + 0 = a := by rfl
-
-/--
-This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat.
--/
-theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
diff --git a/server/nng/NNG/MyNat/AdvAddition.lean b/server/nng/NNG/MyNat/AdvAddition.lean
deleted file mode 100644
index 661425b..0000000
--- a/server/nng/NNG/MyNat/AdvAddition.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import NNG.MyNat.Addition
-
-namespace MyNat
-
-attribute [-simp] MyNat.succ.injEq
-example (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
-  simp
-  sorry
-
-axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
-
-axiom zero_ne_succ (a : ℕ) : 0 ≠ succ a
-
-
diff --git a/server/nng/NNG/MyNat/Definition.lean b/server/nng/NNG/MyNat/Definition.lean
deleted file mode 100644
index bd68ddf..0000000
--- a/server/nng/NNG/MyNat/Definition.lean
+++ /dev/null
@@ -1,38 +0,0 @@
-/-- Our copy of the natural numbers called `MyNat`. -/
-inductive MyNat where
-| zero : MyNat
-| succ : MyNat → MyNat
--- deriving BEq, DecidableEq, Inhabited
-
-@[inherit_doc]
-notation "ℕ" => MyNat
--- Note: as long as we do not import `Mathlib.Init.Data.Nat.Notation` this is fine.
-
-namespace MyNat
-
-instance : Inhabited MyNat where
-  default := MyNat.zero
-
-def myNatFromNat (x : Nat) : MyNat :=
-  match x with
-  | Nat.zero   => MyNat.zero
-  | Nat.succ b => MyNat.succ (myNatFromNat b)
-
-def natFromMyNat (x : MyNat) : Nat :=
-  match x with
-  | MyNat.zero   => Nat.zero
-  | MyNat.succ b => Nat.succ (natFromMyNat b)
-
-instance ofNat {n : Nat} : OfNat MyNat n where
-  ofNat := myNatFromNat n
-
-instance : ToString MyNat where
-  toString p := toString (natFromMyNat p)
-
-theorem zero_eq_0 : MyNat.zero = 0 := rfl
-
-def one : MyNat := MyNat.succ 0
-
--- TODO: Why does this not work here??
--- We do not want `simp` to be able to do anything unless we unlock it manually.
-attribute [-simp] MyNat.succ.injEq
diff --git a/server/nng/NNG/MyNat/Inequality.lean b/server/nng/NNG/MyNat/Inequality.lean
deleted file mode 100644
index 1fb0956..0000000
--- a/server/nng/NNG/MyNat/Inequality.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-import NNG.MyNat.Multiplication
-
--- this is one of *three* routes to
--- canonically_ordered_comm_semiring
-
-namespace MyNat
-
-def le (a b : MyNat) :=  ∃ (c : MyNat), b = a + c
-
--- Another choice is to define it recursively:
--- | le 0 _
--- | le (succ a) (succ b) = le ab
-
--- notation
-instance : LE MyNat := ⟨MyNat.le⟩
-
-theorem le_def' : MyNat.le = (.≤.) := rfl
-
-theorem le_iff_exists_add (a b : MyNat) : a ≤ b ↔ ∃ (c : MyNat), b = a + c := Iff.rfl
-
-def lt_myNat (a b : MyNat) := a ≤ b ∧ ¬ (b ≤ a)
-
-instance : LT MyNat := ⟨lt_myNat⟩
-
-theorem lt :  ∀ (a b : MyNat), a < b ↔ a ≤ b ∧ ¬b ≤ a := fun _ _ => Iff.rfl
-
-
-end MyNat
\ No newline at end of file
diff --git a/server/nng/NNG/MyNat/LE.lean b/server/nng/NNG/MyNat/LE.lean
deleted file mode 100644
index 26fca08..0000000
--- a/server/nng/NNG/MyNat/LE.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-import NNG.MyNat.Multiplication
-
-namespace MyNat
-
-def le (a b : ℕ) :=  ∃ (c : ℕ), b = a + c
-
--- Another choice is to define it recursively:
--- (kb) note: I didn't choose this option because tests showed
--- that mathematicians found it a lot more confusing than
--- the existence definition.
-
--- | le 0 _
--- | le (succ a) (succ b) = le ab
-
--- notation
-instance : LE MyNat := ⟨MyNat.le⟩
-
---@[leakage] theorem le_def' : MyNat.le = (≤) := rfl
-
-theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c := Iff.rfl
-
-end MyNat
diff --git a/server/nng/NNG/MyNat/Multiplication.lean b/server/nng/NNG/MyNat/Multiplication.lean
deleted file mode 100644
index 4444615..0000000
--- a/server/nng/NNG/MyNat/Multiplication.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import NNG.MyNat.Addition
-
-namespace MyNat
-
-open MyNat
-
-def mul : MyNat → MyNat → MyNat
-  | _, 0   => 0
-  | a, b + 1 => a + (MyNat.mul a b)
-
-instance : Mul MyNat where
-  mul := MyNat.mul
-
-axiom mul_zero (a : MyNat) : a * 0 = 0
-
-axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a
diff --git a/server/nng/NNG/MyNat/Power.lean b/server/nng/NNG/MyNat/Power.lean
deleted file mode 100644
index 6585962..0000000
--- a/server/nng/NNG/MyNat/Power.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import NNG.MyNat.Multiplication
-
-namespace MyNat
-open MyNat
-
-def pow : ℕ → ℕ → ℕ
-| _, zero => one
-| m, (succ n) => pow m n * m
-
-instance : Pow ℕ ℕ where
-  pow := pow
-
--- notation a ^ b := pow a b
-
--- Important note: This here is the real `rfl`, not the weaker game version
-
-example : (1 : ℕ) ^ 1 = 1 := by rfl
-
-theorem pow_zero (m : ℕ) : m ^ 0 = 1 := by rfl
-
-theorem pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := by rfl
-
-def two_eq_succ_one : (2 : ℕ) = succ 1 := by rfl
-
-end MyNat
-
diff --git a/server/nng/NNG/Tactic/Induction.lean b/server/nng/NNG/Tactic/Induction.lean
deleted file mode 100644
index 2f244c2..0000000
--- a/server/nng/NNG/Tactic/Induction.lean
+++ /dev/null
@@ -1,82 +0,0 @@
-import Mathlib.Lean.Expr.Basic
-import Lean.Elab.Tactic.Basic
-import NNG.MyNat.Definition
-
-namespace MyNat
-
-/-!
-# Modified `induction` tactic
-
-Modify `induction` tactic to always show `(0 : MyNat)` instead of `MyNat.zero` and
-to support the lean3-style `with` keyword.
-
-This is mainly copied and modified from the mathlib-tactic `induction'`.
--/
-
-def rec' {P : ℕ → Prop} (zero : P 0)
-    (succ : (n : ℕ) → (n_ih : P n) → P (succ n)) (t : ℕ) : P t := by
-  induction t with
-  | zero => assumption
-  | succ n =>
-    apply succ
-    assumption
-
-end MyNat
-
-namespace Lean.Parser.Tactic
-open Meta Elab Elab.Tactic
-
-open private getAltNumFields in evalCases ElimApp.evalAlts.go in
-def ElimApp.evalNames.MyNat (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax)
-    (numEqs := 0) (numGeneralized := 0) (toClear : Array FVarId := #[]) :
-    TermElabM (Array MVarId) := do
-  let mut names : List Syntax := withArg[1].getArgs |>.toList
-  let mut subgoals := #[]
-  for { name := altName, mvarId := g, .. } in alts do
-    let numFields ← getAltNumFields elimInfo altName
-    let (altVarNames, names') := names.splitAtD numFields (Unhygienic.run `(_))
-    names := names'
-    let (fvars, g) ← g.introN numFields <| altVarNames.map (getNameOfIdent' ·[0])
-    let some (g, subst) ← Cases.unifyEqs? numEqs g {} | pure ()
-    let (_, g) ← g.introNP numGeneralized
-    let g ← liftM $ toClear.foldlM (·.tryClear) g
-    for fvar in fvars, stx in altVarNames do
-      g.withContext <| (subst.apply <| .fvar fvar).addLocalVarInfoForBinderIdent ⟨stx⟩
-    subgoals := subgoals.push g
-  pure subgoals
-
-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
-
-/--
-Modified `induction` tactic for this game.
-
-Usage: `induction n with d hd`.
-
-*(The actual `induction` tactic has a more complex `with`-argument that works differently)*
--/
-elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+)
-    withArg:((" with " (colGt binderIdent)+)?)
-    : tactic => do
-  let targets ← elabCasesTargets tgts.1.getSepArgs
-  let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
-  g.withContext do
-    let elimInfo ← getElimInfo `MyNat.rec'
-    let targets ← addImplicitTargets elimInfo targets
-    evalInduction.checkTargets targets
-    let targetFVarIds := targets.map (·.fvarId!)
-    g.withContext do
-      let forbidden ← mkGeneralizationForbiddenSet targets
-      let mut s ← getFVarSetToGeneralize targets forbidden
-      let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray)
-      let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag)
-      let elimArgs := result.elimApp.getAppArgs
-      ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds
-      g.assign result.elimApp
-      let subgoals ← ElimApp.evalNames.MyNat elimInfo result.alts withArg
-        (numGeneralized := fvarIds.size) (toClear := targetFVarIds)
-      setGoals <| (subgoals ++ result.others).toList ++ gs
-
-end Lean.Parser.Tactic
-
-
-
diff --git a/server/nng/NNG/Tactic/Rfl.lean b/server/nng/NNG/Tactic/Rfl.lean
deleted file mode 100644
index b119a3f..0000000
--- a/server/nng/NNG/Tactic/Rfl.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import Mathlib.Lean.Expr.Basic
-import Lean.Elab.Tactic.Basic
-
-/-! # `rfl` tactic
-
-Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
--/
-
-namespace MyNat
-
-open Lean Meta Elab Tactic
-
--- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
-
-/-- Modified `rfl` tactic.
-
-`rfl` closes goals of the form `A = A`.
-
-Note that teh version for this game is somewhat weaker than the real one. -/
-syntax (name := rfl) "rfl" : tactic
-
-@[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
-  liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure []
--- TODO: `rfl` should be able to prove `R ↔ R`!
-
-
--- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
---   liftMetaTactic fun mvarId => do mvarId.refl; pure []
--- (with_reducible rfl)
-
-end MyNat
diff --git a/server/nng/NNG/Tactic/Rw.lean b/server/nng/NNG/Tactic/Rw.lean
deleted file mode 100644
index 29f83ff..0000000
--- a/server/nng/NNG/Tactic/Rw.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-import Mathlib.Lean.Expr.Basic
-import Lean.Elab.Tactic.Basic
-
-/-!
-# Modified `rw`
-
-Modify `rw` to work like `rewrite`.
-
-This is mainly a copy of the implementation of `rewrite` in Lean core.
--/
-
-namespace MyNat
-
-open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic
-
-/--
-Modified `rw` tactic. For this game, `rw` works exactly like `rewrite`.
--/
-syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic
-
-@[tactic MyNat.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
-  let cfg ← elabRewriteConfig stx[1]
-  let loc   := expandOptLocation stx[3]
-  withRWRulesSeq stx[0] stx[2] fun symm term => do
-    withLocation loc
-      (rewriteLocalDecl term symm · cfg)
-      (rewriteTarget term symm cfg)
-      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
diff --git a/server/nng/NNG/Tactic/Simp.lean b/server/nng/NNG/Tactic/Simp.lean
deleted file mode 100644
index 2716d23..0000000
--- a/server/nng/NNG/Tactic/Simp.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-import Mathlib.Lean.Expr.Basic
-import Lean.Elab.Tactic.Basic
-import NNG.Tactic.Rfl
-
-/-! # `simp` tactic
-
-Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
--/
-
-namespace MyNat
-
-open Lean Meta Elab Tactic
-
--- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
-
-/--
-The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
-non-dependent hypotheses. It has many variants:
-- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
-- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
-  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.
-  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with
-  `f` are used. This provides a convenient way to unfold `f`.
-- `simp [*]` simplifies the main goal target using the lemmas tagged with the
-  attribute `[simp]` and all hypotheses.
-- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
-- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
-  with the attribute `[simp]`, but removes the ones named `idᵢ`.
-- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
-  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
-  `hᵢ` is introduced, but the old one remains in the local context.
-- `simp at *` simplifies all the hypotheses and the target.
-- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
-  other hypotheses.
--/
-syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic
-
-/-
-  "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
--/
-@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
-  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
-  let usedSimps ← dischargeWrapper.with fun discharge? =>
-    simpLocation ctx discharge? (expandOptLocation stx[5])
-  if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
-
-end MyNat
-
-
diff --git a/server/nng/lake-manifest.json b/server/nng/lake-manifest.json
deleted file mode 100644
index cc199bf..0000000
--- a/server/nng/lake-manifest.json
+++ /dev/null
@@ -1,33 +0,0 @@
-{"version": 4,
- "packagesDir": "lake-packages",
- "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
-    "subDir?": null,
-    "rev": "fc4a489c2af75f687338fe85c8901335360f8541",
-    "name": "mathlib",
-    "inputRev?": "fc4a489c2af75f687338fe85c8901335360f8541"}},
-  {"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "cc915afc9526e904a7b61f660d330170f9d60dd7",
-    "name": "Qq",
-    "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/JLimperg/aesop",
-    "subDir?": null,
-    "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
-    "name": "aesop",
-    "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/lean4game.git",
-    "subDir?": "server/leanserver",
-    "rev": "9fa94ecc5ca1c398479fb6026b03fcac46928bd7",
-    "name": "GameServer",
-    "inputRev?": "main"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
-    "name": "std",
-    "inputRev?": "main"}}]}
diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean
deleted file mode 100644
index d1adbdc..0000000
--- a/server/nng/lakefile.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Lake
-open Lake DSL
-
-require GameServer from  git
-  "https://github.com/leanprover-community/lean4game.git"@"main"/"server"/"leanserver"
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"
-
-package NNG where
-  moreLeanArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]
-  moreServerArgs := #["-DautoImplicit=false", "-Dtactic.hygienic=false"]
-
-@[default_target]
-lean_lib NNG
diff --git a/server/nng/lean-toolchain b/server/nng/lean-toolchain
deleted file mode 100644
index 7f0fd43..0000000
--- a/server/nng/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:nightly-2023-03-09