some fixes

Game/Levels/Addition/L01two_add_one.lean

@@ -7,18 +7,6 @@ Title "Two add one is three."
 
 namespace MyNat
 
-LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "numerals" "`two_eq_succ_one is a proof of `2 = succ 1`."
-NewLemma MyNat.two_eq_succ_one
-
-LemmaDoc MyNat.three_eq_succ_two as "three_eq_succ_two" in "numerals" "`three_eq_succ_two is a proof of `3 = succ 2`."
-NewLemma MyNat.three_eq_succ_two
-
-LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals" "`four_eq_succ_three is a proof of `4 = succ 3`."
-NewLemma MyNat.four_eq_succ_three
-
-LemmaDoc MyNat.five_eq_succ_four as "five_eq_succ_four" in "numerals" "`five_eq_succ_four is a proof of `5 = succ 4`."
-NewLemma MyNat.five_eq_succ_four
-
 Introduction
 "
 Remember Peano's axioms:
@@ -49,9 +37,21 @@ Statement : (2 : ℕ) + 1 = 3 := by
   rw [three_eq_succ_two]
   rfl
 
+LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "numerals"
+"`two_eq_succ_one is a proof of `2 = succ 1`."
+
+LemmaDoc MyNat.three_eq_succ_two as "three_eq_succ_two" in "numerals"
+"`three_eq_succ_two is a proof of `3 = succ 2`."
+
+LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals"
+"`four_eq_succ_three is a proof of `4 = succ 3`."
+
+LemmaDoc MyNat.five_eq_succ_four as "five_eq_succ_four" in "numerals"
+"`five_eq_succ_four is a proof of `5 = succ 4`."
+
 NewLemma MyNat.two_eq_succ_one MyNat.three_eq_succ_two
   MyNat.four_eq_succ_three MyNat.five_eq_succ_four
-LemmaTab "Add"
+LemmaTab "numerals"
 
 Conclusion
 "

Game/Levels/Addition/L08add_assoc.lean

@@ -47,7 +47,6 @@ Statement add_assoc (a b c : ℕ) : (a + b) + c = a + (b + c) := by
 -- Adding this instance to make `ac_rfl` work.
 instance : Lean.IsAssociative (α := ℕ) (·+·) := ⟨add_assoc⟩
 
-NewLemma MyNat.add_assoc
 LemmaTab "Add"
 
 Conclusion

Game/Levels/Addition/L10annoying.lean

@@ -27,7 +27,7 @@ Statement (a b c d : ℕ) : a + d + (b + c) = a + b + c + d := by
   Hint "Now use targetted `rw [add_comm x y]` and `rw [add_left_comm x y]` to
   switch consecutive variables `x` and `y` on the left hand side until everything
   is in the right order. The point is that `add_comm` switches the last two,
-  and `add_left-comm` can be used to switch any oher pair of consecutive
+  and `add_left_comm` can be used to switch any oher pair of consecutive
   variables."
   Hint (hidden := true) "Start with `add_left_comm d b`, which will switch
   `d` and `b` on the left hand side."

Game/Levels/Tutorial/L05add_zero.lean

@@ -24,22 +24,7 @@ to do a lot of work for us."
 
 namespace MyNat
 
-TacticDoc simp "The simplifier. `rw` on steroids.
-
-A bunch of lemmas like `add_zero : ∀ a, a + 0 = a`
-are tagged with the `@[simp]` tag. If the `simp` tactic
-is run by the user, the simplifier will try and rewrite
-as many of the lemmas tagged `@[simp]` as it can.
-
-`simp` is a *finishing tactic*. After you run `simp`,
-the goal should be closed. If it is not, it is best
-practice to write `simp?` instead and then replace the
-output with the appropriate `simp only` call. Inappropriate
-use of `simp` can make for very slow code.
-"
-NewTactic simp -- TODO: Do we want it to be unlocked here?
-
-/-- $(a+(0+0)+(0+0+0)=a.$ -/
+/-- $a+(0+0)+(0+0+0)=a.$ -/
 Statement (a : ℕ)  : (a + (0 + 0)) + (0 + 0 + 0) = a := by
   Hint "I will walk you through this level so I can show you some
   techniques which will speed up your proving.
@@ -98,6 +83,7 @@ All you need to know is that `add_zero` and `zero_add` are both theorems."
 NewLemma MyNat.add_zero
 NewTactic simp «repeat» -- TODO: Do we want it to be unlocked here?
 NewDefinition Add
+LemmaTab "Add"
 
 Conclusion
 "

Game/Levels/Tutorial/L06add_succ.lean

@@ -19,11 +19,6 @@ your way to a proof of this.
 "
 namespace MyNat
 
-LemmaDoc MyNat.add_succ as "add_succ" in "Add"
-"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
-
-NewLemma MyNat.add_succ
-
 /-- For all natural numbers $a$, we have $a + \operatorname{succ}(0) = \operatorname{succ}(a)$. -/
 Statement : a + succ 0 = succ a := by
   Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
@@ -39,6 +34,13 @@ Statement : a + succ 0 = succ a := by
   Hint (hidden := true) "Finally both sides are identical."
   rfl
 
+
+LemmaDoc MyNat.add_succ as "add_succ" in "Add"
+"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
+
+NewLemma MyNat.add_succ
+LemmaTab "Add"
+
 Conclusion
 "
 You have finished tutorial world! If you're happy, let's move onto Addition World,