diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
index 12c81da..a9acf96 100644
--- a/.devcontainer/Dockerfile
+++ b/.devcontainer/Dockerfile
@@ -2,21 +2,27 @@ FROM node:20
 
 WORKDIR /
 
-ENV ELAN_HOME=/usr/local/elan \
-  PATH=/usr/local/elan/bin:$PATH \
-  LEAN_VERSION=leanprover/lean4:v4.1.0
-  # TODO: read toolchain from `lean-toolchain`
-
-SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
-
-RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
-  chmod -R a+w $ELAN_HOME; \
-  elan --version; \
-  lean --version; \
-  leanc --version; \
-  lake --version;
+COPY ./lean-toolchain /lean-toolchain
 
 USER node
 
 WORKDIR /home/node
-RUN git clone https://github.com/leanprover-community/lean4game.git
+
+RUN export LEAN_VERSION="$(cat /lean-toolchain | grep -oE '[^:]+$')" && git clone --depth 1 --branch $LEAN_VERSION https://github.com/leanprover-community/lean4game.git
+
+WORKDIR /
+
+USER root
+
+ENV ELAN_HOME=/usr/local/elan \
+  PATH=/usr/local/elan/bin:$PATH
+
+SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]
+
+RUN export LEAN_VERSION="$(cat /lean-toolchain)" && \
+  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
+    chmod -R a+w $ELAN_HOME; \
+    elan --version; \
+    lean --version; \
+    leanc --version; \
+    lake --version;
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index a71b3e1..62b8651 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -13,9 +13,11 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake update && lake exe cache get && lake build)"
+    // BUG: Apparently `&& lake exe cache get` was needed here because the update hook was broken.
+    // should been fixed in https://github.com/leanprover-community/mathlib4/pull/8755
+    "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)"
   },
