diff --git a/Game/Levels/AdvMultiplication/L03eq_succ_of_ne_zero.lean b/Game/Levels/AdvMultiplication/L03eq_succ_of_ne_zero.lean
index 4328783..7854468 100644
--- a/Game/Levels/AdvMultiplication/L03eq_succ_of_ne_zero.lean
+++ b/Game/Levels/AdvMultiplication/L03eq_succ_of_ne_zero.lean
@@ -50,7 +50,7 @@ TheoremDoc MyNat.eq_succ_of_ne_zero as "eq_succ_of_ne_zero" in "≤"
 Introduction
 "Multiplication usually makes a number bigger, but multiplication by zero can make
 it smaller. Thus many lemmas about inequalities and multiplication need the
-hypothesis `a ≠ 0`. Here is a key lemma enables us to use this hypothesis.
+hypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.
 To help us with the proof, we can use the `tauto` tactic. Click on the tactic's name
 on the right to see what it does.
 "
diff --git a/Game/Levels/AdvMultiplication/L05le_mul_right.lean b/Game/Levels/AdvMultiplication/L05le_mul_right.lean
index 8540e23..d22d88b 100644
--- a/Game/Levels/AdvMultiplication/L05le_mul_right.lean
+++ b/Game/Levels/AdvMultiplication/L05le_mul_right.lean
@@ -19,7 +19,7 @@ TheoremDoc MyNat.le_mul_right as "le_mul_right" in "≤"
 Introduction
 "
 In Prime Number World we will be 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 pretty much everything which we've proved in this world so far.
diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
index 6f39832..207788c 100644
--- a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
+++ b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
@@ -38,7 +38,7 @@ to the context, because you just supplied the proof of it (`succ_inj a b`).
 ## Example
 
 If you have a proof to hand, then you don't even need to state what you
-are proving. example
+are proving. For example
 
 `have h2 := succ_inj a b`