tinkering with comments and so on

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
 

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
 

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):

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!"

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.
 "

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

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

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."

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

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`.

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

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?"
 

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

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

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.$ -/

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
 

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,