-  "postStartCommand": "cd ~/lean4game && export LEAN4GAME_SINGLE_GAME=true && npm start",
+  "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {
     "vscode": {
       "settings": {
diff --git a/.devcontainer/docker-compose.yml b/.devcontainer/docker-compose.yml
index 3dcf40c..818123c 100644
--- a/.devcontainer/docker-compose.yml
+++ b/.devcontainer/docker-compose.yml
@@ -3,8 +3,8 @@ version: "3.9"
 services:
   game:
     build:
-      context: .
-      dockerfile: Dockerfile
+      context: ..
+      dockerfile: .devcontainer/Dockerfile
     volumes:
       - ..:/home/node/game
     ports:
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 9bae80d..eaa72db 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -9,15 +9,57 @@ jobs:
     runs-on: ubuntu-latest
     steps:
 
-      - uses: actions/checkout@v2
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: build docker image
-        run: docker build . --file Dockerfile --tag game:latest
+      - uses: actions/checkout@v4
 
-      - name: Store docker container as an artifact
-        uses: ishworkh/docker-image-artifact-upload@v1
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+        # Note: this would also happen in the lake post-update-hook
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: create timestamp file
+        run: touch tmp_timestamp
+
+        # Note: this would also happen in the lake post-update-hook
+      - name: build gameserver executable
+        run: env LEAN_ABORT_ON_PANIC=1 lake build gameserver
+
+      - name: building game
+        run: env LEAN_ABORT_ON_PANIC=1 lake build
+
+      - name: delete unused mathlib cache
+        continue-on-error: true
+        run: find . -type d \( -name "*/.git" \) -delete -print && find ./.lake/ -type f \( -name "*.c" -o -name "*.hash" -o -name "*.trace" \) -delete -print && find ./.lake/ -type f \( -name "*.olean" \) \! -neweraa ./tmp_timestamp -delete -print
+
+      - name: delete timestamp file
+        run: rm ./tmp_timestamp
+
+      - name: compress built game
+        #run: tar -czvf ../game.tar.gz .
+        run: zip game.zip * .lake/ -r
+
+      - name: upload compressed game folder
+        uses: actions/upload-artifact@v3
         with:
-          image: "game:latest"
+          name: build-for-server-import
+          path: |
+            game.zip
 
       - name: What next?
         run: echo "To export the game to the Game Server, open https://adam.math.hhu.de/import/trigger/${GITHUB_REPOSITORY,,} \n Afterwards, you can play the game at https://adam.math.hhu.de/#/g/${GITHUB_REPOSITORY,,}"
diff --git a/.github/workflows/build_non_main.yml b/.github/workflows/build_non_main.yml
index 196483c..23c541c 100644
--- a/.github/workflows/build_non_main.yml
+++ b/.github/workflows/build_non_main.yml
@@ -10,7 +10,28 @@ jobs:
     runs-on: ubuntu-latest
     steps:
 
-      - uses: actions/checkout@v2
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: build docker image
-        run: docker build . --file Dockerfile --tag game:latest
+      - uses: actions/checkout@v4
+
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: building game
+        run: env LEAN_ABORT_ON_PANIC=1 lake build
diff --git a/.gitignore b/.gitignore
index c1338ac..32f4763 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,4 @@
 build/
 lake-packages/
-lakefile.olean
+.lake/
 **/.DS_Store
diff --git a/Game.lean b/Game.lean
index 1386e2f..aa8dd68 100644
--- a/Game.lean
+++ b/Game.lean
@@ -98,16 +98,16 @@ Alternatively, if you experience issues / bugs you can also open github issues:
 
 "
 
--- Here's where we show how to glue the worlds together
-Dependency Addition → Multiplication → Power
---Dependency Addition → AdvAddition → AdvMultiplication → Inequality → Prime → Hard
---Dependency Multiplication → AdvMultiplication
---Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
-Dependency Addition → Implication → AdvAddition → LessOrEqual
-Dependency AdvAddition → Algorithm
--- The game automatically computes connections between worlds based on introduced
--- tactics and theorems, but for example it cannot detect introduced definitions
-
 -- Dependency Implication → Power -- `Power` uses `≠` which is introduced in `Implication`
 
+/-! Information to be displayed on the servers landing page. -/
+Languages "English"
+CaptionShort "The classical introduction game for Lean."
+CaptionLong "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,
+learning the basics about theorem proving in Lean.
+
+This is a good first introduction to Lean!"
+CoverImage "images/cover.png"
+
+/-! Build the game. Show's warnings if it found a problem with your game. -/
 MakeGame
diff --git a/Game/Doc/Definitions.lean b/Game/Doc/Definitions.lean
index 83cb084..4559048 100644
--- a/Game/Doc/Definitions.lean
+++ b/Game/Doc/Definitions.lean
@@ -13,7 +13,7 @@ import GameServer.Commands
 -- 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
+-- If you end up getting something of type `Nat` in this game, you probably
 -- need to write `(4 : ℕ)` to force it to be of type `MyNat`.
 
 -- *Write with `\\N`.*
diff --git a/Game/Levels/Addition/L01zero_add.lean b/Game/Levels/Addition/L01zero_add.lean
index 76c6602..2fcc783 100644
--- a/Game/Levels/Addition/L01zero_add.lean
+++ b/Game/Levels/Addition/L01zero_add.lean
@@ -45,7 +45,8 @@ Statement zero_add (n : ℕ) : 0 + n = n := by
     This first goal is the base case $n = 0$.
 
     Recall that you can rewrite the proof of any lemma which is visible
-    in your inventory, or of any assumption displayed above the goal."
+    in your inventory, or of any assumption displayed above the goal,
+    as long as it is of the form `X = Y`."
     Hint (hidden := true) "try rewriting `add_zero`."
     rw [add_zero]
     rfl
diff --git a/Game/Levels/Addition/L05add_right_comm.lean b/Game/Levels/Addition/L05add_right_comm.lean
index 6d21385..3f02bdf 100644
--- a/Game/Levels/Addition/L05add_right_comm.lean
+++ b/Game/Levels/Addition/L05add_right_comm.lean
@@ -45,4 +45,6 @@ You can begin the journey towards this boss by entering Multiplication World.
 Or you can go off the beaten track and learn some new tactics in Implication
 World. These tactics let you prove more facts about addition, such as
 how to deduce `a = 0` from `x + a = x`.
+
+Click \"Leave World\" and make your choice.
 "
diff --git a/Game/Levels/AdvAddition.lean b/Game/Levels/AdvAddition.lean
index f6cc3a6..a3e8209 100644
--- a/Game/Levels/AdvAddition.lean
+++ b/Game/Levels/AdvAddition.lean
@@ -3,8 +3,8 @@ import Game.Levels.AdvAddition.L02add_right_cancel
 import Game.Levels.AdvAddition.L03add_left_cancel
 import Game.Levels.AdvAddition.L04add_left_eq_self
 import Game.Levels.AdvAddition.L05add_right_eq_self
-import Game.Levels.AdvAddition.L06eq_zero_of_add_right_eq_zero
-import Game.Levels.AdvAddition.L07eq_zero_of_add_left_eq_zero
+import Game.Levels.AdvAddition.L06add_right_eq_zero
+import Game.Levels.AdvAddition.L07add_left_eq_zero
 
 World "AdvAddition"
 Title "Advanced Addition World"
diff --git a/Game/Levels/AdvAddition/L06add_right_eq_zero.lean b/Game/Levels/AdvAddition/L06add_right_eq_zero.lean
new file mode 100644
index 0000000..6b1a40f
--- /dev/null
+++ b/Game/Levels/AdvAddition/L06add_right_eq_zero.lean
@@ -0,0 +1,90 @@
+import Game.Levels.AdvAddition.L05add_right_eq_self
+import Game.Tactic.Cases
+
+World "AdvAddition"
+Level 6
+Title "add_right_eq_zero"
+
+LemmaTab "Peano"
+
+namespace MyNat
+
+Introduction
+"The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.
+Let's prove one of these facts in this level, and the other in the next.
+
+## A new tactic: `cases`
+
+The `cases` tactic will split an object or hypothesis up into the possible ways
+that it could have been created.
+
+For example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,
+but don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.
+In this situation you can use `cases b with d` instead. There are two ways to make
+a number: it's either zero or a successor. So you will end up with two goals, one
+with `b = 0` and one with `b = succ d`.
+
+Another example: if you have a hypothesis `h : False` then you are done, because a false statement implies
+any statement. Here `cases h` will close the goal, because there are *no* ways to
+make a proof of `False`! So you will end up with no goals, meaning you have proved everything.
+
+"
+
+TacticDoc cases "
+## Summary
+
+If `n` is a number, then `cases n with d` will break the goal into two goals,
+one with `n = 0` and the other with `n = succ d`.
+
+If `h` is a proof (for example a hypothesis), then `cases h with...` will break the
+proof up into the pieces used to prove it.
+
+## Example
+
+If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,
+one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This
+corresponds to the mathematical idea that every natural number is either `0`
+or a successor.
+
+## Example
+
+If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal
+into two goals, one with a hypothesis `hp : P` and the other with a
+hypothesis `hq : Q`.
+
+## Example
+
+If `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,
+because there are no ways to make a proof of `False`! And if you have no goals left,
+you have finished the level.
+
+## Example
+
+If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`
+and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is
+`∃ c, b = a + c`.
+"
+NewTactic cases
+
+LemmaDoc MyNat.add_right_eq_zero as "add_right_eq_zero" in "+" "
+  A proof that $a+b=0 \\implies a=0$.
+"
+
+-- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
+-- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/eq_zero_of_add_eq_zero_right/near/395716874
+
+/-- If $a+b=0$ then $a=0$. -/
+Statement add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
+  Hint "Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,
+  so start with `cases b with d`."
+  cases b with d
+  intro h
+  rw [add_zero] at h
+  exact h
+  intro h
+  rw [add_succ] at h
+  symm at h
+  apply zero_ne_succ at h
+  cases h
+
+Conclusion "Well done!"
diff --git a/Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean b/Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean
deleted file mode 100644
index 53698bd..0000000
--- a/Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean
+++ /dev/null
@@ -1,106 +0,0 @@
-import Game.Levels.AdvAddition.L05add_right_eq_self
-import Game.Tactic.Cases
-
-World "AdvAddition"
-Level 6
-Title "eq_zero_of_add_right_eq_zero"
-
-LemmaTab "Peano"
-
-namespace MyNat
-
-Introduction
-" We have still not proved that if `a + b = 0` then `a = 0` and also `b = 0`. Let's finish this
-world by proving one of these in this level, and the other in the next.
-
-## Two new tactics
-
-If you have a hypothesis `h : False` then you are done, because a false statement implies
-any statement. You can use the `tauto` tactic to finish your proof.
-
-Sometimes you just want to deal with the two cases `b = 0` and `b = succ d` separately,
-and don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.
-In this situation you can use `cases b with d` instead.
-
-"
-
-TacticDoc tauto "
-# Summary
-
-The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by
-truth tables).
-
-## Example
-
-If you have `False` as a hypothesis, then `tauto` will solve
-the goal. This is because a false hypothesis implies any hypothesis.
-
-## Example
-
-If your goal is `True`, then `tauto` will solve the goal.
-
-## Example
-
-If you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will
-solve the goal because it can prove `False` from your hypotheses, and thus
-prove the goal (as `False` implies anything).
-
-## Example
-
-If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then
-`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.
-If you switch the goal and hypothesis in this example, `tauto` would solve it too.
-"
-
-TacticDoc cases "
-## Summary
-
-If `n` is a number, then `cases n with d` will break the goal into two goals,
-one with `n = 0` and the other with `n = succ d`.
-
-If `h` is a proof (for example a hypothesis), then `cases h with...` will break the
-proof up into the pieces used to prove it.
-
-## Example
-
-If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`
-and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is
-`∃ c, b = a + c`.
-
-## Example
-
-If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,
-one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This
-corresponds to the mathematical idea that every natural number is either `0`
-or a successor.
-
-## Example
-
-If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal
-into two goals, one with a hypothesis `hp : P` and the other with a
-hypothesis `hq : Q`.
-"
-NewTactic tauto cases
-
-LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in "+" "
-  A proof that $a+b=0 \\implies a=0$.
-"
-
--- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
--- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/eq_zero_of_add_eq_zero_right/near/395716874
-
-/-- If $a+b=0$ then $a=0$. -/
-Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
-  Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately,
-  so start with `cases b with d`."
-  cases b with d
-  intro h
-  rw [add_zero] at h
-  exact h
-  intro h
-  rw [add_succ] at h
-  symm at h
-  apply zero_ne_succ at h
-  tauto
-
-Conclusion "Well done!"
diff --git a/Game/Levels/AdvAddition/L07add_left_eq_zero.lean b/Game/Levels/AdvAddition/L07add_left_eq_zero.lean
new file mode 100644
index 0000000..beb601f
--- /dev/null
+++ b/Game/Levels/AdvAddition/L07add_left_eq_zero.lean
@@ -0,0 +1,33 @@
+import Game.Levels.AdvAddition.L06add_right_eq_zero
+
+World "AdvAddition"
+Level 7
+Title "add_left_eq_zero"
+
+LemmaTab "+"
+
+namespace MyNat
+
+Introduction
+"You can just mimic the previous proof to do this one -- or you can figure out a way
+of using it.
+"
+
+LemmaDoc MyNat.add_left_eq_zero as "add_left_eq_zero" in "+" "
+  A proof that $a+b=0 \\implies b=0$.
+"
+
+/-- If $a+b=0$ then $b=0$. -/
+Statement add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0 := by
+  rw [add_comm]
+  exact add_right_eq_zero b a
+
+Conclusion "How about this for a proof:
+
+```
+rw [add_comm]
+exact add_right_eq_zero b a
+```
+
+We've now proved all the theorems you'll need for `≤` World.
+"
diff --git a/Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean b/Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean
deleted file mode 100644
index 05110ad..0000000
--- a/Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean
+++ /dev/null
@@ -1,33 +0,0 @@
-import Game.Levels.AdvAddition.L06eq_zero_of_add_right_eq_zero
-
-World "AdvAddition"
-Level 7
-Title "eq_zero_of_add_left_eq_zero"
-
-LemmaTab "+"
-
-namespace MyNat
-
-Introduction
-"You can just mimic the previous proof to do this one -- or you can figure out a way
-of using it.
-"
-
-LemmaDoc MyNat.eq_zero_of_add_left_eq_zero as "eq_zero_of_add_left_eq_zero" in "+" "
-  A proof that $a+b=0 \\implies b=0$.
-"
-
-/-- If $a+b=0$ then $b=0$. -/
-Statement eq_zero_of_add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0 := by
-  rw [add_comm]
-  exact eq_zero_of_add_right_eq_zero b a
-
-Conclusion "How about this for a proof:
-
-```
-rw [add_comm]
-exact eq_zero_of_add_right_eq_zero b a
-```
-
-You're now ready for `≤` World.
-"
diff --git a/Game/Levels/Algorithm/L01add_left_comm.lean b/Game/Levels/Algorithm/L01add_left_comm.lean
index 80508b9..609d21b 100644
--- a/Game/Levels/Algorithm/L01add_left_comm.lean
+++ b/Game/Levels/Algorithm/L01add_left_comm.lean
@@ -17,7 +17,7 @@ associativity is very tedious. We start by reminding you of this. `add_left_comm
 is a key component in the first algorithm which we'll explain, but we need
 to prove it manually.
 
-Remember that you do precision commutativity rewriting
+Remember that you can do precision commutativity rewriting
 with things like `rw [add_comm b c]`. And remember that
 `a + b + c` means `(a + b) + c`.
 "
diff --git a/Game/Levels/Algorithm/L03add_algo2.lean b/Game/Levels/Algorithm/L03add_algo2.lean
index a2b4837..4c5d175 100644
--- a/Game/Levels/Algorithm/L03add_algo2.lean
+++ b/Game/Levels/Algorithm/L03add_algo2.lean
@@ -28,8 +28,6 @@ This level is not a level which you want to solve by hand.
 Get the simplifier to solve it for you.
 "
 
---macro_rules | `(tactic| ac_rfl) => `(tactic| simp only [add_assoc, add_left_comm, add_comm])
-
 /-- If $a, b,\ldots h$ are arbitrary natural numbers, we have
 $(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$. -/
 Statement (a b c d e f g h : ℕ) :
diff --git a/Game/Levels/Algorithm/L04add_algo3.lean b/Game/Levels/Algorithm/L04add_algo3.lean
index 2a8e254..9377990 100644
--- a/Game/Levels/Algorithm/L04add_algo3.lean
+++ b/Game/Levels/Algorithm/L04add_algo3.lean
@@ -22,15 +22,15 @@ NewTactic simp_add
 
 Introduction
 "
-You can even make your own tactics in Lean.
+You can make your own tactics in Lean.
 This code here
 ```
 macro \"simp_add\" : tactic => `(tactic|(
   simp only [add_assoc, add_left_comm, add_comm]))
 ```
-creates a new tactic `simp_add`, which runs
+was used to create a new tactic `simp_add`, which runs
 `simp only [add_assoc, add_left_comm, add_comm]`.
-Try it!
+Try running `simp_add` to solve this level!
 "
 
 
diff --git a/Game/Levels/Algorithm/L06is_zero.lean b/Game/Levels/Algorithm/L06is_zero.lean
index b417fd5..779c2f0 100644
--- a/Game/Levels/Algorithm/L06is_zero.lean
+++ b/Game/Levels/Algorithm/L06is_zero.lean
@@ -20,9 +20,11 @@ is_zero (succ n) := False
 We also create two lemmas, `is_zero_zero` and `is_zero_succ n`, saying that `is_zero 0 = True`
 and `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`, Peano's
 Last Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have
-this opposite version too, which can be proved in the same way.
+this opposite version too, which can be proved in the same way. Note: you can
+cheat here by using `zero_ne_succ` but the point of this world is to show
+you how to *prove* results like that.
 
-If you can turn your goal into `True`, then the `tauto` tactic will solve it.
+If you can turn your goal into `True`, then the `triv` tactic will solve it.
 "
 
 LemmaDoc MyNat.is_zero_zero as "is_zero_zero" in "Peano"
@@ -42,14 +44,25 @@ LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Peano"
 
 NewLemma MyNat.is_zero_zero MyNat.is_zero_succ
 
-/-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/
+TacticDoc triv "
+# Summary
+
+`triv` will solve the goal `True`.
+
+"
+
+NewTactic triv
+
+/-- $\operatorname{succ}(a) \neq 0$. -/
 Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   Hint "Start with `intro h` (remembering that `X ≠ Y` is just notation
   for `X = Y → False`)."
   intro h
-  Hint "We're going to change that `False` into `True`. Start by changing it into `is_zero (succ a)`."
-  Hint (hidden := true) "Try `rw [← is_zero_succ a]`."
+  Hint "We're going to change that `False` into `True`. Start by changing it into
+  `is_zero (succ a)` by executing `rw [← is_zero_succ a]`."
   rw [← is_zero_succ a]
+  Hint "See if you can take it from here. Look at the new lemmas and tactic
+  available on the right."
   rw [h]
   rw [is_zero_zero]
-  tauto
+  triv
diff --git a/Game/Levels/Algorithm/L07succ_ne_succ.lean b/Game/Levels/Algorithm/L07succ_ne_succ.lean
index 9682ef5..b261703 100644
--- a/Game/Levels/Algorithm/L07succ_ne_succ.lean
+++ b/Game/Levels/Algorithm/L07succ_ne_succ.lean
@@ -10,20 +10,24 @@ namespace MyNat
 
 Introduction
 "
-Every natural is either `0` or `succ n` for some `n`. Here is an algorithm
-which, given two naturals `a` and `b`, returns the answer to \"does `a = b`?\"
+Here we begin to
+develop an algorithm which, given two naturals `a` and `b`, returns the answer
+to \"does `a = b`?\"
 
-*) If they're both `0`, return \"yes\".
+Here is the algorithm. First note that `a` and `b` are numbers, and hence
+are either `0` or successors.
+
+*) If `a` and `b` are both `0`, return \"yes\".
 
 *) If one is `0` and the other is `succ n`, return \"no\".
 
 *) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"
 
-Let's prove that this algorithm always gives the correct answer. The proof that
+Our job now is to *prove* that this algorithm always gives the correct answer. The proof that
 `0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof
 that `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then
-`succ m = succ n` is `rw [h]` and then `rfl`. The next level is a proof of the one
-remaining case: if `a ≠ b` then `succ a ≠ succ b`.
+`succ m = succ n` is `rw [h]` and then `rfl`. This level is a proof of the one
+remaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`.
 "
 
 TacticDoc contrapose "
