nng levels

server/nng/NNG.lean

@@ -3,13 +3,13 @@ import GameServer.Commands
 import NNG.Levels.Tutorial
 import NNG.Levels.Addition
 import NNG.Levels.Multiplication
-import NNG.Levels.Power
+-- import NNG.Levels.Power
 import NNG.Levels.Function
 import NNG.Levels.Proposition
 import NNG.Levels.AdvProposition
 import NNG.Levels.AdvAddition
 import NNG.Levels.AdvMultiplication
-import NNG.Levels.Inequality
+-- import NNG.Levels.Inequality
 
 Game "NNG"
 Title "Natural Number Game"
@@ -57,8 +57,8 @@ If you delete it, your progress will be lost!
 "
 
 Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition
-Path AdvAddition → AdvMultiplication → Inequality
+Path AdvAddition → AdvMultiplication -- → Inequality
 Path Addition → Multiplication → AdvMultiplication
-Path Multiplication → Power
+-- Path Multiplication → Power
 
 MakeGame

server/nng/NNG/Levels/AdvAddition/Level_1.lean

@@ -1,24 +1,42 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 1
-Title ""
+Title "`succ_inj`. A function."
 
 open MyNat
 
 Introduction
 "
-
+Peano's original collection of axioms for the natural numbers contained two further
+assumptions, which have not yet been mentioned in the game:
+
+```
+succ_inj {a b : mynat} :
+  succ(a) = succ(b) → a = b
+
+zero_ne_succ (a : mynat) :
+  zero ≠ succ(a)
+ ```
+
+The reason they have not been used yet is that they are both implications,
+that is,
+of the form $P\\implies Q$. This is clear for `succ_inj a b`, which
+says that for all $a$ and $b$ we have $succ(a)=succ(b)\\implies a=b$.
+For `zero_ne_succ` the trick is that $X\ne Y$ is *defined to mean*
+$X = Y\\implies{\\tt false}$. If you have played through Proposition world,
+you now have the required Lean skills (i.e., you know the required
+tactics) to work with these implications.
+Let's finally learn how to use `succ_inj`. You should know a couple
+of ways to prove the below -- one directly using an `exact`,
+and one which uses an `apply` first. But either way you'll need to use `succ_inj`.
 "
 
-theorem MyNat.succ_inj {a b : ℕ} : succ a = succ b → a = b := by simp only [succ.injEq, imp_self]
-
-theorem MyNat.zero_ne_succ (a : ℕ) : zero ≠ succ a := by simp only [ne_eq, not_false_iff]
-
 Statement -- MyNat.succ_inj'
-""
+"For all naturals $a$ and $b$, if we assume $succ(a)=succ(b)$, then we can
+deduce $a=b$."
     {a b : ℕ} (hs : succ a = succ b) :  a = b := by
     exact succ_inj hs
 
@@ -26,5 +44,11 @@ NewLemma MyNat.succ_inj MyNat.zero_ne_succ
 
 Conclusion
 "
+## Important thing.
 
+You can rewrite proofs of *equalities*. If `h : A = B` then `rw h` changes `A`s to `B`s.
+But you *cannot rewrite proofs of implications*. `rw succ_inj` will *never work*
+because `succ_inj` isn't of the form $A = B$, it's of the form $A\\implies B$. This is one
+of the most common mistakes I see from beginners. $\\implies$ and $=$ are *two different things*
+and you need to be clear about which one you are using.
 "

server/nng/NNG/Levels/AdvAddition/Level_10.lean

@@ -1,22 +1,74 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
+import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "AdvAddition"
 Level 10
-Title ""
+Title "add_left_eq_zero"
 
 open MyNat
 
 Introduction
 "
+In Lean, `a ≠ b` is *defined to mean* `(a = b) → false`. 
+This means that if you see `a ≠ b` you can *literally treat
+it as saying* `(a = b) → false`. Computer scientists would
+say that these two terms are *definitionally equal*. 
 
