sort out succ_eq_add_one import issue for hopefully the last time

Game/Levels/Addition.lean

@@ -17,6 +17,6 @@ beat all the levels in Addition World, Multiplication World, and Power World.
 Power World contains the final boss of the game.
 
 There are plenty more tactics in this game, but you'll only need to know them if you
-decide you want to explore the game further (for example if you want to 100%
+want to explore the game further (for example if you decide to 100%
 the game).
 "

Game/Levels/Addition/L01zero_add.lean

@@ -1,9 +1,10 @@
 import Game.Metadata
 import Game.MyNat.Addition
-import Game.MyNat.DecidableEq
-
--- try to fix tutorial world entry page text issue
+import Game.Levels.Tutorial
+-- note that
 -- import Game.Levels.Tutorial.L05add_succ
+-- breaks the game server -- text disappears from
+-- tutorial world intro level!
 
 World "Addition"
 Level 1
@@ -43,7 +44,8 @@ Statement zero_add (n : ℕ) : 0 + n = n := by
   · 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."
+    Recall that you can rewrite the proof of any lemma which is visible
+    in your inventory, or of any assumption displayed above the goal."
     Hint (hidden := true) "try rewriting `add_zero`."
     rw [add_zero]
     rfl
@@ -65,16 +67,8 @@ If `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d h
 attempts to prove the goal by induction on `n`, with the inductive
 variable in the successor case being `d`, and the inductive hypothesis being `hd`.
 
-## Details
-
-If you have a natural number `n : ℕ` in your assumptions
-then `induction n with d hd` turns your
-goal into two goals, a base case with `n = 0` and
-an inductive step where `hd` is a proof of the `n = d`
-case and your goal is the `n = succ d` case.
-
 ### Example:
-If our goal is
+If the goal is
 ```
 0 + n = n
 ```
@@ -83,11 +77,12 @@ then
 
 `induction n with d hd`
 
-will turn it into two goals. The first is `0 + 0 = 0`, and
+will turn it into two goals. The first is `0 + 0 = 0`;
 the second has an assumption `hd : 0 + d = d` and goal
 `0 + succ d = succ d`.
--/
 
+Note that you must prove the first
+goal before being able to access the second one.
 "
 NewTactic induction
 
@@ -99,5 +94,5 @@ Conclusion
   is called `add_comm` and it is *true*, but unfortunately its proof *uses* both
   `add_zero` and `zero_add`!
 
-  Let's continue on our journey to `add_comm`.
+  Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`.
 "

Game/Levels/Addition/L02succ_add.lean

@@ -10,10 +10,10 @@ namespace MyNat
 Introduction
 "
 Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add a b`
-is the proof that `succ(a) + b = succ(a + b)` for `a` and `b` numbers.
+is the proof that `(succ a) + b = succ (a + b)` for `a` and `b` numbers.
 This result is what's standing in the way of `x + y = y + x`. Again
 we have the problem that we are adding `b` to things, so we need
-to split into the cases where `b = 0` and `b` is a successor.
+to use induction to split into the cases where `b = 0` and `b` is a successor.
 "
 
 LemmaDoc MyNat.succ_add as "succ_add" in "Add"
@@ -35,7 +35,9 @@ Statement succ_add (a b : ℕ) : succ a + b = succ (a + b)  := by
   · rw [add_zero]
     rw [add_zero]
     rfl
-  · rw [add_succ, add_succ, hd]
+  · 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."
+    rw [add_succ, add_succ, hd]
     rfl
 
 LemmaTab "Add"

Game/Levels/Addition/L05add_right_comm.lean

@@ -11,7 +11,7 @@ Introduction
 `add_comm b c` is a proof that `b + c = c + b`. But if your goal
 is `a + b + c = a + c + b` then `rw [add_comm b c]` will not
 work! Because the goal means `(a + b) + c = (a + c) + b` so there
-is no `b + c` term in the goal.
+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,

Game/Levels/Multiplication/L01mul_one.lean

@@ -12,7 +12,7 @@ Introduction
 
 See the new \"Mul\" tab in your lemmas, containing `mul_zero` and `mul_succ`.
 Right now these are the only facts we know about multiplication.
-Let's prove eight more.
+Let's prove nine more.
 
 Let's start with a warm-up: no induction needed for this one,
 because we know `1` is a successor.

Game/Levels/Multiplication/L02zero_mul.lean

@@ -8,11 +8,11 @@ namespace MyNat
 
 Introduction
 "
-We're going for `mul_comm x y : x * y = y * x`,
+Our first challenge is `mul_comm x y : x * y = y * x`,
 and we want to prove it by induction. The zero
 case will need `mul_zero` (which we have)
 and `zero_mul` (which we don't), so let's
-start there.
+start with this.
 "
 
 LemmaDoc MyNat.zero_mul as "zero_mul" in "Mul" "

Game/Levels/Multiplication/L03succ_mul.lean

@@ -9,15 +9,14 @@ namespace MyNat
 
 Introduction
 "
-We are on the journey to `mul_comm`, the proof that `a * b = b * a`.
-We'll get there in the next level. Until we're there, it is frustrating
-but true that we cannot assume commutativity. We have `mul_succ`
+Similarly 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 from addition world like
-
-* `add_right_comm a b c : a + b + c = a + c + b`
+The last level from addition world might help you in this level.
+If you can't remember what it is, you can go back to the
+home screen by clicking the house icon and then taking a look.
+You won't lose any progress.
 "
 
 LemmaDoc MyNat.succ_mul as "succ_mul" in "Mul" "
@@ -28,7 +27,7 @@ would be circular because the proof of `mul_comm` uses `mul_succ`.
 "
 
 /-- For all natural numbers $a$ and $b$, we have
-$\operatorname{succ}(a) \times b = a\times b + b$. -/
+$(\operatorname{succ}\ a) \times b = a\times b + b$. -/
 Statement succ_mul
     (a b : ℕ) : succ a * b = a * b + b := by
   induction b with d hd

Game/Levels/Multiplication/L04mul_comm.lean

@@ -9,9 +9,11 @@ namespace MyNat
 
 Introduction
 "
-When you've proved this theorem you will have \"spare\" proofs
+The first sub-boss of Multiplication World is `mul_comm x y : x * y = y * x`.
+
+When you've proved this theorem we will have \"spare\" proofs
 such as `zero_mul`, which is now easily deducible from `mul_zero`.
-But we keep hold of these theorems anyway, because often it's convenient
+But we'll keep hold of these proofs anyway, because it's convenient
 to have exactly the right tool for a job.
 "
 

Game/Levels/Multiplication/L05one_mul.lean

@@ -8,9 +8,12 @@ namespace MyNat
 
 Introduction
 "
-You can prove this one in at least three ways.
+You can prove $1\\times m=m$ in at least three ways.
 Either by induction, or by using `succ_mul`, or
 by using commutativity. Which do you think is quickest?
+
+You can even do `rw [one_mul]`, although this is a bug :-)
+**TODO** check this is happening on `main` and open an issue.
 "
 
 LemmaDoc MyNat.one_mul as "one_mul" in "Mul" "

Game/Levels/Multiplication/L06two_mul.lean

@@ -9,7 +9,7 @@ namespace MyNat
 Introduction
 "
 This level is more important than you think; it plays
-a key role in defeating a big boss.
+a useful role when battling a big boss later on.
 "
 
 LemmaDoc MyNat.two_mul as "two_mul" in "Mul" "

Game/Levels/Multiplication/L07mul_add.lean

@@ -28,7 +28,8 @@ $a(b + c) = ab + ac$. -/
 Statement mul_add
     (a b c : ℕ) : a * (b + c) = a * b + a * c := by
   Hint "You can do induction on any of the three variables. Some choices
-  are harder to push through than others."
+  are harder to push through than others. Can you do the inductive step in
+  5 rewrites only?"
   Hint (hidden := true) "Induction on `a` is the most troublesome, then `b`,
   and `c` is the easiest."
   induction c with d hd

Game/Levels/Multiplication/L08add_mul.lean

@@ -8,12 +8,8 @@ namespace MyNat
 
 Introduction
 "
-`add_mul` is just as fiddly to prove by induction; the proof using
-`add_comm` is easier.
-
-Don't forget that `add_comm` just changes the first `x + y` which it
-sees to `y + x`. If you want to be more targetted, `add_comm b c`
-only changes `b + c` to `c + b`.
+`add_mul` is just as fiddly to prove by induction; but there's a trick
+which avoids it. Can you spot it?
 "
 
 LemmaDoc MyNat.add_mul as "add_mul" in "Mul" "
@@ -24,16 +20,7 @@ In other words, for all natural numbers $a$, $b$ and $c$, we have
 $(a + b) \times c = ac + bc$. -/
 Statement add_mul
     (a b c : ℕ) : (a + b) * c = a * c + b * c := 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
+  rw [mul_comm, mul_add, mul_comm, mul_comm c]
+  rfl
 
 LemmaTab "Mul"

Game/Levels/Multiplication/L09mul_assoc.lean

@@ -9,7 +9,8 @@ namespace MyNat
 
 Introduction
 "
-We now have enough to prove that multiplication is associative.
+We now have enough to prove that multiplication is associative,
+the boss level of multiplication world. Good luck!
 "
 
 LemmaDoc MyNat.mul_assoc as "mul_assoc" in "Mul" "

Game/Levels/Tutorial/L03three_eq_sss0.lean

@@ -1,6 +1,6 @@
 import Game.Metadata
 import Game.MyNat.Definition
-import Game.MyNat.DecidableEq
+import Game.MyNat.TutorialLemmas
 
 World "Tutorial"
 Level 3

Game/MyNat/DecidableEq.lean

@@ -138,9 +138,3 @@ match a with
       match instDecidableEq p q with
       | isTrue h => isTrue <| by simp_all
       | isFalse h => isFalse <| by simp_all
-
-theorem one_eq_succ_zero : 1 = succ 0 := by decide
-theorem two_eq_succ_one : 2 = succ 1 := by decide
-theorem three_eq_succ_two : 3 = succ 2 := by decide
-theorem four_eq_succ_three : 4 = succ 3 := by decide
-theorem five_eq_succ_four : 5 = succ 4 := by decide

Game/MyNat/TutorialLemmas.lean

@@ -0,0 +1,13 @@
+import Game.MyNat.Addition
+/-
+This file adds proofs of results which were used in Tutorial World but
+which we can't import (because tutorial world imports multiplication
+in the first level, and we don't want to import this too early)
+-/
+
+namespace MyNat
+
+theorem one_eq_succ_zero : 1 = succ 0 := by rfl
+theorem two_eq_succ_one : 2 = succ 1 := by rfl
+theorem three_eq_succ_two : 3 = succ 2 := by rfl
+theorem four_eq_succ_three : 4 = succ 3 := by rfl