algorithm world now hopefully finished

Game/Levels/Algorithm/L05pred.lean

@@ -24,8 +24,9 @@ pred 0 := 37
 pred (succ n) := n
 ```
 
-We cannot subtract one from 0, so we just return a junk value. A new lemma `pred_succ`
-says that `pred (succ n) = n`. Let's use it to prove `succ_inj`, the theorem which
+We cannot subtract one from 0, so we just return a junk value. As well as this
+definition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.
+Let's use this lemma to prove `succ_inj`, the theorem which
 Peano assumed as an axiom and which we have already used extensively without justification.
 "
 
@@ -45,5 +46,7 @@ Statement (a b : ℕ) (h : succ a = succ b) : a = b := by
   rfl
 
 Conclusion
-"Let's now prove Peano's other axiom, that successors can't be $0$.
+"
+Nice! You've proved `succ_inj`!
+Let's now prove Peano's other axiom, that successors can't be $0$.
 "

Game/Levels/Algorithm/L06is_zero.lean

@@ -10,17 +10,17 @@ namespace MyNat
 
 Introduction
 "
-We now define a function `is_zero` thus:
+We define a function `is_zero` thus:
 
 ```
 is_zero 0 := True
 is_zero (succ n) := False
 ```
 
-We also need two lemmas, `is_zero_zero` and `is_zero_succ`, saying that `is_zero 0 = True`
-and `is_zero (succ n) = False`. Let's use this function to prove `succ_ne_zero`, Peano's
-Last Axiom. We have been using `zero_ne_succ` before, but it's handy to have
-this opposite version too.
+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.
 
 If you can turn your goal into `True`, then the `tauto` tactic will solve it.
 "
@@ -44,7 +44,8 @@ NewLemma MyNat.is_zero_zero MyNat.is_zero_succ
 
 /-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/
 Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
-  Hint "Start with `intro h`."
+  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]`."

Game/Levels/Algorithm/L07succ_ne_succ.lean

@@ -70,8 +70,9 @@ LemmaDoc MyNat.succ_ne_succ as "succ_ne_succ" in "Peano" "
 
 /-- If $a \neq b$ then $\operatorname{succ}(a) \neq\operatorname{succ}(b)$. -/
 Statement succ_ne_succ (m n : ℕ) (h : m ≠ n) : succ m ≠ succ n := by
-  Hint "Start by adding `succ a = succ b → a = b` to our list of hypotheses,
-  with `have h2 := succ_inj m n`."
+  Hint "Start by adding `succ m = succ n → m = n` to our list of hypotheses,
+  with `have h2 := succ_inj m n`. Read about the `have` tactic in the
+  documentation on the top right."
   have := succ_inj m n
   Hint "Now the goal can be solved by pure logic, so use a logic tactic."
   Hint (hidden := true) "Use `tauto`."

Game/Levels/Algorithm/L08decide.lean

@@ -18,7 +18,7 @@ can run to solve it.
 ## Example
 
 A term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals
-are equal or difference. Hence, once this term is made and made into an `instance`,
+are equal or different. Hence, once this term is made and made into an `instance`,
 the `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.
 "
 
@@ -58,3 +58,6 @@ between two naturals. Run it with the `decide` tactic.
 /-- $20+20=40$. -/
 Statement : (20 : ℕ) + 20 = 40 := by
   decide
+
+Conclusion "You can read more about the `decide` tactic by clicking
+on it in the top right."