hopefully finished advanced multiplication world!

Game/Levels/AdvMultiplication.lean

@@ -1,9 +1,13 @@
 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
+import Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+import Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
+import Game.Levels.AdvMultiplication.L05le_mul_right
 import Game.Levels.AdvMultiplication.L06mul_right_eq_one
+import Game.Levels.AdvMultiplication.L07mul_ne_zero
+import Game.Levels.AdvMultiplication.L08mul_eq_zero
+import Game.Levels.AdvMultiplication.L09mul_left_cancel
+import Game.Levels.AdvMultiplication.L10mul_right_eq_self
 
 World "AdvMultiplication"
 Title "Advanced Multiplication World"

Game/Levels/AdvMultiplication/L05le_mul_right.lean

@@ -1,4 +1,4 @@
-import Game.Levels.AdvMultiplication.L04one_le_of_zero_ne
+import Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
 
 World "AdvMultiplication"
 Level 5

Game/Levels/AdvMultiplication/L07mul_ne_zero.lean

@@ -0,0 +1,31 @@
+import Game.Levels.AdvMultiplication.L06mul_right_eq_one
+
+World "AdvMultiplication"
+Level 7
+Title "mul_ne_zero"
+
+LemmaTab "*"
+
+namespace MyNat
+
+LemmaDoc MyNat.mul_ne_zero as "mul_ne_zero" in "*" "
+`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`.
+"
+
+Introduction
+"
+This level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy
+is to write both `a` and `b` as `succ` of something, deduce that `a * b` is
+also `succ` of something, and then `apply zero_ne_succ`.
+"
+
+Statement mul_ne_zero (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by
+  Hint (hidden := true) "Start with `apply eq_succ_of_ne_zero at ha` and `... at hb`"
+  apply eq_succ_of_ne_zero at ha
+  apply eq_succ_of_ne_zero at hb
+  cases ha with c hc
+  cases hb with d hd
+  rw [hc, hd]
+  rw [mul_succ, add_succ]
+  symm
+  apply zero_ne_succ

Game/Levels/AdvMultiplication/L08mul_eq_zero.lean

@@ -0,0 +1,26 @@
+import Game.Levels.AdvMultiplication.L07mul_ne_zero
+
+World "AdvMultiplication"
+Level 8
+Title "mul_eq_zero"
+
+LemmaTab "*"
+
+namespace MyNat
+
+LemmaDoc MyNat.mul_eq_zero as "mul_eq_zero" in "*" "
+`mul_eq_zero a b` is a proof that if `a * b = 0` then `a = 0` or `b = 0`.
+"
+
+Introduction
+"
+This level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is
+logically equivalent to the last level, so there is a very short proof.
+"
+
+Statement mul_eq_zero (a b : ℕ) (h : a * b = 0) : a = 0 ∨ b = 0 := by
+  Hint (hidden := true) "Start with `have h2 := mul_ne_zero a b`."
+  have h2 := mul_ne_zero a b
+  Hint (hidden := true) "Now the goal can be deduced from `h2` by pure logic, so use the `tauto`
+  tactic."
+  tauto

Game/Levels/AdvMultiplication/L09mul_left_cancel.lean

@@ -0,0 +1,54 @@
+import Game.Levels.AdvMultiplication.L08mul_eq_zero
+
+World "AdvMultiplication"
+Level 9
+Title "mul_left_cancel"
+
+LemmaTab "*"
+
+namespace MyNat
+
+LemmaDoc MyNat.mul_left_cancel as "mul_left_cancel" in "*" "
+`mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`.
+"
+
+Introduction
+"
+In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for
+several reasons. One of these is that
+we need to introduce a new idea: we will need to understand the concept of
+mathematical induction a little better.
+
+Starting with `induction b with d hd` is too naive, because in the inductive step
+the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,
+hence the induction hypothesis does not apply!
+
+Assume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is
+\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,
+because we now have the flexibility to change `c`.\"
+"
+
+Statement mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = c := by
+  Hint "The way to start this proof is `induction b with d hd generalizing c`."
+  induction b with d hd generalizing c
+  · Hint (hidden := true) "Use `mul_eq_zero` and remember that `tauto` will solve a goal
+  if there are hypotheses `a = 0` and `a ≠ 0`."
+    rw [mul_zero] at h
+    symm at h
+    apply mul_eq_zero at h
+    cases h with h1 h2
+    · tauto
+    · rw [h2]
+      rfl
+  · Hint "The inductive hypothesis `hd` is \"For all natural numbers `c`, a * d = a * c → d = c`\".
+    You can `apply` it `at` any hypothesis of the form `a * d = a * ?`. "
+    Hint (hidden := true) "Split into cases `c = 0` and `c = succ e` with `cases c with e`."
+    cases c with e
+    · rw [mul_succ, mul_zero] at h
+      apply add_left_eq_zero at h
+      tauto
+    · rw [mul_succ, mul_succ] at h
+      apply add_right_cancel at h
+      apply hd at h
+      rw [h]
+      rfl

Game/Levels/AdvMultiplication/L10mul_right_eq_self.lean

@@ -0,0 +1,35 @@
+import Game.Levels.AdvMultiplication.L09mul_left_cancel
+
+World "AdvMultiplication"
+Level 10
+Title "mul_right_eq_self"
+
+LemmaTab "*"
+
+namespace MyNat
+
+LemmaDoc MyNat.mul_right_eq_self as "mul_right_eq_self" in "*" "
+`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`.
+"
+
+Introduction
+"The lemma proved in the final level of this world will be helpful
+in Divisibility World.
+"
+
+Statement mul_right_eq_self (a b : ℕ) (ha : a ≠ 0) (h : a * b = a) : b = 1 := by
+  Hint (hidden := true) "Reduce to the previous lemma with `nth_rewrite 2 [← mul_one a] at h`"
+  nth_rewrite 2 [← mul_one a] at h
+  Hint (hidden := true) "You can now `apply mul_left_cancel at h`"
+  exact mul_left_cancel a b 1 ha h
+
+Conclusion "
+A two-line proof is
+
+```
+nth_rewrite 2 [← mul_one a] at h
+exact mul_left_cancel a b 1 ha h
+```
+
+We now have all the tools necessary to set up the basic theory of divisibility of naturals.
+"

Game/Levels/AdvMultiplication/all_levels.lean

@@ -58,12 +58,12 @@ namespace MyNat
 --     tauto
 --   exact h1
 
--- used in `mul_ne_zero`, which is used in `mul_eq_zero`, which is used in `mul_left_cancel`
-lemma eq_succ_of_ne_zero (a : ℕ) (ha : a ≠ 0) : ∃ n, a = succ n := by
-  cases a with d
-  tauto
-  use d
-  rfl
+-- -- used in `mul_ne_zero`, which is used in `mul_eq_zero`, which is used in `mul_left_cancel`
+-- lemma eq_succ_of_ne_zero (a : ℕ) (ha : a ≠ 0) : ∃ n, a = succ n := by
+--   cases a with d
+--   tauto
+--   use d
+--   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
@@ -94,7 +94,7 @@ lemma mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = c :
       rfl
   · cases c with c
     · rw [mul_succ, mul_zero] at h
-      apply eq_zero_of_add_left_eq_zero at h
+      apply add_left_eq_zero at h
       tauto
     · rw [mul_succ, mul_succ] at h
       apply add_right_cancel at h