Advanced multiplication minor reorganisation

Game/Levels/AdvMultiplication/L04one_le_of_zero_ne.lean

@@ -0,0 +1,26 @@
+import Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
+
+World "AdvMultiplication"
+Level 4
+Title "one_le_of_ne_zero"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.one_le_of_ne_zero as "one_le_of_ne_zero" in "≤" "
+`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`.
+"
+
+Introduction
+"The previous lemma can be used to prove this one.
+"
+
+Statement one_le_of_ne_zero (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by
+  Hint (hidden := true) "Use the previous lemma with `apply eq_succ_of_ne_zero at ha`."
+  apply eq_succ_of_ne_zero at ha
+  Hint (hidden := true) "Now take apart the existence statement with `cases ha with n hn`."
+  cases ha with n hn
+  use n
+  rw [hn, succ_eq_add_one, add_comm]
+  rfl

Game/Levels/AdvMultiplication/L04le_mul_right.lean → Game/Levels/AdvMultiplication/L05le_mul_right.lean

@@ -1,7 +1,7 @@
-import Game.Levels.AdvMultiplication.L03one_le_of_zero_ne
+import Game.Levels.AdvMultiplication.L04one_le_of_zero_ne
 
 World "AdvMultiplication"
-Level 4
+Level 5
 Title "le_mul_right"
 
 LemmaTab "≤"
@@ -18,23 +18,23 @@ 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.$
+To do this, we will have to rule out things like $2 ≠ 323846224 \times 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.
+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.
 "
 
 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 one_le_of_ne_zero 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 one_le_of_ne_zero at h
 apply mul_le_mul_right 1 b a at h
 rw [one_mul, mul_comm] at h
 exact h

Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean

@@ -1,4 +1,4 @@
-import Game.Levels.AdvMultiplication.L05le_one
+import Game.Levels.AdvMultiplication.L05le_mul_right
 
 World "AdvMultiplication"
 Level 6
@@ -53,8 +53,11 @@ LemmaDoc MyNat.mul_right_eq_one as "mul_right_eq_one" in "*" "
 
 Introduction
 "
-This is the multiplicative analogue of Advanced Addition World's `x + y = 0 → x = 0`.
-We'll prove it using a new tactic called `have`.
+This level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition
+World's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the
+lemma `le_one` from `≤` world.
+
+We'll prove it using a new and very useful tactic called `have`.
 "
 
 Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by
@@ -63,9 +66,8 @@ Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by
   prove it, and then you'll have a new hypothesis which you can apply
   `le_mul_right` to."
   have hx : x * y ≠ 0
-  rw [h, one_eq_succ_zero]
-  symm
-  apply zero_ne_succ
+  rw [h]
+  exact one_ne_zero
   Hint (hidden := true) "Now you can `apply le_mul_right at hx`."
   apply le_mul_right at hx
   Hint (hidden := true) "Now `rw [h] at hx` so you can `apply le_one at hx`."
@@ -75,6 +77,6 @@ Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by
   cases separately."
   cases hx with h0 h1
   · rw [h0, zero_mul] at h
-    apply zero_ne_succ at h
+    Hint (hidden := true) "`tauto` is good enough to solve this goal."
     tauto
-  exact h1
+  · exact h1