diff --git a/Game/Levels/Addition/L02succ_add.lean b/Game/Levels/Addition/L02succ_add.lean
index 8a519651..84e28667 100644
--- a/Game/Levels/Addition/L02succ_add.lean
+++ b/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.
 "
diff --git a/Game/Levels/AdvAddition/L03add_left_eq_self.lean b/Game/Levels/AdvAddition/L03add_left_eq_self.lean
index bf0f877d..c0ec1a2c 100644
--- a/Game/Levels/AdvAddition/L03add_left_eq_self.lean
+++ b/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
diff --git a/Game/Levels/AdvMultiplication/L05le_mul_right.lean b/Game/Levels/AdvMultiplication/L05le_mul_right.lean
index 334cc671..d733a370 100644
--- a/Game/Levels/AdvMultiplication/L05le_mul_right.lean
+++ b/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
diff --git a/Game/Levels/Implication/L05succ_inj2.lean b/Game/Levels/Implication/L05succ_inj2.lean
index 9cd9b9e7..92cd7c7b 100644
--- a/Game/Levels/Implication/L05succ_inj2.lean
+++ b/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$. -/
diff --git a/Game/Levels/Multiplication/L08add_mul.lean b/Game/Levels/Multiplication/L08add_mul.lean
index eaba5192..207f5cae 100644
--- a/Game/Levels/Multiplication/L08add_mul.lean
+++ b/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
diff --git a/Game/Levels/OldFunction/Level_3.lean b/Game/Levels/OldFunction/Level_3.lean
index 6618d1d8..cfe4f2c5 100644
--- a/Game/Levels/OldFunction/Level_3.lean
+++ b/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
diff --git a/Game/Levels/OldProposition/Level_8.lean b/Game/Levels/OldProposition/Level_8.lean
index 292bd816..c38953ca 100644
--- a/Game/Levels/OldProposition/Level_8.lean
+++ b/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."