removing some TODOs

Game/Levels/Addition.lean

@@ -15,10 +15,8 @@ This will enable us to defeat the boss level of this world, namely `x + y = y +
 The tactics `rw`, `rfl` and `induction` are the only tactics you'll need to
 beat all the levels in Addition World, Multiplication World, and Power World.
 Power World contains the final boss of the game.
-"
 
--- **TODO** put this comment back when it becomes true
--- There are plenty more tactics in this game, but you'll only need to know them if you
--- want to explore the game further (for example if you decide to 100%
--- the game).
--- "
+There are plenty more tactics in this game, but you'll only need to know them if you
+want to explore the game further (for example if you decide to 100%
+the game).
+"

Game/Levels/Addition/L05add_right_comm.lean

@@ -39,14 +39,9 @@ LemmaTab "Add"
 
 Conclusion "
 You've now seen all the tactics you need to beat the final boss of the game.
-You can begin the journey towards this boss by entering Multiplication
-World.
-"
-
-/-
-Or you can go off the beaten track and learn some new tactics in Advanced
-Addition World (except that ). These tactics let you prove more facts about addition, such as
-how to deduce `a = b` from `x + a = x + b`.
--/
+You can begin the journey towards this boss by entering Multiplication World.
 
--- **TODO** choose a better example from advanced addition world once it's written
+Or you can go off the beaten track and learn some new tactics in Implication
+World. These tactics let you prove more facts about addition, such as
+how to deduce `a = 0` from `x + a = x`.
+"

Game/Levels/Tutorial/L02rw.lean

@@ -167,22 +167,3 @@ Statement
 Conclusion
 "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey.
 "
-/-
-
-**TODO** where to put this? Not this early.
-
-You can now press on by clicking \"Next\", but if you want to inspect the
-proof you just created, toggle \"Editor mode\" by clicking
-on the `</>` button in the top right. In editor mode,
-you can click or move your cursor around the proof to see the state of Lean's brain at any point.
-If you want to go back to the default (command line) mode with hints,
-click the button again (it now displays `>_`).
-
-In editor mode, note that each tactic is written on a new line and Lean is sensitive
-to indentation (i.e. there must be no spaces before any of the tactics).
-
-If you are just learning the game, I would recommend staying in command
-line mode in general, because you do not get hints during a level
-in editor mode, and hints are used to teach new tactics.
-"
--/

Game/Levels/Tutorial/L07add_succ.lean

@@ -18,8 +18,6 @@ NewLemma MyNat.add_succ
 LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add"
 "`succ_eq_add_one n` is the proof that `succ n = n + 1`."
 
-NewLemma MyNat.succ_eq_add_one
-
 Introduction
 "
 Every number in Lean is either 0 or a successor. We know how to add $0$,

Game/Levels/Tutorial/L08twoaddtwo.lean

@@ -48,13 +48,7 @@ Statement : (2 : ℕ) + 2 = 4 := by
 
 Conclusion
 "
-Below is an example proof showing off various techniques. You can copy
-and paste it directly into Lean if you switch into editor mode, and then
-you can inspect it by clicking around within the proof or moving your cursor
-down the lines.
-Click on `</>` and `>_` in the top right to switch between editor mode
-and command line mode. Switch back to command line mode
-when you've finished, if you prefer to see hints.
+Here is an example proof of 2+2=4 showing off various techniques.
 
 ```lean
 nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.
@@ -66,6 +60,14 @@ rw [← four_eq_succ_three]
 rfl
 ```
 
+Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking
+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
+move back into command line mode.
+
 You have finished tutorial world! Now let's move onto Addition World,
 and learn the `induction` tactic.
 "