+The following lemma, $a+b=0\\implies b=0$, will be useful in inequality world.
+Let me go through the proof, because it introduces several new
+concepts: 
+
+* `cases b`, where `b : mynat`
+* `exfalso`
+* `apply succ_ne_zero`
+
+We're going to prove $a+b=0\\implies b=0$. Here is the
+strategy. Each natural number is either `0` or `succ(d)` for
+some other natural number `d`. So we can start the proof
+with 
+
+`cases b with d,`
+
+and then we have two goals, the case `b = 0` (which you can solve easily)
+and the case `b = succ(d)`, which looks like this:
+
+```
+a d : mynat,
+H : a + succ d = 0
+⊢ succ d = 0
+```
+
+Our goal is impossible to prove. However our hypothesis `H`
+is also impossible, meaning that we still have a chance!
+First let's see why `H` is impossible. We can
+
+`rw add_succ at H,`
+
+to turn `H` into `H : succ (a + d) = 0`. Because
+`succ_ne_zero (a + d)` is a proof that `succ (a + d) ≠ 0`,
+it is also a proof of the implication `succ (a + d) = 0 → false`.
+Hence `succ_ne_zero (a + d) H` is a proof of `false`!
+Unfortunately our goal is not `false`, it's a generic
+false statement. 
+
+Recall however that the `exfalso` command turns any goal into `false`
+(it's logically OK because `false` implies every proposition, true or false).
+You can probably take it from here.
 "
 
-Statement
+Statement -- add_left_eq_zero
-""
+"If $a$ and $b$ are natural numbers such that 
-    : true := by
+$$ a + b = 0, $$
-  trivial
+then $b = 0$."
+    {{a b : ℕ}} (H : a + b = 0) : b = 0 := by
+  induction b with d
+  rfl
+  rw [add_succ] at H
+  exfalso
+  apply succ_ne_zero (a + d)
+  exact H
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_11.lean

@@ -1,22 +1,29 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 11
-Title ""
+Title "add_right_eq_zero"
 
 open MyNat
 
+theorem MyNat.add_left_eq_zero {{a b : ℕ}} (H : a + b = 0) : b = 0 := by sorry
+
 Introduction
 "
-
+We just proved `add_left_eq_zero (a b : mynat) : a + b = 0 → b = 0`.
+Hopefully `add_right_eq_zero` shouldn't be too hard now.
 "
 
 Statement
-""
+"If $a$ and $b$ are natural numbers such that 
-    : true := by
+$$ a + b = 0, $$
-  trivial
+then $a = 0$."
+    {a b : ℕ} : a + b = 0 → a = 0 := by
+  intro H
+  rw [add_comm] at H
+  exact add_left_eq_zero H
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_12.lean

@@ -1,22 +1,30 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 12
-Title ""
+Title "add_one_eq_succ"
 
 open MyNat
 
 Introduction
 "
+We have
 
+  * `succ_eq_add_one (n : mynat) : succ n = n + 1`
+
+but sometimes the other way is also convenient.
 "
 
+theorem succ_eq_add_one (d : ℕ) : succ d = d + 1 := by sorry
+
 Statement
-""
+"For any natural number $d$, we have
-    : true := by
+$$ d+1 = \\operatorname{succ}(d). $$"
-  trivial
+    (d : ℕ) : d + 1 = succ d := by
+  rw [succ_eq_add_one]
+  rfl
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_13.lean

@@ -1,22 +1,32 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 13
-Title ""
+Title "ne_succ_self"
 
 open MyNat
 
 Introduction
 "
-
+The last level in Advanced Addition World is the statement
+that $n\\not=\\operatorname{succ}(n)$. When you've done this
+you've completed Advanced Addition World and can move on
+to Advanced Multiplication World (after first doing
+Multiplication World, if you didn't do it already). 
 "
 
-Statement
+Statement --ne_succ_self
-""
+"For any natural number $n$, we have
-    : true := by
+$$ n \\neq \\operatorname{succ}(n). $$"
-  trivial
+     (n : ℕ) : n ≠ succ n := by
+  induction n with d hd
+  apply zero_ne_succ
+  intro hs
+  apply hd
+  apply succ_inj
+  assumption
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_2.lean

@@ -1,24 +1,53 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 2
-Title ""
+Title "succ_succ_inj"
 
 open MyNat
 
 Introduction
 "
-
+In the below theorem, we need to apply `succ_inj` twice. Once to prove
+$succ(succ(a))=succ(succ(b))\\implies succ(a)=succ(b)$, and then again
+to prove $succ(a)=succ(b)\\implies a=b$. However `succ(a)=succ(b)` is
+nowhere to be found, it's neither an assumption or a goal when we start
+this level. You can make it with `have` or you can use `apply`.
 "
 
 Statement
-""
+"For all naturals $a$ and $b$, if we assume $succ(succ(a))=succ(succ(b))$, then we can
-    : true := by
+deduce $a=b$. "
-  trivial
+    {a b : ℕ} (h : succ (succ a) = succ ( succ b )) : a = b := by
+  apply succ_inj
+  apply succ_inj
+  assumption
 
 Conclusion
 "
+## Sample solutions to this level. 
+
+Make sure you understand them all. And remember that `rw` should not be used
+with `succ_inj` -- `rw` works only with equalities or `↔` statements,
+not implications or functions.
+
+example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
+begin
+  apply succ_inj,
+  apply succ_inj,
+  exact h
+end 
+
+example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
+begin
+  apply succ_inj,
+  exact succ_inj(h),
+end 
 
+example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
+begin
+  exact succ_inj(succ_inj(h)),
+end 
 "

server/nng/NNG/Levels/AdvAddition/Level_3.lean

@@ -1,22 +1,28 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 3
-Title ""
+Title "succ_eq_succ_of_eq"
 
 open MyNat
 
 Introduction
 "
-
+We are going to prove something completely obvious: if $a=b$ then
+$succ(a)=succ(b)$. This is *not* `succ_inj`!
+This is trivial -- we can just rewrite our proof of `a=b`.
+But how do we get to that proof? Use the `intro` tactic.
 "
 
 Statement
-""
+"For all naturals $a$ and $b$, $a=b\\implies succ(a)=succ(b)$. 
-    : true := by
+"
-  trivial
+    {a b : ℕ} : a = b → succ a = succ b := by
+  intro h
+  rw [h]
+  rfl
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_4.lean

@@ -1,22 +1,40 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 4
-Title ""
+Title "eq_iff_succ_eq_succ"
 
 open MyNat
 
 Introduction
 "
+Here is an `iff` goal. You can split it into two goals (the implications in both
+directions) using the `split` tactic, which is how you're going to have to start.
 
+`split,`
+
+Now you have two goals. The first is exactly `succ_inj` so you can close
+it with
+
+`exact succ_inj,`
+
+and the second one you could solve by looking up the name of the theorem
+you proved in the last level and doing `exact <that name>`, or alternatively
+you could get some more `intro` practice and seeing if you can prove it
+using `intro`, `rw` and `refl`.
 "
 
 Statement
-""
+"Two natural numbers are equal if and only if their successors are equal.
-    : true := by
+"
-  trivial
+    (a b : ℕ) : succ a = succ b ↔ a = b := by
+  constructor
+  exact succ_inj
+  intro H
+  rw [H]
+  rfl
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_5.lean

@@ -1,22 +1,36 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 5
-Title ""
+Title "add_right_cancel"
 
 open MyNat
 
 Introduction
 "
-
+The theorem `add_right_cancel` is the theorem that you can cancel on the right
+when you're doing addition -- if `a + t = b + t` then `a = b`. After `intro h`
+I'd recommend induction on `t`. Don't forget that `rw add_zero at h` can be used
+to do rewriting of hypotheses rather than the goal.
 "
 
 Statement
-""
+"On the set of natural numbers, addition has the right cancellation property.
-    : true := by
+In other words, if there are natural numbers $a, b$ and $c$ such that
-  trivial
+$$ a + t = b + t, $$
+then we have $a = b$."
+    (a t b : ℕ) : a + t = b + t → a = b := by
+  intro h
+  induction t with d hd
+  rw [add_zero] at h
+  rw [add_zero] at h
+  exact h
+  apply hd
+  rw [add_succ] at h
+  rw [add_succ] at h
+  exact succ_inj h
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_6.lean

@@ -1,22 +1,32 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 6
-Title ""
+Title "add_left_cancel"
 
 open MyNat
 
 Introduction
 "
+The theorem `add_left_cancel` is the theorem that you can cancel on the left
+when you're doing addition -- if `t + a = t + b` then `a = b`. 
+There is a three-line proof which ends in `exact add_right_cancel a t b` (or even
+`exact add_right_cancel _ _ _`); this
+strategy involves changing the goal to the statement of `add_right_cancel` somehow.
 
 "
 
 Statement
-""
+"On the set of natural numbers, addition has the left cancellation property.
-    : true := by
+In other words, if there are natural numbers $a, b$ and $t$ such that
-  trivial
+$$ t + a = t + b, $$
+then we have $a = b$."
+    (t a b : ℕ) : t + a = t + b → a = b := by
+  rw [add_comm]
+  rw [add_comm t]
+  exact add_right_cancel a t b
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_7.lean

@@ -1,23 +1,34 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 7
-Title ""
+Title "add_right_cancel_iff"
 
 open MyNat
 
 Introduction
 "
+It's sometimes convenient to have the \"if and only if\" version
+of theorems like `add_right_cancel`. Remember that you can use `split`
+to split an `↔` goal into the `→` goal and the `←` goal.
 
-"
+## Pro tip:
 
-Statement
+`exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\"
-""
+"
-    : true := by
-  trivial
 
+Statement --add_right_cancel_iff 
+"For all naturals $a$, $b$ and $t$, 
+$$ a + t = b + t\\iff a=b. $$
+"
+    (t a b : ℕ) :  a + t = b + t ↔ a = b := by
+  constructor
+  exact add_right_cancel _ _ _ -- done that way already,
+  intro H -- H : a = b,
+  rw [H]
+  rfl
 Conclusion
 "
 

server/nng/NNG/Levels/AdvAddition/Level_8.lean

@@ -1,22 +1,29 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 8
-Title ""
+Title "eq_zero_of_add_right_eq_self"
 
 open MyNat
 
 Introduction
 "
-
+The lemma you're about to prove will be useful when we want to prove that $\\leq$ is antisymmetric.
+There are some wrong paths that you can take with this one.
 "
 
-Statement
+Statement --eq_zero_of_add_right_eq_self
-""
+"If $a$ and $b$ are natural numbers such that 
-    : true := by
+$$ a + b = a, $$
-  trivial
+then $b = 0$."
+    {a b : ℕ} : a + b = a → b = 0 := by
+  intro h
+  apply add_left_cancel a
+  rw [h]
+  rw [add_zero]
+  rfl
 
 Conclusion
 "

server/nng/NNG/Levels/AdvAddition/Level_9.lean

@@ -1,22 +1,32 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
 Level 9
-Title ""
+Title "succ_ne_zero"
 
 open MyNat
 
 Introduction
 "
+Levels 9 to 13 introduce the last axiom of Peano, namely
+that $0\\not=\\operatorname{succ}(a)$. The proof of this is called `zero_ne_succ a`. 
 
+`zero_ne_succ (a : mynat) : 0 ≠ succ(a)`
+
+The `symmetry` tactic will turn any goal of the form `R x y` into `R y x`,
+if `R` is a symmetric binary relation (for example `=` or `≠`).
+In particular, you can prove `succ_ne_zero` below by first using
+`symmetry` and then `exact zero_ne_succ a`. 
 "
 
-Statement
+Statement -- succ_ne_zero
-""
+"Zero is not the successor of any natural number."
-    : true := by
+    (a : ℕ) : succ a ≠ 0 := by
-  trivial
+  apply Ne.symm
+  exact zero_ne_succ a
+
 
 Conclusion
 "

server/nng/NNG/Levels/AdvMultiplication/Level_1.lean

@@ -1,22 +1,55 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.Multiplication
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
 Level 1
-Title ""
+Title "mul_pos"
 
 open MyNat
 
 Introduction
 "
+Welcome to Advanced Multiplication World! Before attempting this
+world you should have completed seven other worlds, including
+Multiplication World and Advanced Addition World. There are four
+levels in this world.
+
+Recall that if `b : mynat` is a hypothesis and you do `cases b with n`,
+your one goal will split into two goals, 
+namely the cases `b = 0` and `b = succ(n)`. So `cases` here is like
+a weaker version of induction (you don't get the inductive hypothesis).
+
+## Tricks
+
+1) if your goal is `⊢ X ≠ Y` then `intro h` will give you `h : X = Y` and
+a goal of `⊢ false`. This is because `X ≠ Y` *means* `(X = Y) → false`.
+Conversely if your goal is `false` and you have `h : X ≠ Y` as a hypothesis
+then `apply h` will turn the goal into `X = Y`.
+
+2) if `hab : succ (3 * x + 2 * y + 1) = 0` is a hypothesis and your goal is `⊢ false`,
+then `exact succ_ne_zero _ hab` will solve the goal, because Lean will figure
+out that `_` is supposed to be `3 * x + 2 * y + 1`.
 
 "
 
 Statement
-""
+"The product of two non-zero natural numbers is non-zero."
-    : true := by
+    (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 := by
-  trivial
+  intro ha hb
+  intro hab
+  induction b with b
+  apply hb
+  rfl
+  rw [mul_succ] at hab
+  apply ha
+  induction a with a
+  rfl
+  rw [add_succ] at hab
+  exfalso
+  exact succ_ne_zero _ hab
 
 Conclusion
 "

server/nng/NNG/Levels/AdvMultiplication/Level_2.lean

@@ -1,22 +1,34 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.Multiplication
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
 Level 2
-Title ""
+Title "eq_zero_or_eq_zero_of_mul_eq_zero"
 
 open MyNat
 
 Introduction
 "
-
+A variant on the previous level.
 "
 
-Statement
+Statement -- eq_zero_or_eq_zero_of_mul_eq_zero
-""
+"If $ab = 0$, then at least one of $a$ or $b$ is equal to zero."
-    : true := by
+    (a b : ℕ) (h : a * b = 0) :
-  trivial
+  a = 0 ∨ b = 0 := by
+  induction a with d
+  left
+  rfl
+  induction b with e he
+  right
+  rfl
+  exfalso
+  rw [mul_succ] at h
+  rw [add_succ] at h
+  exact succ_ne_zero _ h
 
 Conclusion
 "

server/nng/NNG/Levels/AdvMultiplication/Level_3.lean

@@ -1,22 +1,39 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.Multiplication
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
 Level 3
-Title ""
+Title "mul_eq_zero_iff"
 
 open MyNat
 
 Introduction
 "
-
+Now you have `eq_zero_or_eq_zero_of_mul_eq_zero` this is pretty straightforward.
 "
 
+axiom eq_zero_or_eq_zero_of_mul_eq_zero (a b : ℕ) (h : a * b = 0) : a = 0 ∨ b = 0 
+axiom zero_mul (a : ℕ) : 0 * a = 0
+
 Statement
-""
+"$ab = 0$, if and only if at least one of $a$ or $b$ is equal to zero.
-    : true := by
+"
-  trivial
+    (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 := by
+  constructor
+  intro h
+  exact eq_zero_or_eq_zero_of_mul_eq_zero a b h
+  intro hab
+  rcases hab with hab | hab
+  rw [hab]
+  rw [zero_mul]
+  rfl
+  rw [hab]
+  rw [mul_zero]
+  rfl
+
 
 Conclusion
 "

server/nng/NNG/Levels/AdvMultiplication/Level_4.lean

@@ -1,22 +1,63 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.Multiplication
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
 Level 4
-Title ""
+Title "mul_left_cancel"
 
 open MyNat
 
 Introduction
 "
+This is the last of the bonus multiplication levels.
+`mul_left_cancel` will be useful in inequality world.
 
+People find this level hard. I have probably had more questions about this
+level than all the other levels put together, in fact. Many levels in this
+game can just be solved by \"running at it\" -- do induction on one of the
+variables, keep your head, and you're done. In fact, if you like a challenge,
+it might be instructive if you stop reading after the end of this paragraph and try solving this level now by induction,
+seeing the trouble you run into, and reading the rest of these comments afterwards. This level
+has a sting in the tail. If you are a competent mathematician, try
+and figure out what is going on. Write down a maths proof of the
+theorem in this level. Exactly what statement do you want to prove
+by induction? It is subtle.
+
+Ok so here are some spoilers. The problem with naively running at it, is that if you try induction on,
+say, $c$, then you are imagining a and b as fixed, and your inductive
+hypothesis $P(c)$ is $ab=ac \\implies b=c$. So for your inductive step
+you will be able to assume $ab=ad \\implies b=d$ and your goal will
+be to show $ab=a(d+1) \\implies b=d+1$. When you also assume $ab=a(d+1)$
+you will realise that your inductive hypothesis is *useless*, because
+$ab=ad$ is not true! The statement $P(c)$ (with $a$ and $b$ regarded
+as constants) is not provable by induction.
+
+What you *can* prove by induction is the following *stronger* statement.
+Imagine $a\not=0$ as fixed, and then prove \"for all $b$, if $ab=ac$ then $b=c$\"
+by induction on $c$. This gives us the extra flexibility we require.
+Note that we are quantifying over all $b$ in the inductive hypothesis -- it
+is essential that $b$ is not fixed. 
+
+You can do this in two ways in Lean -- before you start the induction
+you can write `revert b,`. The `revert` tactic is the opposite of the `intro`
+tactic; it replaces the `b` in the hypotheses with \"for all $b$\" in the goal.
+
+Alternatively, you can write `induction c with d hd
+generalizing b` as the first line of the proof. 
+
+If you do not modify your technique in this way, then this level seems
+to be impossible (judging by the comments I've had about it!)
 "
 
 Statement
-""
+"If $a \\neq 0$, $b$ and $c$ are natural numbers such that
-    : true := by
+$ ab = ac, $
-  trivial
+then $b = c$."
+    (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c := by
+  sorry
 
 Conclusion
 "

server/nng/NNG/Levels/AdvProposition/Level_1.lean

@@ -4,17 +4,28 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "AdvProposition"
 Level 1
-Title ""
+Title "the `split` tactic"
 
 open MyNat
 
 Introduction
 "
-
+In this world we will learn five key tactics needed to solve all the
+levels of the Natural Number Game, namely `split`, `cases`, `left`, `right`, and `exfalso`.
+These, and `use` (which we'll get to in Inequality World) are all the
+tactics you will need to beat all the levels of the game.
+
+## Level 1: the `split` tactic.
+
+The logical symbol `∧` means \"and\". If $P$ and $Q$ are propositions, then
+$P\\land Q$ is the proposition \"$P$ and $Q$\". If your *goal* is `P ∧ Q` then
+you can make progress with the `split` tactic, which turns one goal `⊢ P ∧ Q`
+into two goals, namely `⊢ P` and `⊢ Q`. In the level below, after a `split`,
+you will be able to finish off the goals with the `exact` tactic.
 "
 
 Statement
-""
+"If $P$ and $Q$ are true, then $P\\land Q$ is true."
     (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
   constructor
   exact p

server/nng/NNG/Levels/AdvProposition/Level_10.lean

@@ -5,17 +5,54 @@ import Std.Tactic.RCases
 Game "NNG"
 World "AdvProposition"
 Level 10
-Title ""
+Title "Level 10: the law of the excluded middle."
 
 open MyNat
 
 Introduction
 "
+We proved earlier that `(P → Q) → (¬ Q → ¬ P)`. The converse,
+that `(¬ Q → ¬ P) → (P → Q)` is certainly true, but trying to prove
+it using what we've learnt so far is impossible (because it is not provable in
+constructive logic). For example, after
 
+```
+intro h,
+intro p,
+repeat {rw not_iff_imp_false at h},
+```
+
+in the below, you are left with
+```
+P Q : Prop,
+h : (Q → false) → P → false
+p : P
+⊢ Q
+```
+
+The tools you have are not sufficient to continue. But you can just
+prove this, and any other basic lemmas of this form like `¬ ¬ P → P`,
+using the `by_cases` tactic. Instead of starting with all the `intro`s,
+try this instead:
+
+`by_cases p : P; by_cases q : Q,`
+
+**Note the semicolon**! It means \"do the next tactic to all the goals, not just the top one\".
+After it, there are four goals, one for each of the four possibilities PQ=TT, TF, FT, FF.
+You can see that `p` is a proof of `P` in some of the goals, and a proof of `¬ P` in others.
+Similar comments apply to `q`. 
+
+`repeat {cc}` then finishes the job.
+
+This approach assumed that `P ∨ ¬ P` was true; the `by_cases` tactic just does `cases` on
+this result. This is called the law of the excluded middle, and it cannot be proved just
+using tactics such as `intro` and `apply`.
 "
 
 Statement
-""
+"If $P$ and $Q$ are true/false statements, then
+$$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$ 
+"
     (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by
   by_cases p : P
   · by_cases q : Q
@@ -32,5 +69,11 @@ Statement
 
 Conclusion
 "
+OK that's enough logic -- now perhaps it's time to go on to Advanced Addition World!
+Get to it via the main menu.
+
+## Pro tip
+
+In fact the tactic `tauto!` just kills this goal (and many other logic goals) immediately.
 
 "

server/nng/NNG/Levels/AdvProposition/Level_2.lean

@@ -5,19 +5,34 @@ import Std.Tactic.RCases
 Game "NNG"
 World "AdvProposition"
 Level 2
-Title ""
+Title "the `cases` tactic"
 
 open MyNat
 
 Introduction
 "
+If `P ∧ Q` is in the goal, then we can make progress with `split`.
+But what if `P ∧ Q` is a hypothesis? In this case, the `cases` tactic will enable
+us to extract proofs of `P` and `Q` from this hypothesis.
 
+The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,
+symmetry of the \"and\" relation. The obvious first move is
+
+`intro h,`
+
+because the goal is an implication and this tactic is guaranteed
+to make progress. Now `h : P ∧ Q` is a hypothesis, and
+
+`cases h with p q,`
+
+will change `h`, the proof of `P ∧ Q`, into two proofs `p : P`
+and `q : Q`. From there, `split` and `exact` will get you home.
 "
 
 set_option tactic.hygienic false
 
 Statement --and_symm
-""
+"If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. "
     (P Q : Prop) : P ∧ Q → Q ∧ P :=  by
   intro h
   rcases h with ⟨p, q⟩

server/nng/NNG/Levels/AdvProposition/Level_3.lean

@@ -5,7 +5,7 @@ import Std.Tactic.RCases
 Game "NNG"
 World "AdvProposition"
 Level 3
-Title ""
+Title "and_trans"
 
 open MyNat
 
@@ -15,7 +15,8 @@ Introduction
 "
 
 Statement --and_trans
-""
+"If $P$, $Q$ and $R$ are true/false statements, then $P\\land Q$ and
+$Q\\land R$ together imply $P\\land R$."
     (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by
   intro hpq
   intro hqr

server/nng/NNG/Levels/AdvProposition/Level_4.lean

@@ -11,11 +11,16 @@ open MyNat
 
 Introduction
 "
+The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `cases`
+and `split` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need
+to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to. After an initial
+`intro h,` you can type `cases h with hpq hqp` to break `h : P ↔ Q` into its constituent parts.
 
 "
 
 Statement --iff_trans
-""
+"If $P$, $Q$ and $R$ are true/false statements, then
+$P\\iff Q$ and $Q\\iff R$ together imply $P\\iff R$."
     (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
   intro hpq
   intro hqr

server/nng/NNG/Levels/AdvProposition/Level_5.lean

@@ -5,17 +5,42 @@ import Std.Tactic.RCases
 Game "NNG"
 World "AdvProposition"
 Level 5
-Title ""
+Title "`iff_trans` easter eggs."
 
 open MyNat
 
 Introduction
 "
+Let's try `iff_trans` again. Try proving it in other ways.
 
+### A trick.
+
+Instead of using `cases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P`
+directly with `h.1` and `h.2`. So you can solve this level with
+
+```
+intros hpq hqr, 
+split,
+intro p,
+apply hqr.1,
+...
+```
+
+### Another trick
+
+Instead of using `cases` on `h : P ↔ Q`, you can just `rw h`, and this will change all `P`s to `Q`s
+in the goal. You can use this to create a much shorter proof. Note that
+this is an argument for *not* running the `cases` tactic on an iff statement;
+you cannot rewrite one-way implications, but you can rewrite two-way implications.
+
+### Another trick
+
+`cc` works on this sort of goal too.
 "
 
 Statement --iff_trans
-""
+"If $P$, $Q$ and $R$ are true/false statements, then `P ↔ Q` and `Q ↔ R` together imply `P ↔ R`.
+"
     (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
   intro hpq hqr
   constructor

server/nng/NNG/Levels/AdvProposition/Level_6.lean

@@ -7,17 +7,25 @@ import Mathlib.Tactic.LeftRight
 Game "NNG"
 World "AdvProposition"
 Level 6
-Title ""
+Title "Or, and the `left` and `right` tactics."
 
 open MyNat
 
 Introduction
 "
-
+`P ∨ Q` means \"$P$ or $Q$\". So to prove it, you
+need to choose one of `P` or `Q`, and prove that one.
+If `⊢ P ∨ Q` is your goal, then `left` changes this
+goal to `⊢ P`, and `right` changes it to `⊢ Q`.
+Note that you can take a wrong turn here. Let's
+start with trying to prove $Q\\implies (P\\lor Q)$.
+After the `intro`, one of `left` and `right` leads
+to an impossible goal, the other to an easy finish.
 "
 
 Statement
-""
+"If $P$ and $Q$ are true/false statements, then
+$$Q\\implies(P\\lor Q).$$ "
     (P Q : Prop) : Q → (P ∨ Q) := by
   intro q
   right

server/nng/NNG/Levels/AdvProposition/Level_7.lean

@@ -6,17 +6,25 @@ import Mathlib.Tactic.LeftRight
 Game "NNG"
 World "AdvProposition"
 Level 7
-Title ""
+Title "`or_symm`"
 
 open MyNat
 
 Introduction
 "
-
+Proving that $(P\\lor Q)\\implies(Q\\lor P)$ involves an element of danger.
+`intro h,` is the obvious start. But now,
+even though the goal is an `∨` statement, both `left` and `right` put
+you in a situation with an impossible goal. Fortunately, after `intro h,`
+you can do `cases h with p q`. Then something new happens: because
+there are two ways to prove `P ∨ Q` (namely, proving `P` or proving `Q`),
+the `cases` tactic turns one goal into two, one for each case. You should
+be able to make it home from there. 
 "
 
 Statement --or_symm
-""
+"If $P$ and $Q$ are true/false statements, then
+$$P\\lor Q\\implies Q\\lor P.$$ "
     (P Q : Prop) : P ∨ Q → Q ∨ P := by
   intro h
   rcases h with p | q

server/nng/NNG/Levels/AdvProposition/Level_8.lean

@@ -6,17 +6,21 @@ import Mathlib.Tactic.LeftRight
 Game "NNG"
 World "AdvProposition"
 Level 8
-Title ""
+Title "`and_or_distrib_left`"
 
 open MyNat
 
 Introduction
 "
-
+We know that `x(y+z)=xy+xz` for numbers, and this
+is called distributivity of multiplication over addition.
+The same is true for `∧` and `∨` -- in fact `∧` distributes
+over `∨` and `∨` distributes over `∧`. Let's prove one of these.
 "
 
 Statement --and_or_distrib_left
-""
+"If $P$. $Q$ and $R$ are true/false statements, then
+$$P\\land(Q\\lor R)\\iff(P\\land Q)\\lor (P\\land R).$$ "
     (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
   constructor
   intro h
@@ -45,5 +49,13 @@ Statement --and_or_distrib_left
 
 Conclusion
 "
+## Pro tip
+
+Did you spot the import? What do you think it does?
+
+If you follow the instructions at
+<a href=\"https://github.com/leanprover-community/mathlib#installation\" target=\"blank\">the mathlib github page</a>
+you will be able to install Lean and mathlib on your own system, and then you can create a new project
+and experiment with such imports yourself.
 
 "

server/nng/NNG/Levels/AdvProposition/Level_9.lean

@@ -8,17 +8,30 @@ import NNG.MyNat.Theorems.Proposition
 Game "NNG"
 World "AdvProposition"
 Level 9
-Title ""
+Title "`exfalso` and proof by contradiction. "
 
 open MyNat
 
 Introduction
 "
+You already know enough to embark on advanced addition world. But here are just a couple
+more things.
+
+## Level 9: `exfalso` and proof by contradiction. 
+
+It's certainly true that $P\\land(\\lnot P)\\implies Q$ for any propositions $P$
+and $Q$, because the left hand side of the implication is false. But how do
+we prove that `false` implies any proposition $Q$? A cheap way of doing it in
+Lean is using the `exfalso` tactic, which changes any goal at all to `false`. 
+You might think this is a step backwards, but if you have a hypothesis `h : ¬ P`
+then after `rw not_iff_imp_false at h,` you can `apply h,` to make progress. 
+Try solving this level without using `cc` or `tauto`, but using `exfalso` instead.
 
 "
 
 Statement --contra
-""
+"If $P$ and $Q$ are true/false statements, then
+$$(P\\land(\\lnot P))\\implies Q.$$"
   (P Q : Prop) : (P ∧ ¬ P) → Q := by
   intro h
   rcases h with ⟨p, np ⟩
@@ -32,5 +45,27 @@ NewTactic exfalso contradiction
 
 Conclusion
 "
+## Pro tip.
+
+`¬ P` is actually `P → false` *by definition*. Try
+commenting out `rw not_iff_imp_false at ...` by putting two minus signs `--`
+before the `rw`. Does it still compile?
+-/
+
+/- Tactic : exfalso
+
+## Summary
+
+`exfalso` changes your goal to `false`. 
+
+## Details
+
+We know that `false` implies `P` for any proposition `P`, and so if your goal is `P`
+then you should be able to `apply` `false → P` and reduce your goal to `false`. This
+is what the `exfalso` tactic does. The theorem that `false → P` is called `false.elim`
+so one can achieve the same effect with `apply false.elim`. 
 
+This tactic can be used in a proof by contradiction, where the hypotheses are enough
+to deduce a contradiction and the goal happens to be some random statement (possibly
+a false one) which you just want to simplify to `false`.
 "

server/nng/NNG/Levels/Function/Level_9.lean

@@ -10,11 +10,16 @@ open MyNat
 
 Introduction
 "
+I asked around on Zulip and apparently there is not a tactic for this, perhaps because
+this level is rather artificial. In world 6 we will see a variant of this example
+which can be solved by a tactic. It would be an interesting project to make a tactic
+which could solve this sort of level in Lean.
 
+You can of course work both forwards and backwards, or you could crack and draw a picture.
 "
 
 Statement
-""
+"Given a bunch of functions, we can define another one."
     (A B C D E F G H I J K L : Type)
     (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
     (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
@@ -32,5 +37,6 @@ Statement
 
 Conclusion
 "
-
+That's the end of Function World! Next it's Proposition world, and the tactics you've learnt in Function World are enough
+to solve all nine levels! In fact, the levels in Proposition world might look strangely familiar$\\ldots$.
 "

server/nng/NNG/Levels/Inequality.lean

@@ -22,4 +22,29 @@ Title "Inequality World"
 
 Introduction
 "
+A new import, giving us a new definition. If `a` and `b` are naturals,
+`a ≤ b` is *defined* to mean
+
+`∃ (c : mynat), b = a + c`
+
+The upside-down E means \"there exists\". So in words, $a\\le b$
+if and only if there exists a natural $c$ such that $b=a+c$. 
+
+If you really want to change an `a ≤ b` to `∃ c, b = a + c` then
+you can do so with `rw le_iff_exists_add`:
+
+```
+le_iff_exists_add (a b : mynat) :
+  a ≤ b ↔ ∃ (c : mynat), b = a + c
+```
+
+But because `a ≤ b` is *defined as* `∃ (c : mynat), b = a + c`, you
+do not need to `rw le_iff_exists_add`, you can just pretend when you see `a ≤ b`
+that it says `∃ (c : mynat), b = a + c`. You will see a concrete
+example of this below.
+
+A new construction like `∃` means that we need to learn how to manipulate it.
+There are two situations. Firstly we need to know how to solve a goal
+of the form `⊢ ∃ c, ...`, and secondly we need to know how to use a hypothesis
+of the form `∃ c, ...`. 
 "

server/nng/NNG/Levels/Inequality/Level_1.lean

@@ -1,22 +1,60 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+--import Mathlib.Tactic.Ring
 
 Game "NNG"
 World "Inequality"
 Level 1
-Title ""
+Title "the `use` tactic"
 
 open MyNat
 
 Introduction
 "
+The goal below is to prove $x\\le 1+x$ for any natural number $x$. 
+First let's turn the goal explicitly into an existence problem with
 
+`rw le_iff_exists_add,`
+
+and now the goal has become `∃ c : mynat, 1 + x = x + c`. Clearly
+this statement is true, and the proof is that $c=1$ will work (we also
+need the fact that addition is commutative, but we proved that a long
+time ago). How do we make progress with this goal?
+
+The `use` tactic can be used on goals of the form `∃ c, ...`. The idea
+is that we choose which natural number we want to use, and then we use it.
+So try
+
+`use 1,`
+
+and now the goal becomes `⊢ 1 + x = x + 1`. You can solve this by
+`exact add_comm 1 x`, or if you are lazy you can just use the `ring` tactic,
+which is a powerful AI which will solve any equality in algebra which can
+be proved using the standard rules of addition and multiplication. Now
+look at your proof. We're going to remove a line.
+
+## Important
+
+An important time-saver here is to note that because `a ≤ b` is *defined*
+as `∃ c : mynat, b = a + c`, you *do not need to write* `rw le_iff_exists_add`.
+The `use` tactic will work directly on a goal of the form `a ≤ b`. Just
+use the difference `b - a` (note that we have not defined subtraction so
+this does not formally make sense, but you can do the calculation in your head).
+If you have written `rw le_iff_exists_add` below, then just put two minus signs `--`
+before it and comment it out. See that the proof still compiles.
 "
 
-Statement
+axiom add_comm (a b : ℕ) : a + b = b + a
-""
+
-    : true := by
+Statement --one_add_le_self
-  trivial
+"If $x$ is a natural number, then $x\\le 1+x$.
+"
+    (x : ℕ) : x ≤ 1 + x := by
+  rw [le_iff_exists_add]
+  use 1
+  rw [add_comm]
+  rfl
   
 Conclusion
 "

server/nng/NNG/Levels/Inequality/Level_10.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_11.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_12.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_13.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_14.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_15.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_16.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_17.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_2.lean

@@ -1,22 +1,26 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"
 Level 2
-Title ""
+Title "le_rfl"
 
 open MyNat
 
 Introduction
 "
-
+Here's a nice easy one.
 "
 
 Statement
-""
+"The $\\le$ relation is reflexive. In other words, if $x$ is a natural number,
-    : true := by
+then $x\\le x$."
-  trivial
+    (x : ℕ) : x ≤ x := by
+  use 0
+  rw [add_zero]
+  rfl
 
 Conclusion
 "

server/nng/NNG/Levels/Inequality/Level_3.lean

@@ -1,22 +1,57 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
+import Std.Tactic.RCases
 
 Game "NNG"
 World "Inequality"
 Level 3
-Title ""
+Title "le_succ_of_le"
 
 open MyNat
 
 Introduction
 "
+We have seen how the `use` tactic makes progress on goals of the form `⊢ ∃ c, ...`.
+But what do we do when we have a *hypothesis* of the form `h : ∃ c, ...`?
+The hypothesis claims that there exists some natural number `c` with some
+property. How are we going to get to that natural number `c`? It turns out
+that the `cases` tactic can be used (just like it was used to extract
+information from `∧` and `∨` and `↔` hypotheses). Let me talk you through
+the proof of $a\\le b\\implies a\\le\\operatorname{succ}(b)$.
+
+The goal is an implication so we clearly want to start with 
+
+`intro h,`
+
+. After this, if you *want*, you can do something like
+
+`rw le_iff_exists_add at h ⊢,`
+
+(get the sideways T with `\\|-` then space). This changes the `≤` into
+its `∃` form in `h` and the goal -- but if you are happy with just
+*imagining* the `∃` whenever you read a `≤` then you don't need to do this line.
+
+Our hypothesis `h` is now `∃ (c : mynat), b = a + c` (or `a ≤ b` if you
+elected not to do the definitional rewriting) so
+
+`cases h with c hc,`
+
+gives you the natural number `c` and the hypothesis `hc : b = a + c`.
+Now use `use` wisely and you're home.
 
 "
 
 Statement
-""
+"For all naturals $a$, $b$, if $a\\leq b$ then $a\\leq \\operatorname{succ}(b)$. 
-    : true := by
+"
-  trivial
+    (a b : ℕ) : a ≤ b → a ≤ (succ b) := by
+  intro h
+  rcases h with ⟨c, hc⟩
+  rw [hc]
+  use c + 1
+  sorry
+  --rfl
 
 Conclusion
 "

server/nng/NNG/Levels/Inequality/Level_4.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_5.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_6.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_7.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_8.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Inequality/Level_9.lean

@@ -1,5 +1,6 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+import NNG.MyNat.LE
+import Mathlib.Tactic.Use
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Power.lean

@@ -13,4 +13,26 @@ Title "Power World"
 
 Introduction
 "
+A new world with seven levels. And a new import!
+This import gives you the power to make powers of your
+natural numbers. It is defined by recursion, just like addition and multiplication.
+Here are the two new axioms:
+
+  * `pow_zero (a : mynat) : a ^ 0 = 1`
+  * `pow_succ (a b : mynat) : a ^ succ(b) = a ^ b * a`
+
+The power function has various relations to addition and multiplication.
+If you have gone through levels 1--6 of addition world and levels 1--9 of
+multiplication world, you should have no trouble with this world:
+The usual tactics `induction`, `rw` and `refl` should see you through.
+You might want to fiddle with the
+drop-down menus on the left so you can see which theorems of Power World
+you have proved at any given time. Addition and multiplication -- we
+have a solid API for them now, i.e. if you need something about addition
+or multiplication, it's probably already in the library we have built.
+Collectibles are indication that we are proving the right things.
+
+The levels in this world were designed by Sian Carey, a UROP student
+at Imperial College London, funded by a Mary Lister McCammon Fellowship,
+in the summer of 2019. Thanks Sian!
 "

server/nng/NNG/Levels/Power/Level_1.lean

@@ -4,7 +4,7 @@ import NNG.Metadata
 Game "NNG"
 World "Power"
 Level 1
-Title ""
+Title "zero_pow_zero"
 
 open MyNat
 
@@ -15,7 +15,7 @@ Introduction
 
 Statement
 "$0 ^ 0 = 1$"
-    : true := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by
+    : (0 : ℕ) ^ 0 = (1 : ℕ) := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by
   trivial
 
 Conclusion

server/nng/NNG/Levels/Power/Level_4.lean

@@ -22,3 +22,4 @@ Conclusion
 "
 
 "
+  

server/nng/NNG/Levels/Proposition/Level_1.lean

@@ -4,18 +4,72 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 1
-Title ""
+Title "the `exact` tactic"
 
 open MyNat
 
 Introduction
 "
+A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`.
+Just like we can have concrete sets in Lean like `ℕ`, and abstract
+sets called things like `X`, we can also have concrete propositions like
+`2 + 2 = 5` and abstract propositions called things like `P`. 
 
+Mathematicians are very good at conflating a theorem with its proof.
+They might say \"now use theorem 12 and we're done\". What they really
+mean is \"now use the proof of theorem 12...\" (i.e. the fact that we proved
+it already). Particularly problematic is the fact that mathematicians
+use the word Proposition to mean \"a relatively straightforward statement
+which is true\" and computer scientists use it to mean \"a statement of
+arbitrary complexity, which might be true or false\". Computer scientists
+are far more careful about distinguishing between a proposition and a proof.
+For example: `x + 0 = x` is a proposition, and `add_zero x`
+is its proof. The convention we'll use is capital letters for propositions
+and small letters for proofs. 
 "
 
 Statement
-""
+"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true."
     (P Q : Prop) (p : P) (h : P → Q) : Q := by
+Hint
+"
+Here `P` is the true/false statement (the statement of proposition), and `p` is its proof.
+It's like `P` being the set and `p` being the element. In fact computer scientists
+sometimes think about the following analogy: propositions are like sets,
+and their proofs are like their elements. 
+
+## What's going on in this world? 
+
+We're going to learn about manipulating propositions and proofs.
+Fortunately, we don't need to learn a bunch of new tactics -- the
+ones we just learnt (`exact`, `intro`, `have`, `apply`) will be perfect.
+
+The levels in proposition world are \"back to normal\", we're proving
+theorems, not constructing elements of sets. Or are we?
+
+If you delete the sorry below then your local context will look like this:
+
+In this situation, we have true/false statements $P$ and $Q$,
+a proof $p$ of $P$, and $h$ is the hypothesis that $P\\implies Q$.
+Our goal is to construct a proof of $Q$. It's clear what to do
+*mathematically* to solve this goal, $P$ is true and $P$ implies $Q$
+so $Q$ is true. But how to do it in Lean?
+
+Adopting a point of view wholly unfamiliar to many mathematicians,
+Lean interprets the hypothesis $h$ as a function from proofs
+of $P$ to proofs of $Q$, so the rather surprising approach
+
+`exact h p`
+
+works to close the goal.
+
+Note that `exact h P` (with a capital P) won't work;
+this is a common error I see from beginners. \"We're trying to solve `P`
+so it's exactly `P`\". The goal states the *theorem*, your job is to
+construct the *proof*. $P$ is not a proof of $P$, it's $p$ that is a proof of $P$. 
+
+In Lean, Propositions, like sets, are types, and proofs, like elements of sets, are terms.
+"
 exact h p
 
 Conclusion

server/nng/NNG/Levels/Proposition/Level_2.lean

@@ -4,19 +4,61 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 2
-Title ""
+Title "intro"
 
 open MyNat
 
 Introduction
 "
+Let's prove an implication. Let $P$ be a true/false statement,
+and let's prove that $P\\implies P$. You can see that the goal of this level is
+`P → P`. Constructing a term
+of type `P → P` (which is what solving this goal *means*) in this
+case amounts to proving that $P\\implies P$, and computer scientists
+think of this as coming up with a function which sends proofs of $P$
+to proofs of $P$.
+
+To define an implication $P\\implies Q$ we need to choose an arbitrary
+proof $p : P$ of $P$ and then, perhaps using $p$, construct a proof
+of $Q$.  The Lean way to say \"let's assume $P$ is true\" is `intro p`,
+i.e., \"let's assume we have a proof of $P$\".
+
+## Note for worriers.
+
+Those of you who know
+something about the subtle differences between truth and provability
+discovered by Goedel -- these are not relevant here. Imagine we are
+working in a fixed model of mathematics, and when I say \"proof\"
+I actually mean \"truth in the model\", or \"proof in the metatheory\".
+
+## Rule of thumb: 
+
+If your goal is to prove `P → Q` (i.e. that $P\\implies Q$)
+then `intro p`, meaning \"assume $p$ is a proof of $P$\", will make progress.
 
 "
 
 Statement
-""
+"If $P$ is a proposition then $P\\implies P$."
     {P : Prop} : P → P := by
+  Hint "
+  To solve this goal, you have to come up with a function from
+  `P` (thought of as the set of proofs of $P$!) to itself. Start with
+
+  `intro p`
+  "
   intro p
+  Hint "
+  Our job now is to construct a proof of $P$. But $p$ is a proof of $P$.
+  So
+
+  `exact p`
+
+  will close the goal. Note that `exact P` will not work -- don't
+  confuse a true/false statement (which could be false!) with a proof.
+  We will stick with the convention of capital letters for propositions
+  and small letters for proofs.
+  "
   exact p
 
 Conclusion

server/nng/NNG/Levels/Proposition/Level_3.lean

@@ -4,17 +4,58 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 3
-Title ""
+Title "have"
 
 open MyNat
 
 Introduction
 "
+Say you have a whole bunch of propositions and implications between them,
+and your goal is to build a certain proof of a certain proposition.
+If it helps, you can build intermediate proofs of other propositions
+along the way, using the `have` command. `have q : Q := ...` is the Lean analogue
+of saying \"We now see that we can prove $Q$, because...\"
+in the middle of a proof.
+It is often not logically necessary, but on the other hand
+it is very convenient, for example it can save on notation, or
+it can break proofs up into smaller steps.
 
+In the level below, we have a proof of $P$ and we want a proof
+of $U$; during the proof we will construct proofs of
+of some of the other propositions involved. The diagram of
+propositions and implications looks like this pictorially:
+
+![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg)
+
+and so it's clear how to deduce $U$ from $P$.
+Indeed, we could solve this level in one move by typing
+
+`exact l(j(h(p))),`
+
+But let us instead stroll more lazily through the level.
+We can start by using the `have` tactic to make a proof of $Q$:
+
+`have q := h(p),`
+
+and then we note that $j(q)$ is a proof of $T$:
+
+`have t : T := j(q),`
+
+(note how we explicitly told Lean what proposition we thought $t$ was
+a proof of, with that `: T` thing before the `:=`) 
+and we could even define $u$ to be $l(t)$:
+
+`have u : U := l(t),`
+
+and then finish the level with
+
+`exact u,`
+
+. 
 "
 
 Statement
-""
+"In the maze of logical implications above, if $P$ is true then so is $U$."
     (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R)
     (j : Q → T) (k : S → T) (l : T → U) : U := by
   have q := h p
@@ -26,5 +67,27 @@ DisabledTactic apply
 
 Conclusion
 "
+If you solved the level using `have`, then click on the last line of your proof
+(you do know you can move your cursor around with the arrow keys
+and explore your proof, right?) and note that the local context at that point
+is in something like the following mess:
+
+```
+P Q R S T U : Prop,
+p : P,
+h : P → Q,
+i : Q → R,
+j : Q → T,
+k : S → T,
+l : T → U,
+q : Q,
+t : T,
+u : U
+⊢ U
+```
 
+It was already bad enough to start with, and we added three more
+terms to it. In level 4 we will learn about the `apply` tactic
+which solves the level using another technique, without leaving
+so much junk behind.
 "

server/nng/NNG/Levels/Proposition/Level_4.lean

@@ -4,17 +4,40 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 4
-Title ""
+Title "apply"
 
 open MyNat
 
 Introduction
 "
+Let's do the same level again:
 
+![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg)
+
+We are given a proof $p$ of $P$ and our goal is to find a proof of $U$, or
+in other words to find a path through the maze that links $P$ to $U$.
+In level 3 we solved this by using `have`s to move forward, from $P$
+to $Q$ to $T$ to $U$. Using the `apply` tactic we can instead construct
+the path backwards, moving from $U$ to $T$ to $Q$ to $P$.
+
+Our goal is to prove $U$. But $l:T\\implies U$ is
+an implication which we are assuming, so it would suffice to prove $T$.
+Tell Lean this by starting the proof below with
+
+`apply l,`
+
+and notice that our assumptions don't change but *the goal changes*
+from `⊢ U` to `⊢ T`. 
+
+Keep `apply`ing implications until your goal is `P`, and try not
+to get lost! Now solve this goal
+with `exact p`. Note: you will need to learn the difference between
+`exact p` (which works) and `exact P` (which doesn't, because $P$ is
+not a proof of $P$).
 "
 
 Statement
-""
+"We can solve a maze."
     (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R)
     (j : Q → T) (k : S → T) (l : T → U) : U := by
   apply l

server/nng/NNG/Levels/Proposition/Level_5.lean

@@ -4,17 +4,53 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 5
-Title ""
+Title "P → (Q → P)"
 
 open MyNat
 
 Introduction
 "
+In this level, our goal is to construct an implication, like in level 2.
 
+```
+⊢ P → (Q → P)
+```
+
+So $P$ and $Q$ are propositions, and our goal is to prove
+that $P\\implies(Q\\implies P)$.
+We don't know whether $P$, $Q$ are true or false, so initially
+this seems like a bit of a tall order. But let's give it a go. Delete
+the `sorry` and let's think about how to proceed.
+
+Our goal is `P → X` for some true/false statement $X$, and if our
+goal is to construct an implication then we almost always want to use the
+`intro` tactic from level 2, Lean's version of \"assume $P$\", or more precisely
+\"assume $p$ is a proof of $P$\". So let's start with
+
+`intro p,`
+
+and we then find ourselves in this state:
+
+```
+P Q : Prop,
+p : P
+⊢ Q → P
+```
+
+We now have a proof $p$ of $P$ and we are supposed to be constructing
+a proof of $Q\\implies P$. So let's assume that $Q$ is true and try
+and prove that $P$ is true. We assume $Q$ like this:
+
+`intro q,`
+
+and now we have to prove $P$, but have a proof handy:
+
+`exact p,`
 "
 
 Statement
-""
+"For any propositions $P$ and $Q$, we always have
+$P\\implies(Q\\implies P)$."
     (P Q : Prop) : P → (Q → P) := by
   intro p
   intro q
@@ -22,5 +58,23 @@ Statement
 
 Conclusion
 "
+A mathematician would treat the proposition $P\\implies(Q\\implies P)$
+as the same as the proposition $P\\land Q\\implies P$,
+because to give a proof of either of these is just to give a method which takes
+a proof of $P$ and a proof of $Q$, and returns a proof of $P$. Thinking of the
+goal as $P\\land Q\\implies P$ we see why it is provable.
+
+## Did you notice?
+
+I wrote `P → (Q → P)` but Lean just writes `P → Q → P`. This is because
+computer scientists adopt the convention that `→` is *right associative*,
+which is a fancy way of saying \"when we write `P → Q → R`, we mean `P → (Q → R)`.
+Mathematicians would never dream of writing something as ambiguous as
+$P\\implies Q\\implies R$ (they are not really interested in proving abstract
+propositions, they would rather work with concrete ones such as Fermat's Last Theorem),
+so they do not have a convention for where the brackets go. It's important to
+remember Lean's convention though, or else you will get confused. If your goal
+is `P → Q → R` then you need to know whether `intro h` will create `h : P` or `h : P → Q`. 
+Make sure you understand which one. 
 
 "

server/nng/NNG/Levels/Proposition/Level_6.lean

@@ -4,12 +4,29 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 6
-Title ""
+Title "(P → (Q → R)) → ((P → Q) → (P → R))"
 
 open MyNat
 
 Introduction
 "
+You can solve this level completely just using `intro`, `apply` and `exact`,
+but if you want to argue forwards instead of backwards then don't forget
+that you can do things like `have j : Q → R := f p` if `f : P → (Q → R)`
+and `p : P`. I recommend that you start with `intro f` rather than `intro p`
+because even though the goal starts `P → ...`, the brackets mean that
+the goal is not the statement that `P` implies anything, it's the statement that
+$P\\implies (Q\\implies R)$ implies something. In fact I'd recommend that you started
+with `intros f h p`, which introduces three variables at once.
+You then find that your your goal is `⊢ R`. If you try `have j : Q → R := f p`
+now then you can `apply j`. Alternatively you can `apply (f p)` directly.
+What happens if you just try `apply f`? Can you figure out what just happened? This is a little
+`apply` easter egg. Why is it mathematically valid?
+-/
+
+/- Lemma : no-side-bar
+If $P$ and $Q$ and $R$ are true/false statements, then
+$$(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).$$
 
 "
 

server/nng/NNG/Levels/Proposition/Level_7.lean

@@ -4,17 +4,26 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Proposition"
 Level 7
-Title ""
+Title "(P → Q) → ((Q → R) → (P → R))"
 
 open MyNat
 
 Introduction
 "
-
+If you start with `intro hpq` and then `intro hqr`
+the dust will clear a bit and the level will look like this:
+```
+P Q R : Prop,
+hpq : P → Q,
+hqr : Q → R
+⊢ P → R
+```
+So this level is really about showing transitivity of $\\implies$,
+if you like that sort of language.
 "
 
 Statement
-""
+"From $P\\implies Q$ and $Q\\implies R$ we can deduce $P\\implies R$."
     (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) := by
   intro hpq hqr
   intro p

server/nng/NNG/Levels/Proposition/Level_8.lean

@@ -6,17 +6,32 @@ import NNG.MyNat.Theorems.Proposition
 Game "NNG"
 World "Proposition"
 Level 8
-Title ""
+Title "(P → Q) → (¬ Q → ¬ P)"
 
 open MyNat
 
 Introduction
 "
+There is a false proposition `false`, with no proof. It is
+easy to check that $\\lnot Q$ is equivalent to $Q\\implies {\tt false}$,
+and in the natural number game we call this
 
+`not_iff_imp_false (P : Prop) : ¬ P ↔ (P → false)`
+
+So you can start the proof of the contrapositive below with
+
+`repeat {rw not_iff_imp_false},`
+
+to get rid of the two occurences of `¬`, and I'm sure you can
+take it from there (note that we just added `not_iff_imp_false` to the
+theorem statements in the menu on the left). At some point your goal might be to prove `false`.
+At that point I guess you must be proving something by contradiction.
+Or are you? 
 "
 
 Statement
-""
+"If $P$ and $Q$ are propositions, and $P\\implies Q$, then
+$\\lnot Q\\implies \\lnot P$. "
     (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) := by
   rw [not_iff_imp_false]
   rw [not_iff_imp_false]

server/nng/NNG/Levels/Proposition/Level_9.lean

@@ -5,17 +5,25 @@ import NNG.MyNat.Theorems.Proposition
 Game "NNG"
 World "Proposition"
 Level 9
-Title ""
+Title "a big maze."
 
 open MyNat
 
 Introduction
 "
-
+Now move onto advanced proposition world, where you will see
+how to prove goals such as `P ∧ Q` ($P$ and $Q$), `P ∨ Q` ($P$ or $Q$),
+`P ↔ Q` ($P\\iff Q$).
+You will need to learn five more tactics: `split`, `cases`,
+`left`, `right`, and `exfalso`,
+but they are all straightforward, and furthermore they are
+essentially the last tactics you
+need to learn in order to complete all the levels of the Natural Number Game,
+including all the 17 levels of Inequality World. 
 "
 
 Statement
-""
+"There is a way through the following maze."
     (A B C D E F G H I J K L : Prop)
     (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
     (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)

server/nng/NNG/Modifications/Tactics.lean

@@ -51,7 +51,7 @@ namespace Lean.Parser.Tactic
 open Meta Elab Elab.Tactic
 
 open private getAltNumFields in evalCases ElimApp.evalAlts.go in
-def ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax)
+def ElimApp.evalNames.MyNat (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax)
     (numEqs := 0) (numGeneralized := 0) (toClear : Array FVarId := #[]) :
     TermElabM (Array MVarId) := do
   let mut names : List Syntax := withArg[1].getArgs |>.toList
@@ -96,7 +96,7 @@ elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+)
       let elimArgs := result.elimApp.getAppArgs
       ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds
       g.assign result.elimApp
-      let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
+      let subgoals ← ElimApp.evalNames.MyNat elimInfo result.alts withArg
         (numGeneralized := fvarIds.size) (toClear := targetFVarIds)
       setGoals <| (subgoals ++ result.others).toList ++ gs
 

server/nng/NNG/MyNat/AdvAddition.lean

@@ -0,0 +1,13 @@
+import NNG.MyNat.Theorems.Addition
+
+namespace MyNat
+open MyNat
+
+axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
+
+axiom zero_ne_succ (a : ℕ) : zero ≠ succ a
+
+axiom add_right_cancel (a t b : ℕ) : a + t = b + t → a = b
+
+axiom add_left_cancel (a b c : ℕ) : a + b = a + c → b = c
+

server/nng/NNG/MyNat/LE.lean

@@ -0,0 +1,18 @@
+import NNG.MyNat.Multiplication
+
+namespace MyNat
+
+def le (a b : ℕ) :=  ∃ (c : ℕ), b = a + c
+
+-- Another choice is to define it recursively: 
+-- | le 0 _
+-- | le (succ a) (succ b) = le ab 
+
+-- notation
+instance : LE MyNat := ⟨MyNat.le⟩
+
+--@[leakage] theorem le_def' : MyNat.le = (≤) := rfl
+
+theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c := Iff.rfl
+
+end MyNat

server/nng/NNG/MyNat/Multiplication.lean

@@ -15,3 +15,5 @@ axiom mul_zero (a : MyNat) : a * 0 = 0
 
 axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a
 
+-- ToDO
+axiom succ_ne_zero (a : ℕ) : succ a ≠ 0