diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index a521364..8a3b211 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -244,17 +244,31 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
   | some name =>
     let env ← getEnv
     if env.contains name.getId then
-      logWarningAt name s!"Environment already contains {name.getId}! Only the existing statement will be available in later levels."
-      -- TODO: Check if the two agree. turn into `logInfo` in that case.
-      -- let origType := (env.constants.map₁.find! name.getId).type
-      -- -- let newType := (env.constants.map₁.find! defaultDeclName).type
+      let origType := (env.constants.map₁.find! name.getId).type
+      -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
+      -- in that case.
+      logWarningAt name m!"Environment already contains {name.getId}!
+Only the existing statement will be available in later levels:
+
+{origType}"
+      -- let (binders, typeStx) := expandDeclSig sig
+      -- --let type ← Term.elabType typeStx
+      -- runTermElabM (fun vars =>
+      --   Term.elabBinders binders.getArgs (fun xs => do
+      --   let type ← Term.elabType typeStx
+      --   --Term.synthesizeSyntheticMVarsNoPostponing
+      --   --let type ← instantiateMVars type
+      --   --let type ← mkForallFVars xs type
+      -- ))
+      --let newType := Term.elabTerm sig.raw
+      --dbg_trace newType
+      --logInfo origType
       -- dbg_trace sig
       -- dbg_trace origType
       --dbg_trace (env.constants.map₁.find! name.getId).value! -- that's the proof
       --let newType := Lean.Elab.Term.elabTerm sig none
 
       let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
-      dbg_trace thmStatement
       elabCommand thmStatement
     else
       let thmStatement ← `(theorem $(mkIdent name.getId) $sig $val)
diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean
index 84d07b5..8b75036 100644
--- a/server/nng/NNG.lean
+++ b/server/nng/NNG.lean
@@ -17,7 +17,7 @@ Introduction
 "
 # Natural Number Game
 
-##### version 2.0.1
+##### version 3.0.1
 
 Welcome to the natural number game -- a game which shows the power of induction.
 
@@ -45,12 +45,13 @@ If you delete it, your progress will be lost!
 
 ## Credits
 
-* **Content and Lean3-version:** Kevin Buzzard, Mohammad Pedramfar
+* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar
+* **Content adaptation**: Jon Eugster
 * **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot
 
 ## Resources
 
-* The [Lean Zulip chat] forum
+* 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)
 
diff --git a/server/nng/NNG/Doc/Definitions.lean b/server/nng/NNG/Doc/Definitions.lean
index ec56a79..8a1d6c4 100644
--- a/server/nng/NNG/Doc/Definitions.lean
+++ b/server/nng/NNG/Doc/Definitions.lean
@@ -3,4 +3,12 @@ import GameServer.Commands
 DefinitionDoc MyNat as "ℕ"
 "
 The Natural Numbers.
+
+## 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`.
 "
\ No newline at end of file
diff --git a/server/nng/NNG/Doc/Tactics.lean b/server/nng/NNG/Doc/Tactics.lean
index e0b50a3..5712775 100644
--- a/server/nng/NNG/Doc/Tactics.lean
+++ b/server/nng/NNG/Doc/Tactics.lean
@@ -2,6 +2,34 @@ 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 rewrite
@@ -10,6 +38,83 @@ TacticDoc rewrite
 
 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`) and
+`rw h at h2` (changes `X` to `Y` in hypothesis `h2` instead
+of the goal).
+
+## 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:
+
+```
+  x y : ℕ
+  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 `refl,`.
+
+### Example:
+
+You can use `rw` to change a hypothesis as well.
+For example, if your local context looks like this:
+
+```
+  x y : ℕ
+  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
diff --git a/server/nng/NNG/Levels/Tutorial.lean b/server/nng/NNG/Levels/Tutorial.lean
index 5fcd9a3..9efc7d0 100644
--- a/server/nng/NNG/Levels/Tutorial.lean
+++ b/server/nng/NNG/Levels/Tutorial.lean
@@ -9,4 +9,7 @@ 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
index 13a6d5b..7c0749e 100644
--- a/server/nng/NNG/Levels/Tutorial/Level_1.lean
+++ b/server/nng/NNG/Levels/Tutorial/Level_1.lean
@@ -10,14 +10,14 @@ 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
-$x \\cdot y + z = x \\cdot y + z$ (displayed under \"Goal\").
+$xy + z = xy + z$ (displayed under \"Goal\").
 
-You can modify the Goal using *Tactics* until you can close (i.e. prove) it. 
+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 (a computer scientist would say \"definitionally equal\"). I really mean \"press the same buttons
+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.
 "
diff --git a/server/nng/NNG/Levels/Tutorial/Level_2.lean b/server/nng/NNG/Levels/Tutorial/Level_2.lean
index a17243e..4178943 100644
--- a/server/nng/NNG/Levels/Tutorial/Level_2.lean
+++ b/server/nng/NNG/Levels/Tutorial/Level_2.lean
@@ -33,11 +33,11 @@ Statement
   "Now both sides are identical, so you can use `rfl` to close the goal."
   rfl
 
-NewTactic rewrite rw
+NewTactic rw
 
 Conclusion
 "
-If you want to see the entire proof you created, toggle \"Editor mode\" above.
+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.
 
diff --git a/server/nng/NNG/MyNat/Addition.lean b/server/nng/NNG/MyNat/Addition.lean
index 9f482f4..46be116 100644
--- a/server/nng/NNG/MyNat/Addition.lean
+++ b/server/nng/NNG/MyNat/Addition.lean
@@ -21,3 +21,6 @@ theorem add_zero (a : MyNat) : a + 0 = a := by rfl
 This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat.
 -/
 theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
+
+-- TODO: testing. Remove me
+axiom zero_add (n : ℕ) : 0 + n = n