diff --git a/Game/Levels/Addition/L02succ_add.lean b/Game/Levels/Addition/L02succ_add.lean
index d76f8ba..6423ad6 100644
--- a/Game/Levels/Addition/L02succ_add.lean
+++ b/Game/Levels/Addition/L02succ_add.lean
@@ -36,7 +36,7 @@ Statement succ_add (a b : ℕ) : succ a + b = succ (a + b)  := by
     rw [add_zero]
     rfl
   · Hint "Note that `succ a + {d}` means `(succ a) + {d}`. Put your cursor
-  on any `succ` in the goal to see what exactly it's eating."
+  on any `succ` in the goal or assumptions to see what exactly it's eating."
     rw [add_succ, add_succ, hd]
     rfl
 
diff --git a/Game/Levels/Addition/L05add_right_comm.lean b/Game/Levels/Addition/L05add_right_comm.lean
index b817e9f..2cd1d8e 100644
--- a/Game/Levels/Addition/L05add_right_comm.lean
+++ b/Game/Levels/Addition/L05add_right_comm.lean
@@ -16,6 +16,11 @@ is no `b + c` term *directly* in the goal.
 Use associativity and commutativity to prove `add_right_comm`.
 You don't need induction. `add_assoc` moves brackets around,
 and `add_comm` moves variables around.
+
+Remember that you can do more targetted rewrites by
+adding explicit variables as inputs to theorems. For example `rw [add_comm b]`
+will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`
+will only do rewrites of the form `b + c = c + b`.
 "
 
 LemmaDoc MyNat.add_right_comm as "add_right_comm" in "Add"
@@ -28,10 +33,6 @@ as `a + b + c = a + c + b`."
 $(a + b) + c = (a + c) + b$. -/
 Statement add_right_comm (a b c : ℕ) : a + b + c = a + c + b := by
   rw [add_assoc]
-  Hint "Remember that you can do more targetted rewrites by
-  adding explicit variables as inputs to theorems. For example `rw [add_comm b]`
-  will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`
-  will only do rewrites of the form `b + c = c + b`."
   rw [add_comm b, add_assoc]
   rfl
 
diff --git a/Game/Levels/AdvAddition/L05add_right_eq_self.lean b/Game/Levels/AdvAddition/L05add_right_eq_self.lean
index 5e6fa94..df0865e 100644
--- a/Game/Levels/AdvAddition/L05add_right_eq_self.lean
+++ b/Game/Levels/AdvAddition/L05add_right_eq_self.lean
@@ -21,9 +21,7 @@ Two ways to do it spring to mind; I'll mention them when you've solved it.
 /-- $x+y=x\implies y=0$. -/
 Statement add_right_eq_self (x y : ℕ) : x + y = x → y = 0 := by
   rw [add_comm]
-  intro h
-  apply add_left_eq_self at h
-  exact h
+  exact add_left_eq_self y x
 
 Conclusion "Here's a proof using `add_left_eq_self`:
 ```
@@ -33,6 +31,12 @@ apply add_left_eq_self at h
 exact h
 ```
 
+and here's an even shorter one using the same idea:
+```
+rw [add_comm]
+exact add_left_eq_self y x
+```
+
 Alternatively you can just prove it by induction on `x`
 (the dots in the proof just indicate the two goals and
 can be omitted):
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
index 4daf066..14eb660 100644
--- a/Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean
+++ b/Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean
@@ -77,3 +77,5 @@ Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
   symm at h
   apply zero_ne_succ at h
   contradiction
+
+Conclusion "Well done!"
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
index 0833b37..af8f0bc 100644
--- a/Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean
+++ b/Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean
@@ -26,8 +26,8 @@ Conclusion "How about this for a proof:
 
 ```
 rw [add_comm]
-exact eq_zero_of_add_left_eq_zero b a
+exact eq_zero_of_add_right_eq_zero b a
 ```
 
-You're now ready for LessThanOrEqual World.
+You're now ready for `≤` World.
 "
diff --git a/Game/Levels/Implication/L01exact.lean b/Game/Levels/Implication/L01exact.lean
index e72b213..69347ef 100644
--- a/Game/Levels/Implication/L01exact.lean
+++ b/Game/Levels/Implication/L01exact.lean
@@ -38,6 +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.\"
 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