diff --git a/Game/Levels/Algorithm/L08decide.lean b/Game/Levels/Algorithm/L08decide.lean
index fe90178..df00b10 100644
--- a/Game/Levels/Algorithm/L08decide.lean
+++ b/Game/Levels/Algorithm/L08decide.lean
@@ -52,7 +52,9 @@ instance instDecidableEq : DecidableEq ℕ
 ```
 
 This Lean code is a formally verified algorithm for deciding equality
-between two naturals. Run it with the `decide` tactic.
+between two naturals. I've typed it in already, behind the scenes.
+Because the algorithm is formally verified to be correct, we can
+use it in Lean proofs. You can run the algorithm with the `decide` tactic.
 "
 
 /-- $20+20=40$. -/
diff --git a/Game/Levels/Implication/L01exact.lean b/Game/Levels/Implication/L01exact.lean
index 69347ef..1c92d46 100644
--- a/Game/Levels/Implication/L01exact.lean
+++ b/Game/Levels/Implication/L01exact.lean
@@ -38,7 +38,7 @@ NewTactic exact
 Introduction
 "
 In this world we'll learn how to prove theorems of the form $P\\implies Q$.
-In othey words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"
+In other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"
 To do that we need to learn some more tactics.
 
 The `exact` tactic can be used to close a goal which is exactly one of
@@ -52,5 +52,5 @@ unused variable `h2` [linter.unusedVariables]
 but I want `h2` to be there.
 -/
 Statement (x y z : ℕ) (h1 : x + y = 37) (h2 : 3 * x + z = 42) : x + y = 37 := by
-  Hint "The goal is one of our hypotheses. Solve the goal by executing `exact h1`."
+  Hint "The goal in this level is one of our hypotheses. Solve the goal by executing `exact h1`."
   exact h1
diff --git a/Game/Levels/Implication/L04succ_inj.lean b/Game/Levels/Implication/L04succ_inj.lean
index 822ef68..1d4fc4e 100644
--- a/Game/Levels/Implication/L04succ_inj.lean
+++ b/Game/Levels/Implication/L04succ_inj.lean
@@ -14,7 +14,7 @@ If `a` and `b` are numbers, then `succ_inj a b` is a proof
 that `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*
 tab for more information.
 
