fix typos that surfaced while creating German translation

Game/Levels/Addition/L02succ_add.lean

@@ -45,5 +45,5 @@ Statement succ_add (a b : ℕ) : succ a + b = succ (a + b)  := by
 TheoremTab "+"
 
 Conclusion "
-Well done! You now have enough tools to tackle the main boss of this level.
+Well done! You now have enough tools to tackle the main boss of this world.
 "

Game/Levels/AdvAddition/L03add_left_eq_self.lean

@@ -25,11 +25,11 @@ Statement add_left_eq_self (x y : ℕ) : x + y = y → x = 0 := by
 
 Conclusion "Did you use induction on `y`?
 Here's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.
-If you want to inspect it, you can go into editor mode by clicking `</>` in the top right
+If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right
 and then just cut and paste the proof and move your cursor around it
 to see the hypotheses and goal at any given point
 (although you'll lose your own proof this way). Click `>_` to get
-back to command line mode.
+back to \"Typewriter mode\".
 ```
 nth_rewrite 2 [← zero_add y]
 exact add_right_cancel x 0 y

Game/Levels/AdvMultiplication/L05le_mul_right.lean

@@ -20,7 +20,7 @@ Introduction
 "
 One day this game will have a Prime Number World, with a final boss
 of proving that $2$ is prime.
-To do this, we will have to rule out things like $2 = 37 × 42.$
+To do this, we will have to rule out things like $2 = 37 × 42$.
 We will do this by proving that any factor of $2$ is at most $2$,
 which we will do using this lemma. The proof I have in mind manipulates the hypothesis
 until it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and

Game/Levels/Implication/L05succ_inj2.lean

@@ -15,7 +15,7 @@ Introduction
   the goal until it becomes our hypothesis! In other words, we
   will \"argue backwards\". The `apply` tactic can do this too.
   Again I will walk you through this one (assuming you're in
-  command line mode).
+  \"Typewriter mode\").
 "
 
 /-- If $x+1=4$ then $x=3$. -/

Game/Levels/Multiplication/L08add_mul.lean

@@ -17,7 +17,7 @@ which avoids it. Can you spot it?
 -/
 TheoremDoc MyNat.add_mul as "add_mul" in "*"
 
-/-- Addition is distributive over multiplication.
+/-- Multiplication is distributive over addition.
 In other words, for all natural numbers $a$, $b$ and $c$, we have
 $(a + b) \times c = ac + bc$. -/
 Statement add_mul

Game/Levels/OldFunction/Level_3.lean

@@ -83,7 +83,7 @@ Conclusion
 "
 If you solved the level using `have`, then you might have observed
 that before the final step the context got quite messy by all the intermediate
-variables we introduced. You can click \"Toggle Editor\" and then move the cursor
+variables we introduced. You can switch to \"Editor mode\" and then move the cursor
 around to see the proof you created.
 
 The context was already bad enough to start with, and we added three more

Game/Levels/OldProposition/Level_8.lean

@@ -69,4 +69,4 @@ NewTactic «repeat»
 NewDefinition False Not
 
 Conclusion "If you used `rw [Not]` or `rw [Not] at h` anywhere, go through your proof in
-the \"Editor Mode\" and delete them all. Observe that your proof still works."
+the \"Editor mode\" and delete them all. Observe that your proof still works."