diff --git a/Game/Levels/Implication/L03apply.lean b/Game/Levels/Implication/L03apply.lean
index 6b8ca91..4f9f870 100644
--- a/Game/Levels/Implication/L03apply.lean
+++ b/Game/Levels/Implication/L03apply.lean
@@ -45,5 +45,5 @@ hypothesis with the `apply` tactic.
 Statement (x y : ℕ) (h1 : x = 37) (h2 : x = 37 → y = 42) : y = 42 := by
   Hint "Start with `apply h2 at h1`. This will change `h1` to `y = 42`."
   apply h2 at h1
-  Hint "Now finish using `exact`."
+  Hint "Now finish using the `exact` tactic."
   exact h1
diff --git a/Game/Levels/Implication/L04succ_inj.lean b/Game/Levels/Implication/L04succ_inj.lean
index fa0f8fb..822ef68 100644
--- a/Game/Levels/Implication/L04succ_inj.lean
+++ b/Game/Levels/Implication/L04succ_inj.lean
@@ -52,8 +52,8 @@ NewLemma MyNat.succ_inj
 /-- If $x+1=4$ then $x=3$. -/
 Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
   Hint "Let's first get `h` into the form `succ x = succ 3` so we can
-  apply `succ_inj`. First rewrite
-  `four_eq_succ_three` at `h` to change the 4 on the right hand side."
+  apply `succ_inj`. First execute `rw [four_eq_succ_three] at h`
+  to change the 4 on the right hand side."
   rw [four_eq_succ_three] at h
   Hint "Now rewrite `succ_eq_add_one` backwards at `h`
   to get the right hand side."
diff --git a/Game/Levels/Implication/L10one_ne_zero.lean b/Game/Levels/Implication/L10one_ne_zero.lean
index 93b5e4f..289cfba 100644
--- a/Game/Levels/Implication/L10one_ne_zero.lean
+++ b/Game/Levels/Implication/L10one_ne_zero.lean
@@ -35,7 +35,7 @@ If `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`.
 
 NewTactic symm
 
-/-- $0\neq1$. -/
+/-- $1\neq0$. -/
 Statement : (1 : ℕ) ≠ 0 := by
   symm
   exact zero_ne_one
diff --git a/Game/Levels/LessOrEqual/L01le_refl.lean b/Game/Levels/LessOrEqual/L01le_refl.lean
index bc94ba4..eb46e53 100644
--- a/Game/Levels/LessOrEqual/L01le_refl.lean
+++ b/Game/Levels/LessOrEqual/L01le_refl.lean
@@ -40,8 +40,6 @@ LemmaDoc MyNat.le_refl as "le_refl" in "≤" "
 The reason for the name is that this lemma is \"reflexivity of $\\le$\"
 "
 
-NewLemma MyNat.le_refl
-
 /-- If $x$ is a number, then $x \le x$. -/
 Statement le_refl (x : ℕ) : x ≤ x := by
   Hint "The reason `x ≤ x` is because `x = x + 0`.
diff --git a/Game/Levels/LessOrEqual/L02zero_le.lean b/Game/Levels/LessOrEqual/L02zero_le.lean
index 1ed6e0b..a272eba 100644
--- a/Game/Levels/LessOrEqual/L02zero_le.lean
+++ b/Game/Levels/LessOrEqual/L02zero_le.lean
@@ -15,8 +15,6 @@ LemmaDoc MyNat.zero_le as "zero_le" in "≤" "
 `zero_le x` is a proof that `0 ≤ x`.
 "
 
-NewLemma MyNat.zero_le
-
 /-- If $x$ is a number, then $0 \le x$. -/
 Statement zero_le (x : ℕ) : 0 ≤ x := by
   use x
diff --git a/Game/Levels/LessOrEqual/L03le_succ_self.lean b/Game/Levels/LessOrEqual/L03le_succ_self.lean
index 5289121..8a52205 100644
--- a/Game/Levels/LessOrEqual/L03le_succ_self.lean
+++ b/Game/Levels/LessOrEqual/L03le_succ_self.lean
@@ -10,8 +10,6 @@ LemmaDoc MyNat.le_succ_self as "le_succ_self" in "≤" "
 `le_succ_self x` is a proof that `x ≤ succ x`.
 "
 
-NewLemma MyNat.le_succ_self
-
 Introduction "If you `use` the wrong number, you get stuck with a goal you can't prove.
 What number will you `use` here?"
 