-Peano had this theorem as an axiom, but in Functional Programming World
+Peano had this theorem as an axiom, but in Algorithm World
 we will show how to prove it in Lean. Right now let's just assume it,
 and let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed
 by manipulating our hypothesis until it becomes the goal. I will
diff --git a/Game/Levels/Implication/L08ne.lean b/Game/Levels/Implication/L08ne.lean
index 0e694f3..34a8330 100644
--- a/Game/Levels/Implication/L08ne.lean
+++ b/Game/Levels/Implication/L08ne.lean
@@ -31,4 +31,23 @@ Statement (x y : ℕ) (h1 : x = y) (h2 : x ≠ y) : False := by
   apply h2 at h1
   exact h1
 
+DefinitionDoc Ne as "≠" "
+  `a ≠ b` is *notation* for `(a = b) → False`.
+
+  The reason this is mathematically
+  valid is that if `P` is a true-false statement then `P → False`
+  is the logical opposite of `P`. Indeed `True → False` is false,
+  and `False → False` is true!
+
+  The upshot of this is that use can treat `a ≠ b` in exactly
+  the same way as you treat any implication `P → Q`. For example,
+  if your *goal* is of the form `a ≠ b` then you can make progress
+  with `intro h`, and if you have a hypothesis `h` of the
+  form `a ≠ b` then you can `apply h at h1` if `h1` is a proof
+  of `a = b`.
+
+"
+
+NewDefinition Ne
+
 Conclusion "Remember, `x ≠ y` is *notation* for `x = y → False`."
diff --git a/Game/Levels/Implication/L09zero_ne_succ.lean b/Game/Levels/Implication/L09zero_ne_succ.lean
index 28c6f51..0ba40e9 100644
--- a/Game/Levels/Implication/L09zero_ne_succ.lean
+++ b/Game/Levels/Implication/L09zero_ne_succ.lean
@@ -4,7 +4,7 @@ World "Implication"
 Level 9
 Title "zero_ne_succ"
 
-LemmaTab "Peano"
+LemmaTab "012"
 
 namespace MyNat
 
diff --git a/Game/Levels/Implication/L10one_ne_zero.lean b/Game/Levels/Implication/L10one_ne_zero.lean
index 289cfba..5464f1f 100644
--- a/Game/Levels/Implication/L10one_ne_zero.lean
+++ b/Game/Levels/Implication/L10one_ne_zero.lean
@@ -3,18 +3,18 @@ World "Implication"
 Level 10
 Title "1 ≠ 0"
 
-LemmaTab "Peano"
+LemmaTab "012"
 
 namespace MyNat
 
 Introduction "
-We know `succ_ne_zero n` is a proof of `0 = succ n → false` -- but what
+We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what
 if we have a hypothesis `succ n = 0`? It's the wrong way around!
 
 The `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`
 to `y ≠ x`. And `symm at h`
-does the same for a hypothesis `h`. We've proved $0 \\neq 1$; now try
-proving $1 \\neq 0$.
+does the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called
+the proof `zero_ne_one`; now try proving $1 \\neq 0$.
 "
 
 TacticDoc symm "
diff --git a/Game/Levels/Implication/L11two_add_two_ne_five.lean b/Game/Levels/Implication/L11two_add_two_ne_five.lean
index ac5290c..a729890 100644
--- a/Game/Levels/Implication/L11two_add_two_ne_five.lean
+++ b/Game/Levels/Implication/L11two_add_two_ne_five.lean
@@ -31,7 +31,10 @@ apply zero_ne_succ at h
 exact h
 ```
 
-Right now we have not developed enough material to make Lean an adequate calculator.
-In the forthcoming algorithm and functional programming worlds we will develop machinery
-which makes questions like this much easier, and questions like 20 + 20 ≠ 41 feasible.
-Until I've written them, why not press on to Advanced Addition World."
+Even though Lean is a theorem prover, right now it's pretty clear that we have not
+developed enough material to make it an adequate calculator. In Algorithm
+World, a more computer-sciency world, we will develop machinery which makes
+questions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.
+Alternatively you can do more mathematics in Advanced Addition World, where we prove
+the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and
+decide your route."
diff --git a/Game/Levels/LessOrEqual.lean b/Game/Levels/LessOrEqual.lean
index bdcad61..871595f 100644
--- a/Game/Levels/LessOrEqual.lean
+++ b/Game/Levels/LessOrEqual.lean
@@ -7,6 +7,9 @@ import Game.Levels.LessOrEqual.L05le_zero
 import Game.Levels.LessOrEqual.L06le_antisymm
 import Game.Levels.LessOrEqual.L07or_symm
 import Game.Levels.LessOrEqual.L08le_total
+import Game.Levels.LessOrEqual.L09le_of_succ_le_succ
+import Game.Levels.LessOrEqual.L10le_one
+import Game.Levels.LessOrEqual.L11le_two
 
 World "LessOrEqual"
 Title "≤ World"
diff --git a/Game/Levels/LessOrEqual/L01le_refl.lean b/Game/Levels/LessOrEqual/L01le_refl.lean
index eb46e53..061830d 100644
--- a/Game/Levels/LessOrEqual/L01le_refl.lean
+++ b/Game/Levels/LessOrEqual/L01le_refl.lean
@@ -23,6 +23,19 @@ number which is morally `b - a`.
 
 NewTactic use
 
+DefinitionDoc LE as "≤" "
+`a ≤ b` is *notation* for `∃ c, b = a + c`.
+
+Because this game doesn't have negative numbers, this definition
+is mathematically valid.
+
+This means that if you have a goal of the form `a ≤ b` you can
+make progress with the `use` tactic, and if you have a hypothesis
+`h : a ≤ b`, you can make progress with `cases h with c hc`.
+"
+
+NewDefinition LE
+
 Introduction
 "
 `a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"
diff --git a/Game/Levels/LessOrEqual/L03le_succ_self.lean b/Game/Levels/LessOrEqual/L03le_succ_self.lean
index 8a52205..9eac20f 100644
--- a/Game/Levels/LessOrEqual/L03le_succ_self.lean
+++ b/Game/Levels/LessOrEqual/L03le_succ_self.lean
@@ -34,7 +34,7 @@ This works because `succ_eq_add_one x` is a proof of `succ x = x + 1`.
 /-
 Introduction
 "
-Because constanly rewriting `zero_add` and `add_zero` is a bit dull,
+Because constantly rewriting `zero_add` and `add_zero` is a bit dull,
 let's unlock the `ring` tactic. This will prove any goal which is \"true
 in the language of ring theory\", for example `a + b + c = c + b + a`.
 It doesn't understand `succ` though, so use `succ_eq_add_one` in this
diff --git a/Game/Levels/LessOrEqual/L04le_trans.lean b/Game/Levels/LessOrEqual/L04le_trans.lean
index 139a4db..63724fe 100644
--- a/Game/Levels/LessOrEqual/L04le_trans.lean
+++ b/Game/Levels/LessOrEqual/L04le_trans.lean
@@ -23,7 +23,7 @@ and $Q\\implies R$.
 "
 
 Introduction "
-In this level, we inequalities as *hypotheses*. We have not seen this before.
+In this level, we see inequalities as *hypotheses*. We have not seen this before.
 The `cases` tactic can be used to take `hxy` apart.
 "
 
diff --git a/Game/Levels/LessOrEqual/L05le_zero.lean b/Game/Levels/LessOrEqual/L05le_zero.lean
index b987cea..8e66039 100644
--- a/Game/Levels/LessOrEqual/L05le_zero.lean
+++ b/Game/Levels/LessOrEqual/L05le_zero.lean
@@ -6,6 +6,8 @@ Title "x ≤ 0 → x = 0"
 
 namespace MyNat
 
+LemmaTab "+"
+
 LemmaDoc MyNat.le_zero as "le_zero" in "≤" "
 `le_zero x` is a proof of `x ≤ 0 → x = 0`.
 "
