diff --git a/Game/Levels/AdvMultiplication.lean b/Game/Levels/AdvMultiplication.lean
index b75e941..51adda5 100644
--- a/Game/Levels/AdvMultiplication.lean
+++ b/Game/Levels/AdvMultiplication.lean
@@ -1,5 +1,8 @@
 import Game.Levels.AdvMultiplication.L01mul_le_mul_right
-
+import Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+import Game.Levels.AdvMultiplication.L03one_le_of_zero_ne
+import Game.Levels.AdvMultiplication.L04le_mul_right
+import Game.Levels.AdvMultiplication.L05le_one
 World "AdvMultiplication"
 Title "Advanced Multiplication World"
 
diff --git a/Game/Levels/AdvMultiplication/L02mul_left_ne_zero.lean b/Game/Levels/AdvMultiplication/L02mul_left_ne_zero.lean
new file mode 100644
index 0000000..370f8dc
--- /dev/null
+++ b/Game/Levels/AdvMultiplication/L02mul_left_ne_zero.lean
@@ -0,0 +1,28 @@
+import Game.Levels.AdvMultiplication.L01mul_le_mul_right
+
+World "AdvMultiplication"
+Level 2
+Title "mul_left_ne_zero"
+
+LemmaTab "*"
+
+namespace MyNat
+
+LemmaDoc MyNat.mul_left_ne_zero as "mul_left_ne_zero" in "*" "
+`mul_left_ne_zero a b` is a proof that `a * b ≠ 0 → b ≠ 0`.
+"
+
+Introduction
+"If you have completed Algorithm World then you can use the `contrapose!` tactic
+here. If not then I'll talk you through a manual approach."
+
+Statement mul_left_ne_zero (a b : ℕ) (h : a * b ≠ 0) : b ≠ 0 := by
+  Hint "We want to reduce this to a hypothesis `b = 0` and a goal `a * b = 0`,
+  which is logically equivalent but much easier to prove. Remember that `X ≠ 0`
+  is notation for `X = 0 → False`. Click on `Show more help!` if you need hints."
+  Hint (hidden := true) "Start with `intro hb`."
+  intro hb
+  Hint (hidden := true) "Now `apply h` and you can probably take it from here."
+  apply h
+  rw [hb, mul_zero]
+  rfl
diff --git a/Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean b/Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean
new file mode 100644
index 0000000..1653b26
--- /dev/null
+++ b/Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean
@@ -0,0 +1,30 @@
+import Game.Levels.AdvMultiplication.L02mul_left_ne_zero
+
+World "AdvMultiplication"
+Level 3
+Title "one_le_of_zero_ne"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.one_le_of_zero_ne as "one_le_of_zero_ne" in "≤" "
+`one_le_of_zero_ne a` is a proof that `a ≠ 0 → 1 ≤ a`.
+"
+
+Introduction
+"We need to understand how to use a hypothesis like `a ≠ 0`.
+Here is a useful lemma. I talk through how to get started in the hidden hints.
+Access them by clicking on \"Show more help!\"
+"
+
+Statement one_le_of_zero_ne (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by
+  Hint (hidden := true) "Start with `cases a with n` to do a case split on `a = 0` and `a = succ n`."
+  cases a with n
+  · Hint (hidden := true) "You have a false hypothesis so you can just solve this with the logic
+  tactic `tauto`."
+    tauto
+  · use n
+    rw [succ_eq_add_one]
+    rw [add_comm]
+    rfl
diff --git a/Game/Levels/AdvMultiplication/L04le_mul_right.lean b/Game/Levels/AdvMultiplication/L04le_mul_right.lean
new file mode 100644
index 0000000..6a693e0
--- /dev/null
+++ b/Game/Levels/AdvMultiplication/L04le_mul_right.lean
@@ -0,0 +1,42 @@
+import Game.Levels.AdvMultiplication.L03one_le_of_zero_ne
+
+World "AdvMultiplication"
+Level 4
+Title "le_mul_right"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_mul_right as "le_mul_right" in "≤" "
+`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.
+
+It's one way of saying that a divisor of a positive number
+has to be at most that number.
+"
+
+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 \neq 323846224*3453453459182.$
+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 uses
+everything which we've proved in this world so far.
+"
+
+Statement le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by
+  apply mul_left_ne_zero at h
+  apply one_le_of_zero_ne at h
+  apply mul_le_mul_right 1 b a at h
+  rw [one_mul, mul_comm] at h
+  exact h
+
+Conclusion "Here's what I was thinking of:
+```
+apply mul_left_ne_zero at h
+apply one_le_of_zero_ne at h
+apply mul_le_mul_right 1 b a at h
+rw [one_mul, mul_comm] at h
+exact h
+```
+"
diff --git a/Game/Levels/AdvMultiplication/L05le_one.lean b/Game/Levels/AdvMultiplication/L05le_one.lean
new file mode 100644
index 0000000..7598462
--- /dev/null
+++ b/Game/Levels/AdvMultiplication/L05le_one.lean
@@ -0,0 +1,40 @@
+import Game.Levels.AdvMultiplication.L04le_mul_right
+
+World "AdvMultiplication"
+Level 5
+Title "le_one"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_one as "le_one" in "≤" "
+`le_one a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.
+
+It's one way of saying that a divisor of a positive number
+has to be at most that number.
+"
+
+Introduction
+"We could have proved this result in ≤ World. I leave some hidden hints.
+"
+
+Statement le_one (a : ℕ) (ha : a ≤ 1) : a = 0 ∨ a = 1 := by
+  Hint (hidden := true) "Start with `cases a with b` to break into `a = 0` and `a = succ b` cases."
+  cases a with b
+  · left
+    rfl
+  · Hint (hidden := true) "Now `cases b with c`."
+    cases b with c
+    · right
+      rw [one_eq_succ_zero]
+      rfl
+    · Hint (hidden := true) "Now `cases ha with x hx` and work on `hx` until it's `False`.
+      Then use a logic tactic to finish."
+      cases ha with x hx
+      rw [succ_add, succ_add] at hx
+      rw [one_eq_succ_zero] at hx
+      apply succ_inj at hx
+      apply zero_ne_succ at hx
+      Hint (hidden := true) "Now finish with `tauto`."
+      tauto
diff --git a/Game/Levels/AdvMultiplication/all_levels.lean b/Game/Levels/AdvMultiplication/all_levels.lean
index 5083c20..c054cc7 100644
--- a/Game/Levels/AdvMultiplication/all_levels.lean
+++ b/Game/Levels/AdvMultiplication/all_levels.lean
@@ -1,5 +1,4 @@
-import Game.Levels.AdvMultiplication.L01mul_le_mul_right
-
+import Game.Levels.AdvMultiplication.L05le_one
 namespace MyNat
 
 -- -- good level 1; used in the important `le_mul_right`
@@ -9,49 +8,39 @@ namespace MyNat
 --   rw [hd, add_mul]
 --   rfl
 
--- used in `le_mul_right`
-lemma mul_left_ne_zero (a b : ℕ) (h : a * b ≠ 0) : b ≠ 0 := by
-  apply mt _ h
-  have h1 : b = 0 → a * b = 0
-  · intro h2
-    rw [h2, mul_zero]
-    rfl
-  tauto
-
--- used in `le_mul_right`
-lemma one_le_of_zero_ne (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by
-  cases a with n
-  · tauto
-  · use n
-    rw [succ_eq_add_one]
-    rw [add_comm]
-    rfl
+-- -- used in `le_mul_right`
+-- lemma mul_left_ne_zero (a b : ℕ) (h : a * b ≠ 0) : b ≠ 0 := by
+--   contrapose! h
+--   have h1 : b = 0 → a * b = 0
+--   · intro h2
+--     rw [h2, mul_zero]
+--     rfl
+--   tauto
 
--- `le_mul_right` is used in `if a ∣ x and x ≠ 0 then a ≤ x`, a key fact
--- for proving 2 is prime! It's also used in cd=1=>c=1, which Archie needs.
-lemma le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by
-  apply mul_left_ne_zero at h
-  apply one_le_of_zero_ne at h
-  apply mul_le_mul_right 1 b a at h
-  rw [one_mul, mul_comm] at h
-  exact h
+-- -- `le_mul_right` is used in `if a ∣ x and x ≠ 0 then a ≤ x`, a key fact
+-- -- for proving 2 is prime! It's also used in cd=1=>c=1, which Archie needs.
+-- lemma le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by
+--   apply mul_left_ne_zero at h
+--   apply one_le_of_zero_ne at h
+--   apply mul_le_mul_right 1 b a at h
+--   rw [one_mul, mul_comm] at h
+--   exact h
 
--- needed, with le_mul_right, to prove cd=1=>c=1
-
-lemma le_one (a : ℕ) (ha : a ≤ 1) : a = 0 ∨ a = 1 := by
-  cases a with b
-  · left
-    rfl
-  · cases b with c
-    · right
-      rw [one_eq_succ_zero]
-      rfl
-    · cases ha with x hx
-      rw [succ_add, succ_add] at hx
-      rw [one_eq_succ_zero] at hx
-      apply succ_inj at hx
-      apply zero_ne_succ at hx
-      tauto
+-- -- needed, with le_mul_right, to prove cd=1=>c=1
+-- lemma le_one (a : ℕ) (ha : a ≤ 1) : a = 0 ∨ a = 1 := by
+--   cases a with b
+--   · left
+--     rfl
+--   · cases b with c
+--     · right
+--       rw [one_eq_succ_zero]
+--       rfl
+--     · cases ha with x hx
+--       rw [succ_add, succ_add] at hx
+--       rw [one_eq_succ_zero] at hx
+--       apply succ_inj at hx
+--       apply zero_ne_succ at hx
+--       tauto
 
 -- Archie needs this
 lemma mul_right_eq_one (c d : ℕ) (h : c * d = 1) : c = 1 := by
@@ -73,7 +62,7 @@ lemma eq_succ_of_ne_zero (a : ℕ) (ha : a ≠ 0) : ∃ n, a = succ n := by
   cases a with d
   tauto
   use d
-  -- WTF????? **TODO** `use` shouldn't try `rfl`
+  rfl
 
 -- used in `mul_eq_zero`, which is used in `mul_left_cancel`
 lemma mul_ne_zero (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by