diff --git a/Game/Levels/LessOrEqual/L05le_zero.lean b/Game/Levels/LessOrEqual/L05le_zero.lean
index feb6d67..b987cea 100644
--- a/Game/Levels/LessOrEqual/L05le_zero.lean
+++ b/Game/Levels/LessOrEqual/L05le_zero.lean
@@ -22,9 +22,8 @@ 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 "Now `y` is what you have to add to `x` to get `0`, and `hy` is the proof of this."
   Hint (hidden := true) "You want to use `eq_zero_of_add_right_eq_zero`, which you already
-  proved, but you'll have to start with `symm at hy`."
+  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
   exact hy
diff --git a/Game/Levels/LessOrEqual/L08le_total.lean b/Game/Levels/LessOrEqual/L08le_total.lean
index b95cd26..a7eae68 100644
--- a/Game/Levels/LessOrEqual/L08le_total.lean
+++ b/Game/Levels/LessOrEqual/L08le_total.lean
@@ -10,8 +10,6 @@ LemmaDoc MyNat.le_total as "le_total" in "≤" "
 `le_total x y` is a proof that `x ≤ y` or `y ≤ x`.
 "
 
-NewLemma MyNat.le_total
-
 Introduction "
 This is I think the toughest level yet.
 "
@@ -30,7 +28,7 @@ Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
   use e + 1
   rw [succ_eq_add_one, add_assoc]
   rfl
-  Hint (hidden := true) "Now `cases h2 with e h2`."
+  Hint (hidden := true) "Now `cases h2 with e he`."
   cases h2 with e h2
   Hint (hidden := true) "You still don't know which way to go, so do `cases e with a`."
   cases e with a
@@ -48,9 +46,15 @@ Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
 LemmaTab "≤"
 
 Conclusion "
+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...)
 "
 
--- **TODO** add "if you want to prove it's a totally ordered ring, go
--- to advanced mult world"
+-- **TODO** fix this
diff --git a/Game/Levels/Tutorial/L05add_zero.lean b/Game/Levels/Tutorial/L05add_zero.lean
index a148a62..5de30cf 100644
--- a/Game/Levels/Tutorial/L05add_zero.lean
+++ b/Game/Levels/Tutorial/L05add_zero.lean
@@ -80,12 +80,11 @@ Let's start with adding `0`.
 To make addition agree with our intuition, we should *define* `37 + 0`
 to be `37`. More generally, we should define `a + 0` to be `a` for
 any number `a`. The name of this proof in Lean is `add_zero a`.
+For example `add_zero 37` is a proof of `37 + 0 = 37`,
+`add_zero x` is a proof of `x + 0 = x`, and `add_zero` is a proof
+of `? + 0 = ?`.
 
-* `add_zero 37 : 37 + 0 = 37`
-
-* `add_zero a : a + 0 = a`
-
-*` add_zero : ? + 0 = ?`
+We write `add_zero x : x + 0 = x`, so `proof : statement`.
 "
 
 /-- $a+(b+0)+(c+0)=a+b+c.$ -/
diff --git a/Game/Levels/Tutorial/L06add_zero2.lean b/Game/Levels/Tutorial/L06add_zero2.lean
index 62c6b59..528b65d 100644
--- a/Game/Levels/Tutorial/L06add_zero2.lean
+++ b/Game/Levels/Tutorial/L06add_zero2.lean
@@ -25,7 +25,7 @@ Statement (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
   rw [add_zero c]
   Hint "`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.
   You can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You
-  can usually stick to `add_zero` unless you need real precision."
+  can usually stick to `rw [add_zero]` unless you need real precision."
   rw [add_zero]
   rfl
 
diff --git a/Game/Levels/Tutorial/L08twoaddtwo.lean b/Game/Levels/Tutorial/L08twoaddtwo.lean
index 3ef8a0d..c77d26d 100644
--- a/Game/Levels/Tutorial/L08twoaddtwo.lean
+++ b/Game/Levels/Tutorial/L08twoaddtwo.lean
@@ -65,7 +65,7 @@ on the `</>` button in the top right. You can now see your proof
 written as several lines of code. Move your cursor between lines to see
 the goal state at any point. Now cut and paste your code elsewhere if you
 want to save it, and paste the above proof in instead. Move your cursor
-around to investigate. When you've finished, click the `>_` button to
+around to investigate. When you've finished, click the `>_` button in the top right to
 move back into command line mode.
 
 You have finished tutorial world! Now let's move onto Addition World,