@@ -22,10 +24,10 @@ LemmaDoc MyNat.le_zero as "le_zero" in "≤"
 /-- If $x \leq 0$, then $x=0$. -/
 Statement le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by
   cases hx with y hy
-  Hint (hidden := true) "You want to use `eq_zero_of_add_right_eq_zero`, which you already
+  Hint (hidden := true) "You want to use `add_right_eq_zero`, which you already
   proved, but you'll have to start with `symm at` your hypothesis."
   symm at hy
-  apply eq_zero_of_add_right_eq_zero at hy
+  apply add_right_eq_zero at hy
   exact hy
 
 LemmaTab "≤"
diff --git a/Game/Levels/LessOrEqual/L06le_antisymm.lean b/Game/Levels/LessOrEqual/L06le_antisymm.lean
index 2a90f11..e877995 100644
--- a/Game/Levels/LessOrEqual/L06le_antisymm.lean
+++ b/Game/Levels/LessOrEqual/L06le_antisymm.lean
@@ -24,7 +24,7 @@ Statement le_antisymm (x y : ℕ) (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
   rw [ha, add_assoc] at hb
   symm at hb
   apply add_right_eq_self at hb
-  apply eq_zero_of_add_right_eq_zero at hb
+  apply add_right_eq_zero at hb
   rw [hb, add_zero]
   rfl
 
@@ -39,7 +39,7 @@ rw [ha]
 rw [ha, add_assoc] at hb
 symm at hb
 apply add_right_eq_self at hb
-apply eq_zero_of_add_right_eq_zero at hb
+apply add_right_eq_zero at hb
 rw [hb, add_zero]
 rfl
 ```
diff --git a/Game/Levels/LessOrEqual/L08le_total.lean b/Game/Levels/LessOrEqual/L08le_total.lean
index a7dbf7b..05893bb 100644
--- a/Game/Levels/LessOrEqual/L08le_total.lean
+++ b/Game/Levels/LessOrEqual/L08le_total.lean
@@ -11,7 +11,13 @@ LemmaDoc MyNat.le_total as "le_total" in "≤" "
 "
 
 Introduction "
-This is I think the toughest level yet.
+This is I think the toughest level yet. Tips: if `a` is a number
+then `cases a with b` will split into cases `a = 0` and `a = succ b`.
+And don't go left or right until your hypotheses guarantee that
+you can prove the resulting goal!
+
+I've left hidden hints; if you need them, retry from the beginning
+and click on \"Show more help!\"
 "
 
 /-- If $x$ and $y$ are numbers, then either $x \leq y$ or $y \leq x$. -/
@@ -51,10 +57,5 @@ Very well done.
 A passing mathematician remarks that with you've just proved that `ℕ` is totally
 ordered.
 
-The next step in the development of order theory is to develop
-the theory of the interplay between `≤` and multiplication.
-If you've already done multiplication world, step into
-advanced multiplication world (once I've written it...)
+The final few levels in this world are much easier.
 "
-
--- **TODO** fix this
diff --git a/Game/Levels/LessOrEqual/L09le_of_succ_le_succ.lean b/Game/Levels/LessOrEqual/L09le_of_succ_le_succ.lean
new file mode 100644
index 0000000..2bd245d
--- /dev/null
+++ b/Game/Levels/LessOrEqual/L09le_of_succ_le_succ.lean
@@ -0,0 +1,39 @@
+import Game.Levels.LessOrEqual.L08le_total
+
+World "LessOrEqual"
+Level 9
+Title "succ x ≤ succ y → x ≤ y"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_of_succ_le_succ as "le_of_succ_le_succ" in "≤" "
+`le_of_succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`.
+"
+
+Introduction "
+The last goal in this world is to prove which numbers are `≤ 2`.
+This lemma will be helpful for that.
+"
+
+/-- If $\operatorname{succ}(x) \leq \operatorname{succ}(y)$ then $x \leq y$. -/
+Statement le_of_succ_le_succ (x y : ℕ) (hx : succ x ≤ succ y) : x ≤ y := by
+  cases hx with d hd
+  use d
+  rw [succ_add] at hd
+  apply succ_inj at hd
+  exact hd
+
+Conclusion "
+Here's my proof:
+```
+cases hx with d hd
+use d
+rw [succ_add] at hd
+apply succ_inj at hd
+exact hd
+```
+
+This lemma can be helpful for the next two levels.
+"
diff --git a/Game/Levels/LessOrEqual/L10le_one.lean b/Game/Levels/LessOrEqual/L10le_one.lean
new file mode 100644
index 0000000..b38fe55
--- /dev/null
+++ b/Game/Levels/LessOrEqual/L10le_one.lean
@@ -0,0 +1,46 @@
+import Game.Levels.LessOrEqual.L09le_of_succ_le_succ
+World "LessOrEqual"
+Level 10
+Title "x ≤ 1"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_one as "le_one" in "≤" "
+`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`.
+"
+
+Introduction "
+We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.
+Now we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`.
+"
+
+/-- If $x \leq 1$ then either $x = 0$ or $x = 1$. -/
+Statement le_one (x : ℕ) (hx : x ≤ 1) : x = 0 ∨ x = 1 := by
+  cases x with y
+  left
+  rfl
+  rw [one_eq_succ_zero] at hx ⊢
+  apply le_of_succ_le_succ at hx
+  apply le_zero at hx
+  rw [hx]
+  right
+  rfl
+
+Conclusion "
+Here's my proof:
+```
+cases x with y
+left
+rfl
+rw [one_eq_succ_zero] at hx ⊢
+apply le_of_succ_le_succ at hx
+apply le_zero at hx
+rw [hx]
+right
+rfl
+```
+
+If you solved this level then you should be fine with the next level!
+"
diff --git a/Game/Levels/LessOrEqual/L11le_two.lean b/Game/Levels/LessOrEqual/L11le_two.lean
new file mode 100644
index 0000000..02c1841
--- /dev/null
+++ b/Game/Levels/LessOrEqual/L11le_two.lean
@@ -0,0 +1,48 @@
+import Game.Levels.LessOrEqual.L10le_one
+World "LessOrEqual"
+Level 11
+Title "le_two"
+
+namespace MyNat
+
+LemmaTab "012"
+
+LemmaDoc MyNat.le_two as "le_two" in "≤" "
+`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`.
+"
+
+Introduction "
+We'll need this lemma to prove that two is prime!
+
+You'll need to know that `∨` is right associative. This means that
+`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`.
+"
+
+/-- If $x \leq 2$ then $x = 0$ or $1$ or $2$. -/
+Statement le_two (x : ℕ) (hx : x ≤ 2) : x = 0 ∨ x = 1 ∨ x = 2 := by
+  cases x with y
+  left
+  rfl
+  cases y with z
+  right
+  left
+  rw [one_eq_succ_zero]
+  rfl
+  rw [two_eq_succ_one, one_eq_succ_zero] at hx ⊢
+  apply le_of_succ_le_succ at hx
+  apply le_of_succ_le_succ at hx
+  apply le_zero at hx
+  rw [hx]
+  right
+  right
+  rfl
+
+
+Conclusion "
+Nice!
+
+The next step in the development of order theory is to develop
+the theory of the interplay between `≤` and multiplication.
+If you've already done Multiplication World, step into
+Advanced Multiplication World (once I've written it...)
+"
diff --git a/Game/Levels/LessOrEqual/inequality_world_tactic_notes.txt b/Game/Levels/LessOrEqual/inequality_world_tactic_notes.txt
index d91848d..b0fe688 100644
--- a/Game/Levels/LessOrEqual/inequality_world_tactic_notes.txt
+++ b/Game/Levels/LessOrEqual/inequality_world_tactic_notes.txt
@@ -1,21 +1,21 @@
 Function world:
-lvel 1 exact
+level 1 exact
 level 2 intro
-lwcwl 3 have
+level 3 have
 level 4 apply
 
 Prop world
-LEvel 1 exact again
+level 1 exact again
 level 2 intro
 level 3 have
 level 4 apply
-leevl 8 not P = P -> false (no explanation of false?)
+level 8 not P = P -> false (no explanation of false?)
 
 Advanced Prop world ;
 level 1 split
 level 2 rcases
 (for and)
-(note that level 1 is now consructor)
+(note that level 1 is now constructor)
 level 6 left and right
 level 9 exfalso (because \not is involved)
 level 10 by_cases
diff --git a/Game/Levels/Map.txt b/Game/Levels/Map.txt
index 9cb68c2..e9d5a6d 100644
--- a/Game/Levels/Map.txt
+++ b/Game/Levels/Map.txt
@@ -35,9 +35,9 @@ What about succ m ≤ succ n ↔ m ≤ n? This was a lost level (but not about <
 
 If a ≤ b then a + x ≤ b + x. And iff version?
 
-## Advanced Multiplication world: you can cancel muliplication
+## Advanced Multiplication world: you can cancel multiplication
 by nonzero x. ad+bc=ac+bd -> a=b or c=d? This should be preparation
-for divisilibity world.
+for divisibility world.
 
 ## Divisibility world
 
diff --git a/Game/Levels/OldAdvProposition/Level_3.lean b/Game/Levels/OldAdvProposition/Level_3.lean
index dfab36a..ae387b3 100644
--- a/Game/Levels/OldAdvProposition/Level_3.lean
+++ b/Game/Levels/OldAdvProposition/Level_3.lean
@@ -24,7 +24,7 @@ Statement --and_trans
   intro h
   rcases h with ⟨p, q⟩
   ```
-  i.e. introducing a new assumption and then immediately take it appart.
+  i.e. introducing a new assumption and then immediately take it apart.
 
   In that case you could do that in a single step:
 
diff --git a/Game/Levels/OldAdvProposition/Level_7.lean b/Game/Levels/OldAdvProposition/Level_7.lean
index 2539e52..175cd6f 100644
--- a/Game/Levels/OldAdvProposition/Level_7.lean
+++ b/Game/Levels/OldAdvProposition/Level_7.lean
@@ -51,5 +51,5 @@ Well done! Note that the syntax for `rcases` is different whether it's an \"or\"
 * `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.
+assumptions, once assuming the lefthand-side of the dismantled \"or\"-assumption, once the righthand-side.
 "
diff --git a/Game/Levels/Power/L01zero_pow_zero.lean b/Game/Levels/Power/L01zero_pow_zero.lean
index 041fe4d..d39a29e 100644
--- a/Game/Levels/Power/L01zero_pow_zero.lean
+++ b/Game/Levels/Power/L01zero_pow_zero.lean
@@ -44,8 +44,7 @@ convention that `0 ^ 0 = 1`.
 "
 
 /-- $0 ^ 0 = 1$ -/
-Statement zero_pow_zero
-    : (0 : ℕ) ^ 0  = 1 := by
+Statement zero_pow_zero : (0 : ℕ) ^ 0 = 1 := by
   rw [pow_zero]
   rfl
 
diff --git a/Game/Levels/Power/L03pow_one.lean b/Game/Levels/Power/L03pow_one.lean
index a955035..671b7a8 100644
--- a/Game/Levels/Power/L03pow_one.lean
+++ b/Game/Levels/Power/L03pow_one.lean
@@ -14,8 +14,7 @@ defined to be `a ^ 0 * a` so it's `1 * a`, and to prove
 that this is equal to `a` you need to use induction somewhere.
 "
 /-- For all naturals $a$, $a ^ 1 = a$. -/
-Statement pow_one
-    (a : ℕ) : a ^ 1 = a  := by
+Statement pow_one (a : ℕ) : a ^ 1 = a  := by
   rw [one_eq_succ_zero]
   rw [pow_succ]
   rw [pow_zero]
diff --git a/Game/Levels/Power/L06pow_add.lean b/Game/Levels/Power/L06pow_add.lean
index cc80c22..9293eca 100644
--- a/Game/Levels/Power/L06pow_add.lean
+++ b/Game/Levels/Power/L06pow_add.lean
@@ -6,7 +6,7 @@ Title "pow_add"
 
 namespace MyNat
 
-Introduction "Let's now begin our approch to the final boss,
+Introduction "Let's now begin our approach to the final boss,
 by proving some more subtle facts about powers."
 
 LemmaDoc MyNat.pow_add as "pow_add" in "^" "
diff --git a/Game/Levels/Power/L09add_sq.lean b/Game/Levels/Power/L09add_sq.lean
index b7ff479..10a0e1b 100644
--- a/Game/Levels/Power/L09add_sq.lean
+++ b/Game/Levels/Power/L09add_sq.lean
@@ -14,7 +14,7 @@ Introduction
 -- **TODO** get the `ring` hack working again.
 
 LemmaDoc MyNat.add_sq as "add_sq" in "^" "
-`add_sq a b` is the statment that $(a+b)^2=a^2+b^2+2ab.$
+`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$
 "
 
 /-- For all numbers $a$ and $b$, we have
diff --git a/Game/Levels/Tutorial/L03two_eq_ss0.lean b/Game/Levels/Tutorial/L03two_eq_ss0.lean
index 246b0b3..d654e8d 100644
--- a/Game/Levels/Tutorial/L03two_eq_ss0.lean
+++ b/Game/Levels/Tutorial/L03two_eq_ss0.lean
@@ -58,7 +58,8 @@ Similarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.
 This gives us plenty of numbers to be getting along with.
 
 The *proof* that `2 = succ 1` is called `two_eq_succ_one`.
-Check out the \"numerals\" tab in the list of lemmas on the right.
+Check out the \"012\" tab in the list of lemmas on the right
+for this and other proofs.
 
 Let's prove that $2$ is the number after the number after zero.
 "
diff --git a/Game/Levels/Tutorial/L07add_succ.lean b/Game/Levels/Tutorial/L07add_succ.lean
index 416b27a..8edbcf4 100644
--- a/Game/Levels/Tutorial/L07add_succ.lean
+++ b/Game/Levels/Tutorial/L07add_succ.lean
@@ -33,8 +33,9 @@ If you ever see `... + succ ...` in your goal, `rw [add_succ]` is
 normally a good idea.
 
 Let's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into
-the picture, and then `rw [add_succ]`. Use the Add and Numerals tabs to
-switch between lemmas so you can see which proofs you can rewrite.
+the picture, and then `rw [add_succ]`. Switch between the `+` (addition) and
+`012` (numerals) tabs under \"Theorems\" on the right to
+see which proofs you can rewrite.
 "
 
 /-- For all natural numbers $a$, we have $\operatorname{succ}(a) = a+1$. -/
diff --git a/Game/Metadata.lean b/Game/Metadata.lean
index 33dc9a5..76f9035 100644
--- a/Game/Metadata.lean
+++ b/Game/Metadata.lean
@@ -13,6 +13,7 @@ import Game.Tactic.Rfl
 import Game.Tactic.Rw
 import Game.Tactic.Apply
 import Game.Tactic.Use
+import Game.Tactic.Ne
 import Game.Tactic.Xyzzy
 -- import Std.Tactic.RCases
 -- import Game.Tactic.Have
diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean
index a3049dc..9cd4b23 100644
--- a/Game/MyNat/Addition.lean
+++ b/Game/MyNat/Addition.lean
@@ -2,11 +2,7 @@ import Game.MyNat.Definition
 
 namespace MyNat
 
-open MyNat
-
-def add : MyNat → MyNat → MyNat
-  | a, zero  => a
-  | a, MyNat.succ b => MyNat.succ (MyNat.add a b)
+opaque add : MyNat → MyNat → MyNat
 
 instance instAdd : Add MyNat where
   add := MyNat.add
@@ -17,11 +13,12 @@ instance instAdd : Add MyNat where
 `add_zero` is a `simp` lemma, because if you see `a + 0`
 you usually want to simplify it to `a`.
 -/
-@[simp]
-theorem add_zero (a : MyNat) : a + 0 = a := by rfl
+@[simp, MyNat_decide]
+axiom add_zero (a : MyNat) : a + 0 = a
 
 /--
 If `a` and `d` are natural numbers, then `add_succ a d` is the proof that
 `a + succ d = succ (a + d)`.
 -/
-theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
+@[MyNat_decide]
+axiom add_succ (a d : MyNat) : a + (succ d) = succ (a + d)
diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
index 88b8f4f..6257dab 100644
--- a/Game/MyNat/DecidableEq.lean
+++ b/Game/MyNat/DecidableEq.lean
@@ -1,7 +1,7 @@
-import Game.MyNat.Addition-- makes simps work?
 import Game.MyNat.PeanoAxioms
-import Game.Levels.Algorithm.L07succ_ne_succ
-import Mathlib.Tactic
+import Game.Levels.Algorithm.L07succ_ne_succ -- succ_ne_succ
+import Game.Tactic.decide -- modified decide tactic
+
 namespace MyNat
 
 instance instDecidableEq : DecidableEq MyNat
diff --git a/Game/MyNat/DecidableTests.lean b/Game/MyNat/DecidableTests.lean
new file mode 100644
index 0000000..fe512a5
--- /dev/null
+++ b/Game/MyNat/DecidableTests.lean
@@ -0,0 +1,29 @@
+import Game.MyNat.DecidableEq
+import Game.MyNat.Power
+
+example : 4 = 4 := by
+  decide
+
+example : 4 ≠ 5 := by
+  decide
+
+example : (0 : ℕ) + 0 = 0 := by
+  decide
+
+example : (2 : ℕ) + 2 = 4 := by
+  decide
+
+example : (2 : ℕ) + 2 ≠ 5 := by
+  decide
+
+example : (20 : ℕ) + 20 = 40 := by
+  decide
+
+example : (2 : ℕ) * 2 = 4 := by
+  decide
+
+example : (2 : ℕ) * 2 ≠ 5 := by
+  decide
+
+example : (3 : ℕ) ^ 2 ≠ 37 := by
+  decide
diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean
index 3034fbd..2270acb 100644
--- a/Game/MyNat/Definition.lean
+++ b/Game/MyNat/Definition.lean
@@ -1,3 +1,5 @@
+import Game.Tactic.LabelAttr -- MyNat_decide attribute
+
 /-- Our copy of the natural numbers called `MyNat`, with notation `ℕ`. -/
 inductive MyNat where
 | zero : MyNat
@@ -13,26 +15,25 @@ namespace MyNat
 instance : Inhabited MyNat where
   default := MyNat.zero
 
-def myNatFromNat (x : Nat) : MyNat :=
+@[MyNat_decide]
+def ofNat (x : Nat) : MyNat :=
   match x with
   | Nat.zero   => MyNat.zero
-  | Nat.succ b => MyNat.succ (myNatFromNat b)
+  | Nat.succ b => MyNat.succ (ofNat b)
 
-def natFromMyNat (x : MyNat) : Nat :=
+@[MyNat_decide]
+def toNat (x : MyNat) : Nat :=
   match x with
   | MyNat.zero   => Nat.zero
-  | MyNat.succ b => Nat.succ (natFromMyNat b)
+  | MyNat.succ b => Nat.succ (toNat b)
 
-instance ofNat {n : Nat} : OfNat MyNat n where
-  ofNat := myNatFromNat n
+instance instofNat {n : Nat} : OfNat MyNat n where
+  ofNat := ofNat n
 
 instance : ToString MyNat where
-  toString p := toString (natFromMyNat p)
+  toString p := toString (toNat p)
 
+@[MyNat_decide]
 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/Game/MyNat/LE.lean b/Game/MyNat/LE.lean
index 41672a6..a4ef4bd 100644
--- a/Game/MyNat/LE.lean
+++ b/Game/MyNat/LE.lean
@@ -15,8 +15,7 @@ def le (a b : ℕ) :=  ∃ (c : ℕ), b = a + c
 -- 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
+-- We don't use this any more; I tell the users `≤` is *notation*
+-- theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c := Iff.rfl
 
 end MyNat
diff --git a/Game/MyNat/Multiplication.lean b/Game/MyNat/Multiplication.lean
index f3fb6ff..6ff858a 100644
--- a/Game/MyNat/Multiplication.lean
+++ b/Game/MyNat/Multiplication.lean
@@ -2,13 +2,13 @@ import Game.MyNat.Addition
 
 namespace MyNat
 
-def mul : MyNat → MyNat → MyNat
-  | _, 0   => 0
-  | a, b + 1 => (MyNat.mul a b) + a
+opaque mul : MyNat → MyNat → MyNat
 
 instance : Mul MyNat where
   mul := MyNat.mul
 
-theorem mul_zero (a : MyNat) : a * 0 = 0 := by rfl
+@[MyNat_decide]
+axiom mul_zero (a : MyNat) : a * 0 = 0
 
-theorem mul_succ (a b : MyNat) : a * (succ b) = a * b + a := by rfl
+@[MyNat_decide]
+axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a
diff --git a/Game/MyNat/PeanoAxioms.lean b/Game/MyNat/PeanoAxioms.lean
index 424f68a..a96a9a4 100644
--- a/Game/MyNat/PeanoAxioms.lean
+++ b/Game/MyNat/PeanoAxioms.lean
@@ -21,7 +21,7 @@ theorem succ_inj (a b : ℕ) (h : succ a = succ b) : a = b := by
 
 def is_zero : ℕ → Prop
 | 0 => True
-| succ n => False
+| succ _ => False
 
 lemma is_zero_zero : is_zero 0 = True := rfl
 lemma is_zero_succ (n : ℕ) : is_zero (succ n) = False := rfl
diff --git a/Game/MyNat/Power.lean b/Game/MyNat/Power.lean
index 1d31cef..1031fc0 100644
--- a/Game/MyNat/Power.lean
+++ b/Game/MyNat/Power.lean
@@ -3,21 +3,19 @@ import Game.MyNat.Multiplication
 namespace MyNat
 open MyNat
 
-def pow : ℕ → ℕ → ℕ
-| _, zero => one
-| m, (succ n) => pow m n * m
+opaque pow : ℕ → ℕ → ℕ
 
+-- notation `a ^ b` for `pow a b`
 instance : Pow ℕ ℕ where
   pow := pow
 
--- notation a ^ b := pow a b
+-- Note: since v4.2.0-rc2
+macro_rules | `($x ^ $y)   => `(HPow.hPow ($x : MyNat) ($y : MyNat))
 
--- Important note: This here is the real `rfl`, not the weaker game version
+@[MyNat_decide]
+axiom pow_zero (m : ℕ) : m ^ 0 = 1
 
-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
+@[MyNat_decide]
+axiom pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m
 
 end MyNat
diff --git a/Game/Tactic/LabelAttr.lean b/Game/Tactic/LabelAttr.lean
new file mode 100644
index 0000000..222ba3b
--- /dev/null
+++ b/Game/Tactic/LabelAttr.lean
@@ -0,0 +1,5 @@
+import Std.Tactic.LabelAttr
+import Mathlib.Lean.Meta.Simp
+
+/-- Simp set for `functor_norm` -/
+register_simp_attr MyNat_decide
diff --git a/Game/Tactic/Ne.lean b/Game/Tactic/Ne.lean
new file mode 100644
index 0000000..b076f03
--- /dev/null
+++ b/Game/Tactic/Ne.lean
@@ -0,0 +1,15 @@
+import Lean
+
+/-!
+A pretty-printer that displays `¬ (a = b)` as `a ≠ b`.
+-/
+
+open Lean PrettyPrinter Delaborator SubExpr
+
+@[delab app.Not] def delab_not_mem :=
+  whenPPOption Lean.getPPNotation do
+  let #[f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.getAppFn matches .const `Eq _ do failure
+  let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 1 delab
+  let stx₂ ← SubExpr.withAppArg <| SubExpr.withNaryArg 2 delab
+  return ← `($stx₁ ≠ $stx₂)
diff --git a/Game/Tactic/decide.lean b/Game/Tactic/decide.lean
new file mode 100644
index 0000000..af7ce1d
--- /dev/null
+++ b/Game/Tactic/decide.lean
@@ -0,0 +1,16 @@
+import Game.Tactic.LabelAttr
+import Game.MyNat.Definition
+
+-- to get numerals of type MyNat to reduce to MyNat.succ (MyNat.succ ...)
+@[MyNat_decide]
+theorem ofNat_succ : (OfNat.ofNat (Nat.succ n) : ℕ) = MyNat.succ (OfNat.ofNat n) := _root_.rfl
+
+
+/- modified `decide` tactic which first runs a custom
+simp call to reduce numerals like `1 + 1` to
+`MyNat.succ (MyNat.succ MyNat.zero)
+-/
+macro "decide" : tactic => `(tactic|(
+  try simp only [MyNat_decide]
+  try decide
+))
diff --git a/README.md b/README.md
index 986e349..d50c1ed 100644
--- a/README.md
+++ b/README.md
@@ -1,60 +1,24 @@
 # NNG4
 
-This is the lean4 version of the classical *Natural Number Game*. It uses the [Lean4 Game Engine](https://github.com/leanprover-community/lean4game) and is running live at [adam.math.hhu.de](https://adam.math.hhu.de/#/game/nng).
+This is the lean4 version of the classical *Natural Number Game*. It uses
+the [Lean4 Game Engine](https://github.com/leanprover-community/lean4game) and is
+running live at [adam.math.hhu.de](https://adam.math.hhu.de).
 
 The game was initially designed for lean3 and has been adapted for lean4. [See lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/).
 
 ## Getting Started
 
-There are multiple ways to run the game while developing it:
-
-### VSCode Devcontainer
-
-The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#running-games-locally).
-In particular, the recommended setup is to have `docker` installed on your computer
-and then click on the pop-up "Reopen in Container" which is shown when
-opening this project in VSCode.
-
-You can then open [localhost:3000](http://localhost:3000) in a browser.
-
-After making changes to the code, you need to run `lake build` in a terminal and
-reload the web page inside the "Simple Browser".
-
-### Codespaces
-
-You can work on it using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for for example under "Ports" and clicking on
-"Open in Browser".
-
-Note: You have to wait until `npm` started properly.
-In particular, this is after a message like
-`[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while.
-
-As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser.
-
-### Local setup
-
-The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#running-games-locally).
-In particular, the recommended setup is to have `docker` installed on your computer
-and then click on the pop-up "Reopen in Container" which is shown when
-opening this project in VSCode.
-
-The game is then accessible at [localhost:3000/#/g/local/game](http://localhost:3000/#/g/local/game).
-
-### Gitpod
-
-You can work on this repository using Gitpod : [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/hhu-adam/NNG4)
-
-Note that gitpod is *not* setup to start the game in the background to play.
-
+You can develop the game as any lean project and use `lake build` to build it.
 
+Moreover, there are multiple ways to run the game while developing it, which are described in
+[Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
 
 ## Contributing
 
-If you want to contribute to the Natural Number Game, it is probably best if you ask us for access and push on a non-`main` branch in this repo. That way a github-action will build the game automatically.
-
-See the [documentation](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md) for an explanation of the game commands.
-
+PRs/Issues fixing typos, inconsistencies, missing hints, etc. are very welcome!
 
-## Creating a new game
+## Documentation
 
-In order to create a new game, click "use this template"  above to create your own game. That way there is a github action that can build a docker image from your `main` branch which can be used to add the game to the server at [adam.math.hhu.de](https://adam.math.hhu.de).
+See [Creating a Game](https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md) at
+the [lean4game repo](https://github.com/leanprover-community/lean4game) for a detailed
+explanation.
diff --git a/README_gitpod.md b/README_gitpod.md
deleted file mode 100644
index a7afb8f..0000000
--- a/README_gitpod.md
+++ /dev/null
@@ -1,20 +0,0 @@
-### Remote running via GitPod
-
-You don't need to install anything onto your computer using this method.
-
-Just click here: [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/kbuzzard/IISc-experiments)
-
-Note to self: I got gitpod working by adding the files `.gitpod.yml` and `.docker/gitpod/Dockerfile`
-
-### Remote running via Codespaces
-
-You don't need to install anything onto your computer using this method.
-
-Go to the project's [home page on GitHub](https://github.com/kbuzzard/IISc-experiments),
-click "Code" and then "Codespaces" so it looks like this:
-
-Pic: ![codespaces installation](png/codespaces.png?raw=true "codespaces installation")
-
-Then click "create codespace on main", and then wait for a few minutes. When it looks like everything has downloaded, open up the `IIScExperiments` directory (not the file!) and the code I've been using in the lectures should just work.
-
-Note to self: I got codespaces working by adding the files `.devcontainer/devcontainer.json` and `.devcontainer/Dockerfile`.
diff --git a/images/cover.png b/images/cover.png
new file mode 100644
index 0000000..69b0df5
Binary files /dev/null and b/images/cover.png differ
diff --git a/lake-manifest.json b/lake-manifest.json
index 0d661ab..0331f48 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,60 +1,68 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "f203f2e0caf1d9ea25b7f2e4b8c2afebd2c6967b",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": "v4.1.0",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/lean4game.git",
-    "subDir?": "server",
-    "rev": "bda1f98693ac3f143c5757e61b30892dc26d4c95",
-    "opts": {},
-    "name": "GameServer",
-    "inputRev?": "main",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
-    "subDir?": null,
-    "rev": "21dac2e9cc7e3cf7da5800814787b833e680b2fd",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/JLimperg/aesop",
-    "subDir?": null,
-    "rev": "1a0cded2be292b5496e659b730d2accc742de098",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.16",
-    "inherited": true}}],
- "name": "Game"}
+ [{"url": "https://github.com/leanprover/std4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean4game.git",
+   "type": "git",
+   "subDir": "server",
+   "rev": "d5697d052e5154b909f379073a591ebf66eb3e22",
+   "name": "GameServer",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.23",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.3.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Game",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index b0735c6..bbbd889 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,6 +1,9 @@
 import Lake
 open Lake DSL
 
+-- Using this assumes that each dependency has a tag of the form `v4.X.0`.
+def leanVersion : String := s!"v{Lean.versionString}"
+
 def LocalGameServer : Dependency := {
   name := `GameServer
   src := Source.path "../lean4game/server"
@@ -8,27 +11,44 @@ def LocalGameServer : Dependency := {
 
 def RemoteGameServer : Dependency := {
   name := `GameServer
-  src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
+  src := Source.git "https://github.com/leanprover-community/lean4game.git" leanVersion "server"
 }
 
-/- Choose dependency depending on the environment variable NODE_ENV -/
+/- Choose GameServer dependency depending on the environment variable `LEAN4GAME`. -/
 open Lean in
 #eval (do
-  let gameServerName :=
-    if (← IO.getEnv "NODE_ENV") == some "development" then ``LocalGameServer else ``RemoteGameServer
+  let gameServerName := if get_config? lean4game.local |>.isSome then
+    ``LocalGameServer else ``RemoteGameServer
   modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
-   : Elab.Command.CommandElabM Unit)
+  : Elab.Command.CommandElabM Unit)
+
+/-! # USER SECTION
+
+Below are all the dependencies the game needs. Add or remove packages here as you need them.
+
+Note: If your package (like `mathlib` or `Std`) has tags of the form `v4.X.0` then
+you can use `require mathlib from git "[URL]" @ leanVersion`
+ -/
+
+
+
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ leanVersion
+
+
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "v4.1.0"
+/-! # END USER SECTION -/
 
 -- NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and
 -- off when calling `lake build`. Ideally there would be a better way using `logInfo` and
 -- an option like `lean4game.verbose`.
 package Game where
-  moreLeanArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=false",
+  moreLeanArgs := #[
+    "-Dtactic.hygienic=false",
+    "-Dlinter.unusedVariables.funArgs=false",
     "-Dtrace.debug=false"]
-  moreServerArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=true",
+  moreServerArgs := #[
+    "-Dtactic.hygienic=false",
+    "-Dlinter.unusedVariables.funArgs=true",
     "-Dtrace.debug=true"]
   weakLeanArgs := #[]
 
diff --git a/lean-toolchain b/lean-toolchain
index f8f5f5c..5cadc9d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.1.0
+leanprover/lean4:v4.3.0
diff --git a/test/ne.lean b/test/ne.lean
new file mode 100644
index 0000000..277f567
--- /dev/null
+++ b/test/ne.lean
@@ -0,0 +1,14 @@
+import Game.Metadata
+
+example (a : ℕ) : a = 0 ∨ ¬ (a = 0) := by
+  by_cases h : a = 0
+  · left
+    exact h
+  · right
+    -- here the goal should show `h : a ≠ 0`
+    exact h
+
+-- set_option pp.all true in
+example (a : ℕ) : ¬ (a = 0) ↔ a ≠ 0 := by
+  -- both should be displayed the same way
+  rfl