NNG progress

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,9 +57,8 @@ If you delete it, your progress will be lost!
 
 "
 
-Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition
+Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition → AdvMultiplication
-Path AdvAddition → AdvMultiplication -- → Inequality
+Path Addition → Multiplication → AdvMultiplication -- → Inequality
-Path Addition → Multiplication → AdvMultiplication
+Path Multiplication → Power
--- Path Multiplication → Power
 
 MakeGame

server/nng/NNG/Doc/Definitions.lean

@@ -15,6 +15,8 @@ The natural numbers implemented in Lean's core are called `Nat`.
 
 If you end up getting someting of type `Nat` in this game, you probably
 need to write `(4 : ℕ)` to force it to be of type `MyNat`.
+
+*Write with `\\N`.*
 "
 
 DefinitionDoc Add as "+" "
@@ -23,5 +25,64 @@ Addition on `ℕ` is defined through two axioms:
 * `add_zero (a : ℕ) : a + 0 = a`
 * `add_succ (a d : ℕ) : a + succ d = succ (a + d)`
 "
-  
+
-DefinitionDoc Mul as "*" ""
+DefinitionDoc Pow as "^" "
+Power on `ℕ` is defined through two axioms:
+
+* `pow_zero (a : ℕ) : a ^ 0 = 1`
+* `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`
+
+## Game-specific notes
+
+Note that you might need to manually specify the type of the first number:
+
+```
+(2 : ℕ) ^ 1
+```
+
+If you write `2 ^ 1` then lean will try to work in it's inbuild `Nat`, not in
+the game's natural numbers `MyNat`.
+"
+
+DefinitionDoc One as "1" "
+`1 : ℕ` is by definition `succ 0`. Use `one_eq_succ_zero`
+to change between the two.
+"
+
+DefinitionDoc False as "False" "
+`False` is a proposition that that is always false, in contrast to `True` which is always true.
+
+A proof of `False`, i.e. `(h : False)` is used to implement a contradiction: From a proof of `False`
+anything follows, *ad absurdum*.
+
+For example, \"not\" (`¬ A`) is therefore implemented as `A → False`.
+(\"If `A` is true then we have a contradiction.\")
+"
+
+DefinitionDoc Not as "¬" "
+Logical \"not\" is implemented as `¬ A := A → False`.
+
+*Write with `\\n`.*
+"
+
+DefinitionDoc And as "∧" "
+(missing)
+
+*Write with `\\and`.*
+"
+
+DefinitionDoc Or as "∨" "
+(missing)
+
+*Write with `\\or`.*
+"
+
+DefinitionDoc Iff as "↔" "
+(missing)
+
+*Write with `\\iff`.*
+"
+
+DefinitionDoc Mul as "*" ""
+
+DefinitionDoc Ne as "≠" ""

server/nng/NNG/Doc/Lemmas.lean

@@ -1,31 +1,37 @@
 import GameServer.Commands
 
-LemmaDoc MyNat.add_zero as "add_zero" in "Nat"
+LemmaDoc MyNat.add_zero as "add_zero" in "Add"
 "`add_zero (a : ℕ) : a + 0 = a`
 
 This is one of the two axioms defining addition on `ℕ`."
 
-LemmaDoc MyNat.add_succ as "add_succ" in "Nat"
+LemmaDoc MyNat.add_succ as "add_succ" in "Add"
 "`add_succ (a d : ℕ) : a + (succ d) = succ (a + d)`
 
 This is the second axiom definiting addition on `ℕ`"
 
-LemmaDoc MyNat.zero_add as "zero_add" in "Nat"
+LemmaDoc MyNat.zero_add as "zero_add" in "Add"
 "(missing)"
 
-LemmaDoc MyNat.add_assoc as "add_assoc" in "Nat"
+LemmaDoc MyNat.add_assoc as "add_assoc" in "Add"
 "(missing)"
 
-LemmaDoc MyNat.succ_add as "succ_add" in "Nat"
+LemmaDoc MyNat.succ_add as "succ_add" in "Add"
 "(missing)"
 
-LemmaDoc MyNat.add_comm as "add_comm" in "Nat"
+LemmaDoc MyNat.add_comm as "add_comm" in "Add"
 "(missing)"
 
 LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "Nat"
 "(missing)"
 
-LemmaDoc not_iff_imp_false as "not_iff_imp_false" in "Prop"
+LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_one_eq_succ as "add_one_eq_succ" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_right_comm as "add_right_comm" in "Add"
 "(missing)"
 
 LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat"
@@ -33,3 +39,130 @@ LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat"
 
 LemmaDoc MyNat.zero_ne_succ as "zero_ne_succ" in "Nat"
 "(missing)"
+
+
+/-? Multiplication World -/
+
+LemmaDoc MyNat.mul_zero as "mul_zero" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_succ as "mul_succ" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.zero_mul as "zero_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_one as "mul_one" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.one_mul as "one_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_add as "mul_add" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_assoc as "mul_assoc" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.succ_mul as "succ_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.add_mul as "add_mul" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_comm as "mul_comm" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_left_comm as "mul_left_comm" in "Mul"
+"(missing)"
+
+
+
+LemmaDoc MyNat.succ_eq_succ_of_eq as "succ_eq_succ_of_eq" in "Nat"
+"(missing)"
+
+LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "Add"
+"(missing)"
+
+LemmaDoc Ne.symm as "Ne.symm" in "Nat"
+"(missing)"
+
+LemmaDoc Eq.symm as "Eq.symm" in "Nat"
+"(missing)"
+
+LemmaDoc Iff.symm as "Iff.symm" in "Nat"
+"(missing)"
+
+LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Add"
+"(missing)"
+  
+LemmaDoc MyNat.add_right_cancel_iff as "add_right_cancel_iff" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.eq_zero_of_add_right_eq_self as "eq_zero_of_add_right_eq_self" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_left_eq_zero as "add_left_eq_zero" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.add_right_eq_zero as "add_right_eq_zero" in "Add"
+"(missing)"
+
+LemmaDoc MyNat.eq_zero_or_eq_zero_of_mul_eq_zero as "eq_zero_or_eq_zero_of_mul_eq_zero" in "Mul"
+"(missing)"
+
+LemmaDoc MyNat.mul_left_cancel as "mul_left_cancel" in "Mul"
+"(missing)"
+
+
+LemmaDoc MyNat.zero_pow_zero as "zero_pow_zero" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_zero as "pow_zero" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_succ as "pow_succ" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.zero_pow_succ as "zero_pow_succ" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_one as "pow_one" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.one_pow as "one_pow" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_add as "pow_add" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.mul_pow as "mul_pow" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.pow_pow as "pow_pow" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.two_eq_succ_one as "two_eq_succ_one" in "Pow"
+"(missing)"
+
+LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
+"(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+
+-- LemmaDoc MyNat. as "" in "Pow"
+-- "(missing)"
+

server/nng/NNG/Doc/Tactics.lean

@@ -153,14 +153,34 @@ TacticDoc left
 "
 "
 
+TacticDoc revert
+"
+"
+
+TacticDoc tauto
+"
+"
+
 TacticDoc right
 "
 "
 
+TacticDoc by_cases
+"
+"
+
 TacticDoc contradiction
 "
 "
 
 TacticDoc exfalso
 "
+"
+
+TacticDoc simp
+"
+"
+
+TacticDoc «repeat»
+"
 "

server/nng/NNG/Levels/Addition.lean

@@ -1,47 +1,36 @@
-import NNG.Levels.Addition.Level_1
-import NNG.Levels.Addition.Level_2
-import NNG.Levels.Addition.Level_3
-import NNG.Levels.Addition.Level_4
-import NNG.Levels.Addition.Level_5
 import NNG.Levels.Addition.Level_6
 
-
 Game "NNG"
 World "Addition"
 Title "Addition World"
 
 Introduction
 "
-Hi!
+Welcome to Addition World. If you've done all four levels in tutorial world
-"
+and know about `rw` and `rfl`, then you're in the right place. Here's
-
+a reminder of the things you're now equipped with which we'll need in this world.
--- Introduction
--- "
--- Welcome to Addition World. If you've done all four levels in tutorial world
--- and know about `rewrite` and `rfl`, then you're in the right place. Here's
--- a reminder of the things you're now equipped with which we'll need in this world.
 
--- ## Data:
+## Data:
 
---   * a type called `ℕ` or `MyNat`.
+  * a type called `ℕ` or `MyNat`.
---   * a term `0 : ℕ`, interpreted as the number zero.
+  * a term `0 : ℕ`, interpreted as the number zero.
---   * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\".
+  * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\".
---   * Usual numerical notation `0,1,2` etc. (although `2` onwards will be of no use to us until much later ;-) ).
+  * Usual numerical notation `0,1,2` etc. (although `2` onwards will be of no use to us until much later ;-) ).
---   * Addition (with notation `a + b`).
+  * Addition (with notation `a + b`).
 
--- ## Theorems:
+## Theorems:
 
---   * `add_zero (a : ℕ) : a + 0 = a`. Use with `rewrite [add_zero]`.
+  * `add_zero (a : ℕ) : a + 0 = a`. Use with `rw [add_zero]`.
---   * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rewrite [add_succ]`.
+  * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rw [add_succ]`.
---   * The principle of mathematical induction. Use with `induction` (which we learn about in this chapter).
+  * The principle of mathematical induction. Use with `induction` (which we learn about in this chapter).
 
 
--- ## Tactics:
+## Tactics:
 
---   * `rfl` :  proves goals of the form `X = X`.
+  * `rfl` :  proves goals of the form `X = X`.
---   * `rewrite [h]` : if `h` is a proof of `A = B`, changes all `A`'s in the goal to `B`'s.
+  * `rw [h]` : if `h` is a proof of `A = B`, changes all `A`'s in the goal to `B`'s.
---   * `induction n with d hd` : we're going to learn this right now.
+  * `induction n with d hd` : we're going to learn this right now.
 
 
--- You will also find all this information in your Inventory to read the documentation.
+You will also find all this information in your Inventory to read the documentation.
--- "
+"

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

@@ -8,8 +8,6 @@ Title "the induction tactic."
 
 open MyNat
 
-set_option tactic.hygienic false
-
 Introduction
 "
 OK so let's see induction in action. We're going to prove
@@ -36,7 +34,7 @@ note that `zero_add` is about zero add something, and `add_zero` is about someth
 The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`.
 "
 
-Statement MyNat.zero_add
+Statement MyNat.zero_add (attr := simp)
 "For all natural numbers $n$, we have $0 + n = n$."
     (n : ℕ) : 0 + n = n := by
   Hint "You can start a proof by induction over `n` by typing:
@@ -56,20 +54,25 @@ Statement MyNat.zero_add
     `{hn} : 0 + {n} = {n}` and you need to prove the statement for `succ {n}`."
     Hint (hidden := true) "look at `add_succ`."
     rw [add_succ]
+    Branch
+      simp? -- TODO
     Hint (hidden := true) "At this point you see the term `0 + {n}`, so you can use the
     induction hypothesis with `rw [{hn}]`."
     rw [hn]
     rfl
 
+attribute [simp] MyNat.zero_add
+
 NewTactic induction
+LemmaTab "Add"
 
 Conclusion
 "
 ## Now venture off on your own.
 
-Those three tactics: 
+Those three tactics:
 
-* `induction n with d hd` 
+* `induction n with d hd`
 * `rw [h]`
 * `rfl`
 
@@ -86,8 +89,7 @@ We're going to stop explaining stuff carefully now. If you get stuck or want
 to know more about Lean (e.g. how to do much harder maths in Lean),
 ask in `#new members` at
 [the Lean chat](https://leanprover.zulipchat.com)
-(login required, real name preferred). Kevin or Mohammad or one of the other
+(login required, real name preferred). Any of the people there might be able to help.
-people there might be able to help.
 
 Good luck! Click on \"Next\" to solve some levels on your own.
 "

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

@@ -1,4 +1,3 @@
-import NNG.Metadata
 import NNG.Levels.Addition.Level_1
 
 Game "NNG"
@@ -25,7 +24,7 @@ Statement MyNat.add_assoc
 "On the set of natural numbers, addition is associative.
 In other words, for all natural numbers $a, b$ and $c$, we have
 $ (a + b) + c = a + (b + c). $"
-    (a b c : ℕ) : (a + b) + c = a + (b + c)  := by
+    (a b c : ℕ) : (a + b) + c = a + (b + c) := by
   Hint "Because addition was defined by recursion on the right-most variable,
   use induction on the right-most variable (try other variables at your peril!).
 
@@ -34,8 +33,9 @@ $ (a + b) + c = a + (b + c). $"
   Branch
     induction a
     Hint "Good luck with that…"
-    rw [zero_add, zero_add]
+    simp?
-    rfl
+    --rw [zero_add, zero_add]
+    --rfl
   Branch
     induction b
     Hint "Good luck with that…"
@@ -54,10 +54,5 @@ $ (a + b) + c = a + (b + c). $"
   rw [hc]
   rfl
 
-
+NewLemma MyNat.zero_add
-Conclusion
+LemmaTab "Add"
-"
-
-"
-
-NewLemma MyNat.zero_add

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

@@ -1,4 +1,3 @@
-import NNG.Metadata
 import NNG.Levels.Addition.Level_2
 
 Game "NNG"
@@ -46,6 +45,8 @@ $ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$."
     rw [add_succ]
     rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 

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

@@ -1,4 +1,3 @@
-import NNG.Metadata
 import NNG.Levels.Addition.Level_3
 
 Game "NNG"
@@ -21,6 +20,7 @@ Statement MyNat.add_comm
 In other words, for all natural numbers $a$ and $b$, we have
 $a + b = b + a$."
     (a b : ℕ) : a + b = b + a := by
+  Hint (hidden := true) "You might want to start by induction."
   Branch
     induction a with d hd
     · rw [zero_add]
@@ -39,6 +39,8 @@ $a + b = b + a$."
     rw [succ_add]
     rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 If you got this far -- nice! You're nearly ready to make a choice:

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

@@ -1,5 +1,3 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
 import NNG.Levels.Addition.Level_4
 
 Game "NNG"
@@ -9,13 +7,11 @@ Title "succ_eq_add_one"
 
 open MyNat
 
-theorem one_eq_succ_zero : (1 : ℕ) = succ 0 := by simp only
+axiom MyNat.one_eq_succ_zero : (1 : ℕ) = succ 0
-
-NewLemma MyNat.one_eq_succ_zero
 
 Introduction
 "
-I've just added `one_eq_succ_zero` (a proof of $1 = \\operatorname{succ}(0)$)
+I've just added `one_eq_succ_zero` (a proof of `1 = succc 0`)
 to your list of theorems; this is true
 by definition of $1$, but we didn't need it until now.
 
@@ -28,7 +24,7 @@ some theorems about $0$ (`zero_add`, `add_zero`), but, other than `1 = succ 0`,
 no theorems at all which mention $1$. Let's prove one now.
 "
 
-Statement --MyNat.succ_eq_add_one
+Statement MyNat.succ_eq_add_one
 "For any natural number $n$, we have
 $ \\operatorname{succ}(n) = n+1$ ."
     (n : ℕ) : succ n = n + 1 := by
@@ -37,6 +33,10 @@ $ \\operatorname{succ}(n) = n+1$ ."
   rw [add_zero]
   rfl
 
+NewLemma MyNat.one_eq_succ_zero
+NewDefinition One
+LemmaTab "Add"
+
 Conclusion
 "
 Well done! On to the last level!

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

@@ -1,5 +1,3 @@
-import NNG.Metadata
-import NNG.MyNat.Addition
 import NNG.Levels.Addition.Level_5
 
 Game "NNG"
@@ -25,23 +23,92 @@ then the space bar (note that this is L for left, not a number 1).
 Similarly, if `h : a = b` then `rw [h]` will change `a`'s to `b`'s
 and `rw [← h]` will change `b`'s to `a`'s.
 
-Also, you can be (and will need to be, in this level) more precise
+
-about where to rewrite theorems. `rw add_comm,` will just find the
-first `? + ?` it sees and swap it around. You can target more specific
-additions like this: `rw add_comm a` will swap around
-additions of the form `a + ?`, and `rw add_comm a b,` will only
-swap additions of the form `a + b`.
 "
 
-Statement --add_right_comm
+Statement MyNat.add_right_comm
 "For all natural numbers $a, b$ and $c$, we have
 $a + b + c = a + c + b$."
     (a b c : ℕ) : a + b + c = a + c + b := by
+  Hint (hidden := true) "You want to change your goal to `a + (b + c) = _`
+  so that you can then use commutativity."
   rw [add_assoc]
+  Hint "Here you need to be more precise about where to rewrite theorems.
+  `rw [add_comm]` will just find the
+  first `_ + _` it sees and swap it around. You can target more specific
+  additions like this: `rw [add_comm a]` will swap around
+  additions of the form `a + _`, and `rw [add_comm a b]` will only
+  swap additions of the form `a + b`."
+  Branch
+    rw [add_comm]
+    Hint "`rw [add_comm]` just rewrites to first instance of `_ + _` it finds, which
+    is not what you want to do here. Instead you can provide the arguments explicitely:
+
+    * `rw [add_comm b c]`
+    * `rw [add_comm b]`
+    * `rw [add_comm b _]`
+    * `rw [add_comm _ c]`
+
+    would all have worked. You should go back and try again.
+    "
   rw [add_comm b c]
+  Branch
+    rw [add_assoc]
+    rfl
   rw [←add_assoc]
   rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
+If you have got this far, then you have become very good at
+manipulating equalities in Lean. You can also now collect
+four collectibles (or `instance`s, as Lean calls them)
+
+```
+MyNat.addSemigroup     -- (after level 2)
+MyNat.addMonoid        -- (after level 2)
+MyNat.addCommSemigroup -- (after level 4)
+MyNat.addCommMonoid    -- (after level 4)
+```
+
+These say that `ℕ` is a commutative semigroup/monoid.
+
+In Multiplication World you will be able to collect such
+advanced collectibles as `MyNat.commSemiring` and
+`MyNat.distrib`, and then move on to power world and
+the famous collectible at the end of it.
+
+One last thing -- didn't you think that solving this level
+`add_right_comm` was boring? Check out this AI that can do it for us.
+
+From now on, the `simp` AI becomes accessible (it's just an advanced
+tactic really), and can nail some really tedious-for-a-human-to-solve
+goals. For example check out this one-line proof:
+
+```
+example (a b c d e : ℕ ) :
+    (((a + b) + c) + d) + e = (c + ((b + e) + a)) + d := by
+  simp
+```
+
+Imagine having to do that one by hand! The AI closes the goal
+because it knows how to use associativity and commutativity
+sensibly in a commutative monoid.
+
+You are now done with addition world. Go back to the main menu (top left)
+and decide whether to press on with multiplication world and power world
+(which can be solved with `rw`, `refl` and `induction`), or to go on
+to Function World where you can learn the tactics needed to prove
+goals of the form $P\\implies Q$, thus enabling you to solve more
+advanced addition world levels such as $a+t=b+t\\implies a=b$. Note that
+Function World is more challenging mathematically; but if you can do Addition
+World you can surely do Multiplication World and Power World.
 "
+
+-- First we have to get the `AddCommMonoid` collectible,
+-- which we do by saying the magic words which make Lean's type class inference
+-- system give it to us.
+-- -/
+-- instance : add_comm_monoid mynat := by structure_helper

server/nng/NNG/Levels/AdvAddition.lean

@@ -1,23 +1,28 @@
-import NNG.Levels.AdvAddition.Level_1
-import NNG.Levels.AdvAddition.Level_2
-import NNG.Levels.AdvAddition.Level_3
-import NNG.Levels.AdvAddition.Level_4
-import NNG.Levels.AdvAddition.Level_5
-import NNG.Levels.AdvAddition.Level_6
-import NNG.Levels.AdvAddition.Level_7
-import NNG.Levels.AdvAddition.Level_8
-import NNG.Levels.AdvAddition.Level_9
-import NNG.Levels.AdvAddition.Level_10
-import NNG.Levels.AdvAddition.Level_11
-import NNG.Levels.AdvAddition.Level_12
 import NNG.Levels.AdvAddition.Level_13
 
-
 Game "NNG"
 World "AdvAddition"
 Title "Advanced Addition World"
 
 Introduction
 "
-  Hi
+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 : ℕ) :
+  succ a = succ b → a = b
+
+zero_ne_succ (a : ℕ) :
+  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 $\\operatorname{succ}(a)=\\operatorname{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.
 "

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

@@ -1,5 +1,6 @@
 import NNG.Metadata
 import NNG.MyNat.AdvAddition
+import NNG.Levels.Addition
 
 Game "NNG"
 World "AdvAddition"
@@ -10,44 +11,35 @@ open MyNat
 
 Introduction
 "
-Peano's original collection of axioms for the natural numbers contained two further
+Let's finally learn how to use `succ_inj`:
-assumptions, which have not yet been mentioned in the game:
 
 ```
-succ_inj {a b : mynat} :
+succ_inj (a b : ℕ) :
-  succ(a) = succ(b) → a = b
+  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`.
 "
 
 Statement -- MyNat.succ_inj'
-"For all naturals $a$ and $b$, if we assume $succ(a)=succ(b)$, then we can
+"For all naturals $a$ and $b$, if we assume $\\operatorname{succ}(a)=\\operatorname{succ}(b)$,
-deduce $a=b$."
+then we can deduce $a=b$."
     {a b : ℕ} (hs : succ a = succ b) :  a = b := by
-    exact succ_inj hs
+  Hint "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`."
+  Branch
+    apply succ_inj
+    exact hs
+  exact succ_inj hs
 
-NewLemma MyNat.succ_inj MyNat.zero_ne_succ
+NewLemma MyNat.succ_inj
+LemmaTab "Nat"
 
 Conclusion
 "
-## Important thing.
+**Important thing**:
 
-You can rewrite proofs of *equalities*. If `h : A = B` then `rw h` changes `A`s to `B`s.
+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*
+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,6 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_9
-import NNG.MyNat.AdvAddition
+import Std.Tactic.RCases
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "AdvAddition"
@@ -11,64 +10,66 @@ open MyNat
 
 Introduction
 "
-In Lean, `a ≠ b` is *defined to mean* `(a = b) → false`. 
+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
+it as saying* `(a = b) → False`. Computer scientists would
-say that these two terms are *definitionally equal*. 
+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 -- add_left_eq_zero
+Statement MyNat.add_left_eq_zero
-"If $a$ and $b$ are natural numbers such that 
+"If $a$ and $b$ are natural numbers such that
 $$ a + b = 0, $$
 then $b = 0$."
-    {{a b : ℕ}} (H : a + b = 0) : b = 0 := by
+    {a b : ℕ} (h : a + b = 0) : b = 0 := by
+  Hint "
+  You want to start of by making a distinction `b = 0` or `b = succ d` for some
+  `d`. You can do this with
+
+  ```
+  induction b
+  ```
+  even if you are never going to use the induction hypothesis.
+  "
+
+  -- TODO: induction vs rcases
+
+  Branch
+    rcases b
+    -- TODO: `⊢ zero = 0` :(
   induction b with d
-  rfl
+  · rfl
-  rw [add_succ] at H
+  · Hint "This goal seems impossible! However, our hypothesis `h` is also impossible,
-  exfalso
+    meaning that we still have a chance!
-  apply succ_ne_zero (a + d)
+    First let's see why `h` is impossible. We can
-  exact H
+
+    ```
+    rw [add_succ] at h
+    ```
+    "
+    rw [add_succ] at h
+    Hint "
+    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.
+    "
+    Branch
+      have j := succ_ne_zero (a + d) h
+      exfalso
+      exact j
+    exfalso
+    apply succ_ne_zero (a + d)
+    exact h
+
+LemmaTab "Add"
 
 Conclusion
 "

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

@@ -1,5 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_10
-import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
@@ -8,22 +7,22 @@ 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`.
+We just proved `add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0`.
 Hopefully `add_right_eq_zero` shouldn't be too hard now.
 "
 
-Statement
+Statement MyNat.add_right_eq_zero
-"If $a$ and $b$ are natural numbers such that 
+"If $a$ and $b$ are natural numbers such that
 $$ a + b = 0, $$
 then $a = 0$."
     {a b : ℕ} : a + b = 0 → a = 0 := by
-  intro H
+  intro h
-  rw [add_comm] at H
+  rw [add_comm] at h
-  exact add_left_eq_zero H
+  exact add_left_eq_zero h
+
+LemmaTab "Add"
 
 Conclusion
 "

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

@@ -1,5 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_11
-import NNG.MyNat.AdvAddition
+
 
 Game "NNG"
 World "AdvAddition"
@@ -12,20 +12,22 @@ Introduction
 "
 We have
 
-  * `succ_eq_add_one (n : mynat) : succ n = n + 1`
+```
+succ_eq_add_one (n : ℕ) : 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 MyNat.add_one_eq_succ
-
-Statement
 "For any natural number $d$, we have
 $$ d+1 = \\operatorname{succ}(d). $$"
     (d : ℕ) : d + 1 = succ d := by
   rw [succ_eq_add_one]
   rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 

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

@@ -1,5 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_12
-import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
@@ -11,24 +10,29 @@ open MyNat
 Introduction
 "
 The last level in Advanced Addition World is the statement
-that $n\\not=\\operatorname{succ}(n)$. When you've done this
+that $n\\not=\\operatorname{succ}(n)$.
-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 --ne_succ_self
 "For any natural number $n$, we have
 $$ n \\neq \\operatorname{succ}(n). $$"
      (n : ℕ) : n ≠ succ n := by
+  Hint (hidden := true) "I would start a proof by induction on `n`."
   induction n with d hd
-  apply zero_ne_succ
+  · apply zero_ne_succ
-  intro hs
+  · Hint (hidden := true) "If you have no clue, you could start with `rw [Ne, Not]`."
-  apply hd
+    Branch
-  apply succ_inj
+      rw [Ne, Not]
-  assumption
+    intro hs
+    apply hd
+    apply succ_inj
+    exact hs
+
+LemmaTab "Nat"
 
 Conclusion
 "
-
+Congratulations. 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).
 "

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

@@ -1,5 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_1
-import NNG.MyNat.AdvAddition
+
 
 Game "NNG"
 World "AdvAddition"
@@ -11,43 +11,46 @@ 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
+$\\operatorname{succ}(\\operatorname{succ}(a))=\\operatorname{succ}(\\operatorname{succ}(b))
-to prove $succ(a)=succ(b)\\implies a=b$. However `succ(a)=succ(b)` is
+\\implies \\operatorname{succ}(a)=\\operatorname{succ}(b)$, and then again
+to prove $\\operatorname{succ}(a)=\\operatorname{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
+"For all naturals $a$ and $b$, if we assume
-deduce $a=b$. "
+$\\operatorname{succ}(\\operatorname{succ}(a))=\\operatorname{succ}(\\operatorname{succ}(b))$,
-    {a b : ℕ} (h : succ (succ a) = succ ( succ b )) : a = b := by
+then we can deduce $a=b$. "
+    {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
+  Branch
+    exact succ_inj (succ_inj h)
   apply succ_inj
   apply succ_inj
   assumption
 
+LemmaTab "Nat"
+
 Conclusion
 "
-## Sample solutions to this level. 
+## 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
+example {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
-  apply succ_inj,
+  apply succ_inj
-  apply succ_inj,
+  apply succ_inj
   exact h
-end 
+
-
+example {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
-example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
+  apply succ_inj
-begin
+  exact succ_inj h
-  apply succ_inj,
+
-  exact succ_inj(h),
+example {a b : ℕ} (h : succ (succ a) = succ (succ b)) : a = b := by
-end 
+  exact succ_inj (succ_inj h)
-
+```
-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,5 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_2
-import NNG.MyNat.AdvAddition
+
 
 Game "NNG"
 World "AdvAddition"
@@ -11,20 +11,18 @@ open MyNat
 Introduction
 "
 We are going to prove something completely obvious: if $a=b$ then
-$succ(a)=succ(b)$. This is *not* `succ_inj`!
+$\\operatorname{succ}(a)=\\operatorname{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
+Statement MyNat.succ_eq_succ_of_eq
-"For all naturals $a$ and $b$, $a=b\\implies succ(a)=succ(b)$. 
+"For all naturals $a$ and $b$, $a=b\\implies \\operatorname{succ}(a)=\\operatorname{succ}(b)$."
-"
     {a b : ℕ} : a = b → succ a = succ b := by
+  Hint "This is trivial -- we can just rewrite our proof of `a=b`.
+  But how do we get to that proof? Use the `intro` tactic."
   intro h
+  Hint "Now we can indeed just `rw` `a` to `b`."
   rw [h]
+  Hint (hidden := true) "Recall that `rfl` closes these goals."
   rfl
 
-Conclusion
+LemmaTab "Nat"
-"
-
-"

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

@@ -1,5 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_3
-import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
@@ -11,19 +10,7 @@ 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.
+directions) using the `constructor` 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
@@ -31,10 +18,25 @@ Statement
 "
     (a b : ℕ) : succ a = succ b ↔ a = b := by
   constructor
+  Hint "Now you have two goals. The first is exactly `succ_inj` so you can close
+  it with
+
+  ```
   exact succ_inj
-  intro H
+  ```
-  rw [H]
+  "
-  rfl
+  · exact succ_inj
+  · Hint "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 `rfl`."
+    Branch
+      exact succ_eq_succ_of_eq
+    intro h
+    rw [h]
+    rfl
+
+LemmaTab "Nat"
 
 Conclusion
 "

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

@@ -1,5 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_4
-import NNG.MyNat.AdvAddition
+
 
 Game "NNG"
 World "AdvAddition"
@@ -11,18 +11,19 @@ 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`
+when you're doing addition -- if `a + t = b + t` then `a = b`. 
-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
+Statement MyNat.add_right_cancel
 "On the set of natural numbers, addition has the right cancellation property.
 In other words, if there are natural numbers $a, b$ and $c$ such that
 $$ a + t = b + t, $$
 then we have $a = b$."
     (a t b : ℕ) : a + t = b + t → a = b := by
+  Hint (hidden := true) "You should start with `intro`."
   intro h
+  Hint "I'd recommend now induction on `t`. Don't forget that `rw [add_zero] at h` can be used
+  to do rewriting of hypotheses rather than the goal."
   induction t with d hd
   rw [add_zero] at h
   rw [add_zero] at h
@@ -30,8 +31,13 @@ then we have $a = b$."
   apply hd
   rw [add_succ] at h
   rw [add_succ] at h
+  Hint (hidden := true) "At this point `succ_inj` might be useful."
   exact succ_inj h
 
+-- TODO: Display at this level after induction is confusing: old assumption floating in context
+
+LemmaTab "Add"
+
 Conclusion
 "
 

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

@@ -1,5 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_5
-import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
@@ -11,23 +10,27 @@ 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`. 
+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
+Statement MyNat.add_left_cancel
 "On the set of natural numbers, addition has the left cancellation property.
 In other words, if there are natural numbers $a, b$ and $t$ such that
 $$ t + a = t + b, $$
 then we have $a = b$."
     (t a b : ℕ) : t + a = t + b → a = b := by
+  Hint "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."
   rw [add_comm]
   rw [add_comm t]
+  Hint "Now that looks like `add_right_cancel`!"
+  Hint (hidden := true) "`exact add_right_cancel` does not work. You need
+  `exact add_right_cancel a t b` or `exact add_right_cancel _ _ _`."
   exact add_right_cancel a t b
 
+LemmaTab "Add"
+
 Conclusion
 "
 

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

@@ -1,5 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_6
-import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
@@ -11,25 +10,21 @@ 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`
+of theorems like `add_right_cancel`. Remember that you can use `constructor`
 to split an `↔` goal into the `→` goal and the `←` goal.
-
-## Pro tip:
-
-`exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\"
 "
 
-Statement --add_right_cancel_iff 
+Statement MyNat.add_right_cancel_iff
-"For all naturals $a$, $b$ and $t$, 
+"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,
+  · Hint "Pro tip: `exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\"."
-  intro H -- H : a = b,
+    exact add_right_cancel _ _ _
-  rw [H]
+  · intro H
-  rfl
+    rw [H]
-Conclusion
+    rfl
-"
+
+LemmaTab "Add"
 
-"

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

@@ -1,5 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_7
-import NNG.MyNat.AdvAddition
+
 
 Game "NNG"
 World "AdvAddition"
@@ -14,17 +14,20 @@ The lemma you're about to prove will be useful when we want to prove that $\\leq
 There are some wrong paths that you can take with this one.
 "
 
-Statement --eq_zero_of_add_right_eq_self
+Statement MyNat.eq_zero_of_add_right_eq_self
-"If $a$ and $b$ are natural numbers such that 
+"If $a$ and $b$ are natural numbers such that
 $$ a + b = a, $$
 then $b = 0$."
     {a b : ℕ} : a + b = a → b = 0 := by
   intro h
+  Hint (hidden := true) "Look at `add_left_cancel`."
   apply add_left_cancel a
   rw [h]
   rw [add_zero]
   rfl
 
+LemmaTab "Add"
+
 Conclusion
 "
 

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

@@ -1,5 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvAddition.Level_8
-import NNG.MyNat.AdvAddition
 
 Game "NNG"
 World "AdvAddition"
@@ -11,23 +10,43 @@ 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`. 
+that $0\\not=\\operatorname{succ}(a)$. The proof of this is called `zero_ne_succ a`.
 
-`zero_ne_succ (a : mynat) : 0 ≠ succ(a)`
+```
+zero_ne_succ (a : ¬) : 0 ≠ succ a
+```
 
-The `symmetry` tactic will turn any goal of the form `R x y` into `R y x`,
+$X\\ne Y$ is *defined to mean* $X = Y\\implies{\\tt False}$, similar to how `¬A` was defined.
-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`. 
 "
+-- TODO: I dont think there is a `symmetry` tactic anymore.
+-- 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 -- succ_ne_zero
+Statement MyNat.succ_ne_zero
 "Zero is not the successor of any natural number."
     (a : ℕ) : succ a ≠ 0 := by
+  Hint "You have several options how to start. One would be to recall that `≠` is defined as
+  `(· = ·) → False` and start with `intro`. Or do `rw [Ne, Not]` to explicitely remove the
+  `≠`. Or you could use the lemma `Ne.symm (a b : ℕ) : a ≠ b → b ≠ a` which I just added to your
+  inventory."
+  Branch
+    rw [Ne, Not]
+    intro h
+    apply zero_ne_succ a
+    rw [h]
+    rfl
+  Branch
+    exact (zero_ne_succ a).symm
   apply Ne.symm
   exact zero_ne_succ a
 
 
+NewLemma MyNat.zero_ne_succ Ne.symm Eq.symm Iff.symm
+NewDefinition Ne
+LemmaTab "Nat"
+
 Conclusion
 "
 

server/nng/NNG/Levels/AdvMultiplication.lean

@@ -10,4 +10,8 @@ Title "Advanced Multiplication World"
 
 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.
 "

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

@@ -1,7 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication
-import NNG.MyNat.Multiplication
+import NNG.Levels.AdvAddition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
@@ -12,28 +10,24 @@ 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
+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`.
+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
+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`,
+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`.
 
 "
+-- TODO: cases
+-- Recall that if `b : ℕ` 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).
+
 
 Statement
 "The product of two non-zero natural numbers is non-zero."

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

@@ -1,7 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvMultiplication.Level_1
-import NNG.MyNat.Multiplication
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
@@ -15,14 +12,14 @@ Introduction
 A variant on the previous level.
 "
 
-Statement -- eq_zero_or_eq_zero_of_mul_eq_zero
+Statement MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
 "If $ab = 0$, then at least one of $a$ or $b$ is equal to zero."
     (a b : ℕ) (h : a * b = 0) :
   a = 0 ∨ b = 0 := by
   induction a with d
   left
   rfl
-  induction b with e he
+  induction b with e
   right
   rfl
   exfalso

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

@@ -1,7 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.AdvMultiplication.Level_2
-import NNG.MyNat.Multiplication
+
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
@@ -15,13 +13,10 @@ 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.
 "
-    (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 := by
+    {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

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

@@ -1,7 +1,4 @@
-import NNG.Metadata
+import NNG.Levels.AdvMultiplication.Level_3
-import NNG.MyNat.Multiplication
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvMultiplication"
@@ -19,14 +16,17 @@ 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,
+it might be instructive if you stop reading after the end of this paragraph
-seeing the trouble you run into, and reading the rest of these comments afterwards. This level
+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,
+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
@@ -36,30 +36,64 @@ $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$\"
+Imagine $a\\ne 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. 
+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`
+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
+[TODO: The second way does not work yet in this game]
-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!)
 "
+-- Alternatively, you can write `induction c with d hd
+-- generalizing b` as the first line of the proof.
 
-Statement
+
+Statement MyNat.mul_left_cancel
 "If $a \\neq 0$, $b$ and $c$ are natural numbers such that
 $ ab = ac, $
 then $b = c$."
     (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c := by
-  sorry
+  Hint "NOTE: As is, this level is probably too hard and contains no hints yet.
+  Good luck!
+
+  Your first step should be `revert b`!"
+  revert b
+  induction c with c hc
+  · intro b hb
+    rw [mul_zero] at hb
+    rcases eq_zero_or_eq_zero_of_mul_eq_zero _ _ hb
+    exfalso
+    apply ha
+    exact h
+    exact h
+  · intro b h
+    induction b with b hb
+    exfalso
+    apply ha
+    rw [mul_zero] at h
+    rcases eq_zero_or_eq_zero_of_mul_eq_zero _ _ h.symm with h | h
+    exact h
+    exfalso
+    exact succ_ne_zero _ h
+    rw [mul_succ, mul_succ] at h
+    have j : b = c
+    apply hc
+    exact add_right_cancel _ _ _ h
+    rw [j]
+    rfl
+-- TODO: generalizing b.
+
+NewTactic revert
 
 Conclusion
 "
 
 "
+
+

server/nng/NNG/Levels/AdvProposition.lean

@@ -16,4 +16,8 @@ Title "Advanced Proposition World"
 
 Introduction
 "
+In this world we will learn five key tactics needed to solve all the
+levels of the Natural Number Game, namely `constructor`, `rcases`, `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.
 "

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

@@ -10,30 +10,31 @@ 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
+$P\\land Q$ is the proposition \"$P$ and $Q$\".
-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
+  Hint "If your *goal* is `P ∧ Q` then
+  you can make progress with the `constructor` tactic, which turns one goal `P ∧ Q`
+  into two goals, namely `P` and `Q`."
   constructor
+  Hint "Now you have two goals. The first one is `P`, which you can proof now. The
+  second one is `Q` and you see it in the queue \"Other Goals\". You will have to prove it afterwards."
+  Hint (hidden := true) "This first goal can be proved with `exact p`."
   exact p
+  -- Hint "Observe that now the first goal has been proved, so it disappears and you continue
+  -- proving the second goal."
+  -- Hint (hidden := true) "Like the first goal, this is a case for `exact`."
+  -- -- TODO: It looks like these hints get shown above as well, but weirdly the hints from
+  -- -- above to not get shown here.
   exact q
 
 NewTactic constructor
+NewDefinition And
 
 Conclusion
 "
-
 "

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

@@ -1,11 +1,10 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
 Level 10
-Title "Level 10: the law of the excluded middle."
+Title "The law of the excluded middle."
 
 open MyNat
 
@@ -14,39 +13,8 @@ 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
+constructive logic).
 
-```
-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
@@ -54,26 +22,44 @@ Statement
 $$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$ 
 "
     (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by
-  by_cases p : P
+  Hint "For example, you could start as always with
-  · by_cases q : Q
+
-    intro h p' -- cc
+  ```
-    assumption
+  intro h p
-    intro h p'
+  ```
-    have g : ¬ P := h q
+  "
-    contradiction
+  intro h p
-  · by_cases q : Q
+  Hint "From here there is no way to continue with the tactics you've learned so far.
-    intro h p
+
-    assumption
+  Instead you can call `by_cases q : Q`. This creates **two goals**, once under the assumption
-    intro h p
+  that `Q` is true, once assuming `Q` is false."
-    contradiction
+  by_cases q : Q
+  Hint "This first case is trivial."
+  exact q
+  Hint "The second case needs a bit more work, but you can get there with the tactics you've already
+  learned beforehand!"
+  have j := h q
+  exfalso
+  apply j
+  exact p
+
+NewTactic by_cases
 
 Conclusion
 "
+This approach assumed that `P ∨ ¬ P` is true, which is called \"law of excluded middle\".
+It cannot be proven using just tactics like `intro` or `apply`.
+`by_cases p : P` just does `rcases` on this result `P ∨ ¬ P`.
+
+
 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
+-- TODO: I cannot really import `tauto` because of the notation `ℕ` that's used
+-- for `MyNat`.
+-- ## Pro tip
 
-In fact the tactic `tauto!` just kills this goal (and many other logic goals) immediately.
+-- In fact the tactic `tauto` just kills this goal (and many other logic goals) immediately. You'll be
+-- able to use it from now on.
 
-"

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

@@ -1,48 +1,49 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
 Level 2
-Title "the `cases` tactic"
+Title "the `rcases` tactic"
 
 open MyNat
 
 Introduction
 "
-If `P ∧ Q` is in the goal, then we can make progress with `split`.
+If `P ∧ Q` is in the goal, then we can make progress with `constructor`.
-But what if `P ∧ Q` is a hypothesis? In this case, the `cases` tactic will enable
+But what if `P ∧ Q` is a hypothesis? In this case, the `rcases` 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,
+Statement -- and_symm
-symmetry of the \"and\" relation. The obvious first move is
+"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,`
+  Hint "The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,
+  symmetry of the \"and\" relation. The obvious first move is
 
-because the goal is an implication and this tactic is guaranteed
+  ```
-to make progress. Now `h : P ∧ Q` is a hypothesis, and
+  intro h
+  ```
 
-`cases h with p q,`
+  because the goal is an implication and this tactic is guaranteed
+  to make progress."
+  intro h
+  Hint "Now `{h} : P ∧ Q` is a hypothesis, and
 
-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.
+  rcases {h} with ⟨p, q⟩
-"
+  ```
 
-set_option tactic.hygienic false
+  will change `{h}`, the proof of `P ∧ Q`, into two proofs `p : P`
+  and `q : Q`.
 
-Statement --and_symm
+  You can write `⟨p, q⟩` with `\\<>` or `\\<` and `\\>`. Note that `rcases h` by itself will just
-"If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. "
+  automatically name the new assumptions."
-    (P Q : Prop) : P ∧ Q → Q ∧ P :=  by
-  intro h
   rcases h with ⟨p, q⟩
+  Hint "Now a combination of `constructor` and `exact` will get you home."
   constructor
   exact q
   exact p
 
 NewTactic rcases
 
-Conclusion
-"
-
-"

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

@@ -1,6 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
@@ -11,16 +10,31 @@ open MyNat
 
 Introduction
 "
-
+Here is another exercise to `rcases` and `constructor`.
 "
 
 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
+  Hint "Here's a trick:
+  
+  Your first steps would probably be
+  ```
+  intro h
+  rcases h with ⟨p, q⟩
+  ```
+  i.e. introducing a new assumption and then immediately take it appart.
+
+  In that case you could do that in a single step:
+
+  ```
+  intro ⟨p, q⟩
+  ```
+  "
   intro hpq
-  intro hqr
   rcases hpq with ⟨p, q⟩
+  intro hqr
   rcases hqr with ⟨q', r⟩
   constructor
   assumption

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

@@ -1,6 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
@@ -11,10 +10,9 @@ open MyNat
 
 Introduction
 "
-The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `cases`
+The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `rcases`
-and `split` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need
+and `constructor` 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
+to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to.
-`intro h,` you can type `cases h with hpq hqp` to break `h : P ↔ Q` into its constituent parts.
 
 "
 
@@ -22,15 +20,26 @@ 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
+  Hint "Similar to \"and\", you can use `intro` and `rcases` to add the `P ↔ Q` to your
-  intro hqr
+  assumptions and split it into its constituent parts."
-  rcases hpq with ⟨hpq, hqp⟩
+  Branch
-  rcases hqr with ⟨hqr, hrq⟩
+    intro hpq
+    intro hqr
+    Hint "Now you want to use `rcases {hpq} with ⟨pq, qp⟩`."
+    rcases hpq with ⟨hpq, hqp⟩
+    rcases hqr with ⟨hqr, hrq⟩
+  intro ⟨pq, qp⟩
+  intro ⟨qr, rq⟩
+  Hint "If you want to prove an iff-statement, you can use `constructor` to split it
+  into its two implications."
   constructor
-  exact fun x => hqr (hpq x) -- cc
+  · intro p
-  exact fun x => hqp (hrq x) -- cc
+    apply qr
+    apply pq
+    exact p
+  · intro r
+    apply qp
+    apply rq
+    exact r
 
-Conclusion
+NewDefinition Iff
-"
-
-"

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

@@ -1,50 +1,65 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
 
 Game "NNG"
 World "AdvProposition"
 Level 5
-Title "`iff_trans` easter eggs."
+Title "Easter eggs."
 
 open MyNat
 
 Introduction
 "
-Let's try `iff_trans` again. Try proving it in other ways.
+Let's try this again. Try proving it in other ways. (Note that `rcases` is temporarily disabled.)
 
 ### A trick.
 
-Instead of using `cases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P`
+Instead of using `rcases` 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, 
+intro hpq hqr
-split,
+constructor
-intro p,
+intro p
-apply hqr.1,
+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
+Instead of using `rcases` 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;
+this is an argument for *not* running the `rcases` 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.
 "
+-- TODO
+-- ### 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
+  Hint "Make a choice and continue either with `constructor` or `rw`.
+
+  * if you use `constructor`, you will use `{hqr}.1, {hqr}.2, …` later.
+  * if you use `rw`, you can replace all `P`s with `Q`s using `rw [{hpq}]`"
+  Branch
+    rw [hpq]
+    Branch
+      exact hqr
+    rw [hqr]
+    Hint "Now `rfl` can close this goal.
+
+    TODO: Note that the current modification of `rfl` is too weak to prove this. For now, you can
+    use `simp` instead (which calls the \"real\" `rfl` internally)."
+    simp
   constructor
   intro p
+  Hint "Now you can directly `apply {hqr}.1`"
   apply hqr.1
   apply hpq.1
   assumption
@@ -53,6 +68,8 @@ Statement --iff_trans
   apply hqr.2
   assumption
 
+DisabledTactic rcases
+
 Conclusion
 "
 

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

@@ -1,8 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
---import Mathlib.Logic.Basic
 
 Game "NNG"
 World "AdvProposition"
@@ -15,25 +12,28 @@ 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
+If `P ∨ Q` is your goal, then `left` changes this
-goal to `⊢ P`, and `right` changes it to `⊢ Q`.
+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.
 "
+-- 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
+"If $P$ and $Q$ are true/false statements, then $Q\\implies(P\\lor Q)$."
-$$Q\\implies(P\\lor Q).$$ "
     (P Q : Prop) : Q → (P ∨ Q) := by
+  Hint (hidden := true) "Let's start with an initial `intro` again."
   intro q
+  Hint "Now you need to choose if you want to prove the `left` or `right` side of the goal."
+  Branch
+    left
+    -- TODO: This message is also shown on the correct track. Need strict hints.
+    -- Hint "That was an unfortunate choice, you entered a dead end that cannot be proved anymore.
+    -- Hit \"Undo\"!"
   right
-  assumption
+  exact q
 
 NewTactic left right
+NewDefinition Or
 
-Conclusion
-"
-
-"

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

@@ -1,7 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvProposition"
@@ -13,27 +11,45 @@ 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
+  Hint "`intro h` is the obvious start."
   intro h
+  Branch
+    left
+    Hint "This is a dead end that is not provable anymore. Hit \"undo\"."
+  Branch
+    right
+    Hint "This is a dead end that is not provable anymore. Hit \"undo\"."
+  Hint "But now, even though the goal is an `∨` statement, both `left` and `right` put
+  you in a situation with an impossible goal. Fortunately,
+  you can do `rcases h with p | q`. (that is a normal vertical slash)
+  "
   rcases h with p | q
+  Hint " Something new just happened: because
+  there are two ways to prove the assumption `P ∨ Q` (namely, proving `P` or proving `Q`),
+  the `rcases` tactic turns one goal into two, one for each case.
+
+  So now you proof the goal under the assumption that `P` is true, and waiting under \"Other Goals\"
+  there is the same goal but under the assumption that `Q` is true.
+
+  You should be able to make it home from there. "
   right
   exact p
+  Hint "Note how now you finished the first goal and jumped to the one, where you assume `Q`."
   left
   exact q
 
 Conclusion
 "
+Well done! Note that the syntax for `rcases` is different whether it's an \"or\" or an \"and\".
 
+* `rcases h with ⟨p, q⟩` splits an \"and\" in the assumptions into two parts. You get two assumptions
+but still only one goal.
+* `rcases h with p | q` splits an \"or\" in the assumptions. You get **two goals** which have different
+assumptions, once assumping the lefthand-side of the dismantled \"or\"-assumption, once the righthand-side.
 "

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

@@ -1,7 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
 
 Game "NNG"
 World "AdvProposition"
@@ -12,7 +10,7 @@ open MyNat
 
 Introduction
 "
-We know that `x(y+z)=xy+xz` for numbers, and this
+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.
@@ -28,34 +26,28 @@ $$P\\land(Q\\lor R)\\iff(P\\land Q)\\lor (P\\land R).$$ "
   rcases hqr with q | r
   left
   constructor
-  assumption
+  exact hp
-  assumption
+  exact q
   right
   constructor
-  assumption
+  exact hp
-  assumption
+  exact r
   intro h
   rcases h with hpq | hpr
   rcases hpq with ⟨p, q⟩
   constructor
-  assumption
+  exact p
   left
-  assumption
+  exact q
   rcases hpr with ⟨hp, hr⟩
   constructor
-  assumption
+  exact hp
   right
-  assumption
+  exact hr
+
 
 Conclusion
 "
-## Pro tip
+You already know enough to embark on advanced addition world. But the next two levels comprise
-
+just a couple more things.
-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

@@ -1,9 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import Std.Tactic.RCases
-import NNG.MyNat.Theorems.Proposition
-
-
 
 Game "NNG"
 World "AdvProposition"
@@ -14,58 +10,43 @@ 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
+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`. 
+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. 
+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
+  Hint "Start as usual with `intro ⟨p, np⟩`."
+  Branch
+    exfalso
+    -- TODO: This hint needs to be strict
+    -- Hint "Not so quick! Now you just threw everything away."
   intro h
+  Hint "You should also call `rcases` on your assumption `{h}`."
   rcases h with ⟨p, np ⟩
-  contradiction
+  -- TODO: This hint should before the last `exact p` step again.
-  -- rw [not_iff_imp_false] at np
+  Hint "Now you can call `exfalso` to throw away your goal `Q`. It will be replaced with `False` and
-  -- exfalso
+  which means you will have to prove a contradiction."
-  -- apply np
+  Branch
-  -- exact p
+    -- TODO: Would `contradiction` not be more useful to introduce than `exfalso`?
-
+    contradiction
-NewTactic exfalso contradiction
+  exfalso
-
+  Hint "Recall that `{np} : ¬ P` means `np : P → False`, which means you can simply `apply {np}` now.
-Conclusion
+
-"
+  You can also first call `rw [Not] at {np}` to make this step more explicit."
-## Pro tip.
+  Branch
-
+    rw [Not] at np
-`¬ P` is actually `P → false` *by definition*. Try
+  apply np
-commenting out `rw not_iff_imp_false at ...` by putting two minus signs `--`
+  exact p
-before the `rw`. Does it still compile?
+
--/
+-- TODO: `contradiction`?
-
+NewTactic exfalso
-/- Tactic : exfalso
+-- DisabledTactic cc
-
+LemmaTab "Prop"
-## 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_1.lean

@@ -1,6 +1,6 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
+
-import NNG.MyNat.Multiplication
+-- TODO: Cannot import level from different world.
 
 Game "NNG"
 World "Function"
@@ -64,7 +64,7 @@ Statement
   "
   exact h p
 
-NewTactic exact
+NewTactic exact simp
 
 Conclusion
 "

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

@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
 import NNG.MyNat.Multiplication
 
 Game "NNG"
@@ -37,14 +36,14 @@ Statement
   `intro n`"
   intro n
   Hint "Our job now is to construct a natural number, which is
-  allowed to depend on $n$. We can do this using `exact` and
+  allowed to depend on ${n}$. We can do this using `exact` and
   writing a formula for the function we want to define. For example
   we imported addition and multiplication at the top of this file,
   so
 
-  `exact 3*n+2,`
+  `exact 3 * {n} + 2`
 
-  will close the goal, ultimately defining the function $f(n)=3n+2$."
+  will close the goal, ultimately defining the function $f({n})=3{n}+2$."
   exact 3 * n + 2
 
 NewTactic intro

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

@@ -1,6 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "Function"
@@ -28,8 +26,8 @@ functions looks like this pictorially:
 $$
 \\begin{CD}
   P  @>{h}>> Q       @>{i}>> R \\\\
-  @.         @V{j}VV           \\\\
+  @.         @VV{j}V           \\\\
-  S  @>{k}>> T       @>{l}>> U \\\\
+  S  @>>{k}> T       @>>{l}> U
 \\end{CD}
 $$
 
@@ -42,19 +40,26 @@ Statement
     U := by
   Hint "Indeed, we could solve this level in one move by typing
 
-  `exact l (j (h p))`
+  ```
+  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 an element of $Q$:
 
-  have q := h p"
+  ```
+  have q := h p
+  ```
+  "
   Branch
     exact l (j (h p))
   have q := h p
   Hint "
   and now we note that $j(q)$ is an element of $T$
 
-  `have t : T := j q`
+  ```
+  have t : T := j q
+  ```
 
   (notice how we can explicitly tell Lean
   what set we thought $t$ was in, with that `: T` thing before the `:=`.
@@ -64,7 +69,9 @@ Statement
   Hint "
   Now we could even define $u$ to be $l(t)$:
 
-  `have u : U := l t`
+  ```
+  have u : U := l t
+  ```
   "
   have u : U := l t
   Hint "…and then finish the level with `exact u`."

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

@@ -1,6 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "Function"
@@ -15,8 +13,8 @@ Introduction
 $$
 \\begin{CD}
   P  @>{h}>> Q       @>{i}>> R \\\\
-  @.         @V{j}VV           \\\\
+  @.         @VV{j}V           \\\\
-  S  @>{k}>> T       @>{l}>> U \\\\
+  S  @>>{k}> T       @>>{l}> U
 \\end{CD}
 $$
 
@@ -41,10 +39,13 @@ by
   a function, so it would suffice to construct an element of $T$. Tell
   Lean this by starting the proof below with
 
-  `apply l`"
+  ```
+  apply l
+  ```
+  "
   apply l
   Hint "Notice that our assumptions don't change but *the goal changes*
-  from `Goal: U` to `Goal: T`.
+  from `U` to `T`.
 
   Keep `apply`ing functions until your goal is `P`, and try not
   to get lost!"
@@ -61,8 +62,3 @@ by
 
 NewTactic apply
 DisabledTactic «have»
-
-Conclusion
-"
-
-"

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

@@ -1,6 +1,4 @@
 import NNG.Metadata
-import NNG.Levels.Addition.Level_6
-import NNG.MyNat.Multiplication
 
 Game "NNG"
 World "Function"
@@ -31,7 +29,9 @@ Statement
   `intro` tactic from level 2, Lean's version of \"let $p\\in P$ be arbitrary.\"
   So let's start with
 
-  `intro p`"
+  ```
+  intro p
+  ```"
   intro p
   Hint "
   We now have an arbitrary element $p\\in P$ and we are supposed to be constructing
@@ -39,11 +39,15 @@ Statement
   sends everything to $p$?
   This will work. So let $q\\in Q$ be arbitrary:
 
-  `intro q`"
+  ```
+  intro q
+  ```"
   intro q
   Hint "and then let's output `p`.
 
-  `exact p`"
+  ```
+  exact p
+  ```"
   exact p
 
 Conclusion

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

@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
@@ -14,21 +13,13 @@ 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`
+```
+have j : Q → R := f p
+```
 
 if `f : P → (Q → R)` and `p : P`. Remember the trick with the colon in `have`:
 we could just write `have j := f p,` but this way we can be sure that `j` is
 what we actually expect it to be.
-
-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 a function from `P` to anything, it's a function from
-`P → (Q → R)` to something. In fact you can save time by starting
-with `intros f h p`, which introduces three variables at once, although you'd
-better then look at your tactic state to check that you called all those new
-terms sensible things.
-
-After all the intros, you find that your your goal is `Goal: R`…
 "
 
 Statement
@@ -36,6 +27,13 @@ Statement
 make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,\\operatorname{Hom}(Q,R)),
 \\operatorname{Hom}(\\operatorname{Hom}(P,Q),\\operatorname{Hom}(P,R)))$."
     (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) := by
+  Hint "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 a function from `P` to anything, it's a function from
+  `P → (Q → R)` to something. In fact you can save time by starting
+  with `intro f h p`, which introduces three variables at once, although you'd
+  better then look at your tactic state to check that you called all those new
+  terms sensible things. "
   intro f
   intro h
   intro p
@@ -47,14 +45,17 @@ make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,\\operatorname{Hom
 
   What happens if you just try `apply {f}`?
   "
-  Branch
+  -- TODO: This hint needs strictness to make sense
-    apply f
+  -- Branch
-    Hint "Can you figure out what just happened? This is a little
+  --   apply f
-    `apply` easter egg. Why is it mathematically valid?"
+  --   Hint "Can you figure out what just happened? This is a little
-    Hint (hidden := true) "Note that there are two goals now, first you need to
+  --   `apply` easter egg. Why is it mathematically valid?"
-    provide an element in ${P}$ which you did not provide before."
+  --   Hint (hidden := true) "Note that there are two goals now, first you need to
+  --   provide an element in ${P}$ which you did not provide before."
   have j : Q → R := f p
   apply j
+  Hint (hidden := true) "Is there something you could apply? something of the form
+  `_ → Q`?"
   apply h
   exact p
 

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

@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"

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

@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
@@ -13,31 +12,6 @@ Introduction
 Level 8 is the same as level 7, except we have replaced the
 set $F$ with the empty set $\\emptyset$. The same proof will work (after all, our
 previous proof worked for all sets, and the empty set is a set).
-But note that if you start with `intro f, intro h, intro p,`
-(which can incidentally be shortened to `intros f h p`),
-then the local context looks like this:
-
-```
-P Q : Type,
-f : P → Q,
-h : Q → empty,
-p : P
-⊢ empty
-```
-
-and your job is to construct an element of the empty set!
-This on the face of it seems hard, but what is going on is that
-our hypotheses (we have an element of $P$, and functions $P\\to Q$
-and $Q\\to\\emptyset$) are themselves contradictory, so
-I guess we are doing some kind of proof by contradiction at this point? However,
-if your next line is `apply h` then all of a sudden the goal
-seems like it might be possible again. If this is confusing, note
-that the proof of the previous world worked for all sets $F$, so in particular
-it worked for the empty set, you just probably weren't really thinking about
-this case explicitly beforehand. [Technical note to constructivists: I know
-that we are not doing a proof by contradiction. But how else do you explain
-to a classical mathematician that their goal is to prove something false
-and this is OK because their hypotheses don't add up?]
 "
 
 Statement
@@ -45,6 +19,7 @@ Statement
 make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
 \\operatorname{Hom}(\\operatorname{Hom}(Q,\\emptyset),\\operatorname{Hom}(P,\\emptyset)))$."
     (P Q : Type) : (P → Q) → ((Q → Empty) → (P → Empty)) := by
+  Hint (hidden := true) "Maybe start again with `intro`."
   intros f h p
   Hint "
   Note that now your job is to construct an element of the empty set!
@@ -52,9 +27,11 @@ make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
   our hypotheses (we have an element of $P$, and functions $P\\to Q$
   and $Q\\to\\emptyset$) are themselves contradictory, so
   I guess we are doing some kind of proof by contradiction at this point? However,
-  if your next line is 
+  if your next line is
 
-  `apply {h}`
+  ```
+  apply {h}
+  ```
 
   then all of a sudden the goal
   seems like it might be possible again. If this is confusing, note
@@ -69,7 +46,4 @@ make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
   apply f
   exact p
 
-Conclusion
+Conclusion ""
-"
-
-"

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

@@ -1,5 +1,4 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Function"
@@ -24,7 +23,9 @@ Statement
     (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)
     (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by
+  Hint "In any case, start with `intro a`!"
   intro a
+  Hint "Now use a combination of `have` and `apply`."
   apply f15
   apply f11
   apply f9

server/nng/NNG/Levels/Inequality.lean

@@ -1,20 +1,20 @@
 import NNG.Levels.Inequality.Level_1
-import NNG.Levels.Inequality.Level_2
+-- import NNG.Levels.Inequality.Level_2
-import NNG.Levels.Inequality.Level_3
+-- import NNG.Levels.Inequality.Level_3
-import NNG.Levels.Inequality.Level_4
+-- import NNG.Levels.Inequality.Level_4
-import NNG.Levels.Inequality.Level_5
+-- import NNG.Levels.Inequality.Level_5
-import NNG.Levels.Inequality.Level_6
+-- import NNG.Levels.Inequality.Level_6
-import NNG.Levels.Inequality.Level_7
+-- import NNG.Levels.Inequality.Level_7
-import NNG.Levels.Inequality.Level_8
+-- import NNG.Levels.Inequality.Level_8
-import NNG.Levels.Inequality.Level_9
+-- import NNG.Levels.Inequality.Level_9
-import NNG.Levels.Inequality.Level_10
+-- import NNG.Levels.Inequality.Level_10
-import NNG.Levels.Inequality.Level_11
+-- import NNG.Levels.Inequality.Level_11
-import NNG.Levels.Inequality.Level_12
+-- import NNG.Levels.Inequality.Level_12
-import NNG.Levels.Inequality.Level_13
+-- import NNG.Levels.Inequality.Level_13
-import NNG.Levels.Inequality.Level_14
+-- import NNG.Levels.Inequality.Level_14
-import NNG.Levels.Inequality.Level_15
+-- import NNG.Levels.Inequality.Level_15
-import NNG.Levels.Inequality.Level_16
+-- import NNG.Levels.Inequality.Level_16
-import NNG.Levels.Inequality.Level_17
+-- import NNG.Levels.Inequality.Level_17
 
 Game "NNG"
 World "Inequality"

server/nng/NNG/Levels/Multiplication.lean

@@ -15,4 +15,23 @@ Title "Multiplication World"
 
 Introduction
 "
+In this world you start with the definition of multiplication on `ℕ`. It is
+defined by recursion, just like addition was. So you get two new axioms:
+
+  * `mul_zero (a : ℕ) : a * 0 = 0`
+  * `mul_succ (a b : ℕ) : a * succ b = a * b + a`
+
+In words, we define multiplication by \"induction on the second variable\",
+with `a * 0` defined to be `0` and, if we know `a * b`, then `a` times
+the number after `b` is defined to be `a * b + a`.
+
+You can keep all the theorems you proved about addition, but
+for multiplication, those two results above are what you've got right now.
+
+So what's going on in multiplication world? Like addition, we need to go
+for the proofs that multiplication
+is commutative and associative, but as well as that we will
+need to prove facts about the relationship between multiplication
+and addition, for example `a * (b + c) = a * b + a * c`, so now
+there is a lot more to do. Good luck!
 "

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

@@ -1,24 +1,35 @@
-import NNG.Metadata
+import NNG.MyNat.Multiplication
-import NNG.MyNat.Addition
+import NNG.Levels.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 1
-Title ""
+Title "zero_mul"
 
 open MyNat
 
 Introduction
 "
+As a side note, the lemmas about addition are still available in your inventory
+in the lemma tab \"Add\" while the new lemmas about multiplication appear in the
+tab \"Mul\".
 
+We are given `mul_zero`, and the first thing to prove is `zero_mul`.
+Like `zero_add`, we of course prove it by induction.
 "
 
-Statement
+Statement MyNat.zero_mul
-""
+"For all natural numbers $m$, we have $ 0 \\cdot m = 0$."
-    : true := by
+    (m : ℕ) : 0 * m = 0 := by
-  trivial
+  induction m
+  rw [mul_zero]
+  rfl
+  rw [mul_succ]
+  rw [n_ih]
+  rw [add_zero]
+  rfl
 
-Conclusion
+NewTactic simp
-"
+NewLemma MyNat.mul_zero MyNat.mul_succ
-
+NewDefinition Mul
-"
+LemmaTab "Mul"

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

@@ -1,24 +1,31 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_1
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 2
-Title ""
+Title "mul_one"
 
 open MyNat
 
 Introduction
 "
+In this level we'll need to use
 
-"
+* `one_eq_succ_zero : 1 = succ 0 `
-
-Statement
-""
-    : true := by
-  trivial
 
-Conclusion
+which was mentioned back in Addition World  (see \"Add\" tab in your inventory) and
+which will be a useful thing to rewrite right now, as we
+begin to prove a couple of lemmas about how `1` behaves
+with respect to multiplication.
 "
 
-"
+Statement MyNat.mul_one
+"For any natural number $m$, we have $ m \\cdot 1 = m$."
+    (m : ℕ) : m * 1 = m := by
+rw [one_eq_succ_zero]
+rw [mul_succ]
+rw [mul_zero]
+rw [zero_add]
+rfl
+
+LemmaTab "Mul"

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

@@ -1,24 +1,38 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_2
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 3
-Title ""
+Title "one_mul"
 
 open MyNat
 
 Introduction
 "
+These proofs from addition world might be useful here:
 
+* `one_eq_succ_zero : 1 = succ 0`
+* `succ_eq_add_one a : succ a = a + 1`
+
+We just proved `mul_one`, now let's prove `one_mul`.
+Then we will have proved, in fancy terms,
+that 1 is a \"left and right identity\"
+for multiplication (just like we showed that
+0 is a left and right identity for addition
+with `add_zero` and `zero_add`).
 "
 
-Statement
+Statement MyNat.one_mul
-""
+"For any natural number $m$, we have $ 1 \\cdot m = m$."
-    : true := by
+    (m : ℕ): 1 * m = m := by
-  trivial
+  induction m with d hd
+  · rw [mul_zero]
+    rfl
+  · rw [mul_succ]
+    rw [hd]
+    rw [succ_eq_add_one]
+    rfl
 
-Conclusion
+LemmaTab "Mul"
-"
 
-"
+Conclusion ""

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

@@ -1,24 +1,44 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_3
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 4
-Title ""
+Title "mul_add"
 
 open MyNat
 
 Introduction
 "
+Where are we going? Well we want to prove `mul_comm`
+and `mul_assoc`, i.e. that `a * b = b * a` and
+`(a * b) * c = a * (b * c)`. But we *also* want to
+establish the way multiplication interacts with addition,
+i.e. we want to prove that we can \"expand out the brackets\"
+and show `a * (b + c) = (a * b) + (a * c)`.
+The technical term for this is \"left distributivity of
+multiplication over addition\" (there is also right distributivity,
+which we'll get to later).
 
+Note the name of this proof -- `mul_add`. And note the left
+hand side -- `a * (b + c)`, a multiplication and then an addition.
+I think `mul_add` is much easier to remember than \"`left_distrib`\",
+an alternative name for the proof of this lemma.
 "
 
-Statement
+Statement MyNat.mul_add
-""
+"Multiplication is distributive over addition.
-    : true := by
+In other words, for all natural numbers $a$, $b$ and $t$, we have
-  trivial
+$t(a + b) = ta + tb$."
+    (t a b : ℕ) : t * (a + b) = t * a + t * b := by
+  induction b with d hd
+  · rw [add_zero, mul_zero, add_zero]
+    rfl
+  · rw [add_succ]
+    rw [mul_succ]
+    rw [hd]
+    rw [mul_succ]
+    rw [add_assoc]
+    rfl
 
-Conclusion
+LemmaTab "Mul"
-"
 
-"

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

@@ -1,22 +1,41 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_4
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 5
-Title ""
+Title "mul_assoc"
 
 open MyNat
 
 Introduction
 "
+We now have enough to prove that multiplication is associative.
+
+## Random tactic hint
+
+You can do `repeat rw [mul_succ]` to repeat a tactic as often as possible.
 
 "
 
-Statement
+Statement MyNat.mul_assoc
-""
+"Multiplication is associative.
-    : true := by
+In other words, for all natural numbers $a$, $b$ and $c$, we have
-  trivial
+$(ab)c = a(bc)$."
+    (a b c : ℕ) : (a * b) * c = a * (b * c)  := by
+  induction c with d hd
+  · repeat rw [mul_zero]
+    rfl
+  · rw [mul_succ]
+    rw [mul_succ]
+    rw [hd]
+    rw [mul_add]
+    rfl
+
+NewTactic «repeat»
+LemmaTab "Mul"
+
+-- TODO: old version introduced `rwa` here, but it would need to be modified
+-- as our `rw` does not call `rfl` at the end.
 
 Conclusion
 "

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

@@ -1,22 +1,50 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_5
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 6
-Title ""
+Title "succ_mul"
 
 open MyNat
 
 Introduction
 "
+We now begin our journey to `mul_comm`, the proof that `a * b = b * a`.
+We'll get there in level 8. Until we're there, it is frustrating
+but true that we cannot assume commutativity. We have `mul_succ`
+but we're going to need `succ_mul` (guess what it says -- maybe you
+are getting the hang of Lean's naming conventions).
 
+Remember also that we have tools like
+
+* `add_right_comm a b c : a + b + c = a + c + b`
+
+These things are the tools we need to slowly build up the results
+which we will need to do mathematics \"normally\".
+We also now have access to Lean's `simp` tactic,
+which will solve any goal which just needs a bunch
+of rewrites of `add_assoc` and `add_comm`. Use if
+you're getting lazy!
 "
 
-Statement
+Statement MyNat.succ_mul
-""
+"For all natural numbers $a$ and $b$, we have
-    : true := by
+$\\operatorname{succ}(a) \\cdot b = ab + b$."
-  trivial
+    (a b : ℕ) : succ a * b = a * b + b := by
+  induction b with d hd
+  · rw [mul_zero]
+    rw [mul_zero]
+    rw [add_zero]
+    rfl
+  · rw [mul_succ]
+    rw [mul_succ]
+    rw [hd]
+    rw [add_succ]
+    rw [add_succ]
+    rw [add_right_comm]
+    rfl
+
+LemmaTab "Mul"
 
 Conclusion
 "

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

@@ -1,22 +1,44 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_6
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 7
-Title ""
+Title "add_mul"
 
 open MyNat
 
 Introduction
 "
-
+We proved `mul_add` already, but because we don't have commutativity yet
+we also need to prove `add_mul`. We have a bunch of tools now, so this won't
+be too hard. You know what -- you can do this one by induction on any of
+the variables. Try them all! Which works best? If you can't face
+doing all the commutativity and associativity, remember the high-powered
+`simp` tactic mentioned at the bottom of Addition World level 6,
+which will solve any puzzle which needs only commutativity
+and associativity. If your goal looks like `a + (b + c) = c + b + a` or something,
+don't mess around doing it explicitly with `add_comm` and `add_assoc`,
+just try `simp`.
 "
 
-Statement
+Statement MyNat.add_mul
-""
+"Addition is distributive over multiplication.
-    : true := by
+In other words, for all natural numbers $a$, $b$ and $t$, we have
-  trivial
+$(a + b) \times t = at + bt$."
+    (a b t : ℕ) : (a + b) * t = a * t + b * t := by
+  induction b with d hd
+  · rw [zero_mul]
+    rw [add_zero]
+    rw [add_zero]
+    rfl
+  · rw [add_succ]
+    rw [succ_mul]
+    rw [hd]
+    rw [succ_mul]
+    rw [add_assoc]
+    rfl
+
+LemmaTab "Mul"
 
 Conclusion
 "

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

@@ -1,24 +1,46 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_7
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 8
-Title ""
+Title "mul_comm"
 
 open MyNat
 
 Introduction
 "
-
+Finally, the boss level of multiplication world. But (assuming you
+didn't cheat) you are well-prepared for it -- you have `zero_mul`
+and `mul_zero`, as well as `succ_mul` and `mul_succ`. After this
+level you can of course throw away one of each pair if you like,
+but I would recommend you hold on to them, sometimes it's convenient
+to have exactly the right tools to do a job.
 "
 
-Statement
+Statement MyNat.mul_comm
-""
+"Multiplication is commutative."
-    : true := by
+    (a b : ℕ) : a * b = b * a := by
-  trivial
+  induction b with d hd
+  · rw [zero_mul]
+    rw [mul_zero]
+    rfl
+  · rw [succ_mul]
+    rw [← hd]
+    rw [mul_succ]
+    rfl
+
+LemmaTab "Mul"
 
 Conclusion
 "
+You've now proved that the natural numbers are a commutative semiring!
+That's the last collectible in Multiplication World.
 
+* `CommSemiring ℕ`
+
+But don't leave multiplication just yet -- prove `mul_left_comm`, the last
+level of the world, and then we can beef up the power of `simp`.
 "
+
+-- TODO: collectible
+-- instance mynat.comm_semiring : comm_semiring mynat := by structure_helper

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

@@ -1,24 +1,57 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication.Level_8
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Multiplication"
 Level 9
-Title ""
+Title "mul_left_comm"
 
 open MyNat
 
 Introduction
 "
+You are equipped with
+
+* `mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c)`
+* `mul_comm (a b : ℕ) : a * b = b * a`
+
+Re-read the docs for `rw` so you know all the tricks.
+You can see them in your inventory on the right.
 
 "
 
-Statement
+Statement MyNat.mul_left_comm
-""
+"For all natural numbers $a$ $b$ and $c$, we have $a(bc)=b(ac)$."
-    : true := by
+    (a b c : ℕ) : a * (b * c) = b * (a * c) := by
-  trivial
+  rw [← mul_assoc]
+  rw [mul_comm a]
+  rw [mul_assoc]
+  rfl
+
+LemmaTab "Mul"
+
+-- TODO: make simp work:
+-- attribute [simp] mul_assoc mul_comm mul_left_comm
 
 Conclusion
 "
+And now I whisper a magic incantation
+
+```
+attribute [simp] mul_assoc mul_comm mul_left_comm
+```
+
+and all of a sudden Lean can automatically do levels which are
+very boring for a human, for example
+
+```
+example (a b c d e : ℕ) :
+    (((a * b) * c) * d) * e = (c * ((b * e) * a)) * d := by
+  simp
+```
 
+If you feel like attempting Advanced Multiplication world
+you'll have to do Function World and the Proposition Worlds first.
+These worlds assume a certain amount of mathematical maturity
+(perhaps 1st year undergraduate level).
+Your other possibility is Power World, with the \"final boss\".
 "

server/nng/NNG/Levels/Power.lean

@@ -1,10 +1,3 @@
-import NNG.Levels.Power.Level_1
-import NNG.Levels.Power.Level_2
-import NNG.Levels.Power.Level_3
-import NNG.Levels.Power.Level_4
-import NNG.Levels.Power.Level_5
-import NNG.Levels.Power.Level_6
-import NNG.Levels.Power.Level_7
 import NNG.Levels.Power.Level_8
 
 Game "NNG"
@@ -18,17 +11,15 @@ 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_zero (a : ℕ) : a ^ 0 = 1`
-  * `pow_succ (a b : mynat) : a ^ succ(b) = a ^ b * a`
+  * `pow_succ (a b : ℕ) : 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.
+The usual tactics `induction`, `rw` and `rfl` should see you through.
-You might want to fiddle with the
+You should probably look at your inverntory again: addition and multiplication
-drop-down menus on the left so you can see which theorems of Power World
+have a solid API by now, i.e. if you need something about addition
-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.
 

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

@@ -1,5 +1,5 @@
-import NNG.Metadata
+import NNG.Levels.Multiplication
---import NNG.MyNat.Power
+import NNG.MyNat.Power
 
 Game "NNG"
 World "Power"
@@ -8,18 +8,12 @@ Title "zero_pow_zero"
 
 open MyNat
 
-Introduction
+Statement MyNat.zero_pow_zero
-"
-
-"
-
-Statement
 "$0 ^ 0 = 1$"
-    : (0 : ℕ) ^ 0 = (1 : ℕ) := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by
+    : (0 : ℕ) ^ 0  = 1 := by
-  trivial
+  rw [pow_zero]
-
+  rfl
-Conclusion
-"
-
-"
 
+NewLemma MyNat.pow_zero MyNat.pow_succ
+NewDefinition Pow
+LemmaTab "Pow"

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

@@ -1,24 +1,17 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_1
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Power"
 Level 2
-Title ""
+Title "zero_pow_succ"
 
 open MyNat
 
-Introduction
+Statement MyNat.zero_pow_succ
-"
+"For all naturals $m$, $0 ^{\\operatorname{succ} (m)} = 0$."
+    (m : ℕ) : (0 : ℕ) ^ (succ m) = 0 := by
+  rw [pow_succ]
+  rw [mul_zero]
+  rfl
 
-"
+LemmaTab "Pow"
-
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
-
-"

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

@@ -1,24 +1,19 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_2
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Power"
 Level 3
-Title ""
+Title "pow_one"
 
 open MyNat
 
-Introduction
+Statement MyNat.pow_one
-"
+"For all naturals $a$, $a ^ 1 = a$."
+    (a : ℕ) : a ^ 1 = a  := by
+  rw [one_eq_succ_zero]
+  rw [pow_succ]
+  rw [pow_zero]
+  rw [one_mul]
+  rfl
 
-"
+LemmaTab "Pow"
-
-Statement
-""
-    : true := by
-  trivial
-
-Conclusion
-"
-
-"

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

@@ -1,25 +1,22 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_3
-import NNG.MyNat.Addition
+
 
 Game "NNG"
 World "Power"
 Level 4
-Title ""
+Title "one_pow"
 
 open MyNat
 
-Introduction
+Statement MyNat.one_pow
-"
+"For all naturals $m$, $1 ^ m = 1$."
-
+    (m : ℕ) : (1 : ℕ) ^ m = 1 := by
-"
+  induction m with t ht
-
+  · rw [pow_zero]
-Statement
+    rfl
-""
+  · rw [pow_succ]
-    : true := by
+    rw [ht]
-  trivial
+    rw [mul_one]
-
+    rfl
-Conclusion
-"
 
-"
+LemmaTab "Pow"
-  

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

@@ -1,24 +1,20 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_4
-import NNG.MyNat.Addition
+
 
 Game "NNG"
 World "Power"
 Level 5
-Title ""
+Title "pow_add"
 
 open MyNat
 
-Introduction
+Statement MyNat.pow_add
-"
+"For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m  a ^ n$."
-
+    (a m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n := by
-"
+  induction n with t ht
-
+  · rw [add_zero, pow_zero, mul_one]
-Statement
+    rfl
-""
+  · rw [add_succ, pow_succ, pow_succ, ht, mul_assoc]
-    : true := by
+    rfl
-  trivial
-
-Conclusion
-"
 
-"
+LemmaTab "Pow"

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

@@ -1,24 +1,30 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_5
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Power"
 Level 6
-Title ""
+Title "mul_pow"
 
 open MyNat
 
 Introduction
 "
-
+You might find the tip at the end of level 9 of Multiplication World
+useful in this one. You can go to the main menu and pop back into
+Multiplication World and take a look -- you won't lose any of your
+proofs.
 "
 
-Statement
+Statement MyNat.mul_pow
-""
+"For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$."
-    : true := by
+    (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by
-  trivial
+  induction n with t Ht
-
+  · rw [pow_zero, pow_zero, pow_zero, mul_one]
-Conclusion
+    rfl
-"
+  · rw [pow_succ, pow_succ, pow_succ, Ht]
+    -- simp
+    repeat rw [mul_assoc]
+    rw [mul_comm a (_ * b), mul_assoc, mul_comm b a]
+    rfl
 
-"
+LemmaTab "Pow"

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

@@ -1,24 +1,35 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_6
-import NNG.MyNat.Addition
 
 Game "NNG"
 World "Power"
 Level 7
-Title ""
+Title "pow_pow"
 
 open MyNat
 
 Introduction
 "
-
+Boss level! What will the collectible be?
 "
 
-Statement
+Statement MyNat.pow_pow
-""
+"For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$."
-    : true := by
+    (a m n : ℕ) : (a ^ m) ^ n = a ^ (m * n) := by
-  trivial
+  induction n with t Ht
+  · rw [mul_zero, pow_zero, pow_zero]
+    rfl
+  · rw [pow_succ, Ht, mul_succ, pow_add]
+    rfl
+
+LemmaTab "Pow"
 
 Conclusion
 "
+Apparently Lean can't find a collectible, even though you feel like you
+just finished power world so you must have proved *something*. What should the
+collectible for this level be called?
 
+But what is this? It's one of those twists where there's another
+boss after the boss you thought was the final boss! Go to the next
+level!
 "

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

@@ -1,22 +1,49 @@
-import NNG.Metadata
+import NNG.Levels.Power.Level_7
-import NNG.MyNat.Addition
+-- import Mathlib.Tactic.Ring
 
 Game "NNG"
 World "Power"
 Level 8
-Title ""
+Title "add_squared"
 
 open MyNat
 
 Introduction
 "
+[final boss music] 
 
+You see something written on the stone dungeon wall:
+```
+by
+  rw [two_eq_succ_one]
+  rw [one_eq_succ_zero]
+  repeat rw [pow_succ]
+  …
+```
+
+and you can't make out the last two lines because there's a kind
+of thing in the way that will magically disappear
+but only when you've beaten the boss.
 "
 
-Statement
+Statement MyNat.add_squared
-""
+"For all naturals $a$ and $b$, we have
-    : true := by
+$$(a+b)^2=a^2+b^2+2ab.$$"
-  trivial
+  (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b := by
+  rw [two_eq_succ_one]
+  rw [one_eq_succ_zero]
+  repeat rw [pow_succ]
+  repeat rw [pow_zero]
+  --ring
+  repeat rw [one_mul]
+  rw [add_mul, mul_add, mul_add, mul_comm b a]
+  rw [succ_mul, succ_mul, zero_mul, zero_add, add_mul]
+  repeat rw [add_assoc]
+  rw [add_comm _ (b * b), ← add_assoc _ (b*b), add_comm _ (b*b), add_assoc]
+  rfl
+
+NewLemma MyNat.two_eq_succ_one
+LemmaTab "Pow"
 
 Conclusion
 "

server/nng/NNG/Levels/Proposition.lean

@@ -6,7 +6,7 @@ import NNG.Levels.Proposition.Level_5
 import NNG.Levels.Proposition.Level_6
 import NNG.Levels.Proposition.Level_7
 import NNG.Levels.Proposition.Level_8
--- import NNG.Levels.Proposition.Level_9 -- `cc` is not ported
+import NNG.Levels.Proposition.Level_9 -- `cc` is not ported
 
 
 Game "NNG"
@@ -15,4 +15,34 @@ Title "Proposition World"
 
 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 `mynat`, 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.
+
+In this world you will see the local context in the following kind of state:
+
+```
+Objects:
+  P : Prop
+Assumptions:
+  p : P
+```
+
+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.
 "

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

@@ -10,35 +10,7 @@ open MyNat
 
 Introduction
 "
-A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`.
+What's going on in this world?
-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
@@ -46,9 +18,13 @@ 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:
+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
+"
 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
@@ -59,20 +35,17 @@ 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`
+```
+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$. 
+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

@@ -45,14 +45,16 @@ Statement
   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
+  ```
   "
   intro p
   Hint "
-  Our job now is to construct a proof of $P$. But $p$ is a proof of $P$.
+  Our job now is to construct a proof of $P$. But ${p}$ is a proof of $P$.
   So
 
-  `exact p`
+  `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.
@@ -60,8 +62,3 @@ Statement
   and small letters for proofs.
   "
   exact p
-
-Conclusion
-"
-
-"

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

@@ -25,42 +25,55 @@ 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)
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
+\\end{CD}
+$$
 
 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
+  Hint "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
+  ```
+  "
   have q := h p
+  Hint "
+  and then we note that $j {q}$ is a proof of $T$:
+
+  ```
+  have t : T := j {q}
+  ```
+  "
   have t := j q
+  Hint "
+  (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}
+  ```
+  "
   have u := l t
+  Hint " and now finish the level with `exact {u}`."
   exact u
 
 DisabledTactic apply
@@ -73,17 +86,20 @@ 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,
+Objects:
-p : P,
+  P Q R S T U : Prop
-h : P → Q,
+Assumptions:
-i : Q → R,
+  p : P
-j : Q → T,
+  h : P → Q
-k : S → T,
+  i : Q → R
-l : T → U,
+  j : Q → T
-q : Q,
+  k : S → T
-t : T,
+  l : T → U
-u : U
+  q : Q
-⊢ U
+  t : T
+  u : U
+Goal :
+  U
 ```
 
 It was already bad enough to start with, and we added three more

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

@@ -12,42 +12,48 @@ Introduction
 "
 Let's do the same level again:
 
-![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg)
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @VV{j}V           \\\\
+  S  @>>{k}> T       @>>{l}> U
+\\end{CD}
+$$
 
 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
+  Hint "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
+  ```
+  "
+  apply l
+  Hint "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!"
+  Branch
+    apply k
+    Hint "Looks like you got lost. \"Undo\" the last step."
   apply j
   apply h
+  Hint "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$)."
   exact p
 
-DisabledTactic «have» 
+DisabledTactic «have»
-
-Conclusion
-"
-
-"

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

@@ -13,47 +13,44 @@ Introduction
 In this level, our goal is to construct an implication, like in level 2.
 
 ```
-⊢ P → (Q → P)
+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
+this seems like a bit of a tall order. But let's give it a go.
-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
+  Hint "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
+  ```
+  "
   intro p
+  Hint "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
+  ```
+  "
   intro q
+  Hint "Now we have to prove $P$, but have a proof handy:
+
+  ```
+  exact {p}
+  ```
+  "
   exact p
 
 Conclusion
@@ -75,6 +72,6 @@ propositions, they would rather work with concrete ones such as Fermat's Last Th
 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. 
+Make sure you understand which one.
 
 "

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

@@ -13,35 +13,43 @@ 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`
+and `p : 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)).$$
-
 "
 
 Statement
-""
+"If $P$ and $Q$ and $R$ are true/false statements, then
+$$
+(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).
+$$"
     (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) := by
+  Hint "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 you can save time by starting
+  with `intro f h p`, which introduces three variables at once, although you'd
+  better then look at your tactic state to check that you called all those new
+  terms sensible things. "
   intro f
   intro h
   intro p
+  Hint "
+  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}`?
+  "
+  -- TODO: This hint needs strictness to make sense
+  -- Branch
+  --   apply f
+  --   Hint "Can you figure out what just happened? This is a little
+  --   `apply` easter egg. Why is it mathematically valid?"
+  --   Hint (hidden := true) "Note that there are two goals now, first you need to
+  --   provide an element in ${P}$ which you did not provide before."
   have j : Q → R := f p
   apply j
+  Hint (hidden := true) "Is there something you could apply? something of the form
+  `_ → Q`?"
   apply h
   exact p
-
-Conclusion
-"
-
-"

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

@@ -8,30 +8,20 @@ Title "(P → Q) → ((Q → R) → (P → R))"
 
 open MyNat
 
-Introduction
+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
+  Hint (hidden := true)"If you start with `intro hpq` and then `intro hqr`
+  the dust will clear a bit."
+  intro hpq
+  Hint (hidden := true) "Now try `intro hqr`."
+  intro hqr
+  Hint "So this level is really about showing transitivity of $\\implies$,
+  if you like that sort of language."
   intro p
   apply hqr
   apply hpq
   exact p
 
-Conclusion
-"
-
-"

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

@@ -1,7 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import NNG.MyNat.Theorems.Proposition
-
 
 Game "NNG"
 World "Proposition"
@@ -12,39 +10,63 @@ open MyNat
 
 Introduction
 "
-There is a false proposition `false`, with no proof. It is
+There is a false proposition `False`, with no proof. It is
-easy to check that $\\lnot Q$ is equivalent to $Q\\implies {\tt false}$,
+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},`
+In lean, this is true *by definition*, so you can view and treat `¬A` as an implication
-
+`A → 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]
+  Hint "However, if you would like to *see* `¬ Q` as `Q → False` because it makes you help
-  rw [not_iff_imp_false]
+  understanding, you can call
+
+  ```
+  repeat rw [Not]
+  ```
+
+  to get rid of the two occurences of `¬`. (`Not` is the name of `¬`)
+
+  I'm sure you can take it from there."
+  Branch
+    repeat rw [Not]
+    Hint "Note that this did not actually change anything internally. Once you're done, you
+    could delete the `rw [Not]` and your proof would still work."
+    intro f
+    intro h
+    intro p
+    -- TODO: It is somewhat cumbersome to have these hints several times.
+    -- defeq option in hints would help
+    Hint "Now you have to prove `False`. I guess that means you must be proving something by
+    contradiction. Or are you?"
+    Hint (hidden := true) "If you `apply {h}` the `False` magically dissappears again. Can you make
+    mathematical sense of these two steps?"
+    apply h
+    apply f
+    exact p
   intro f
   intro h
+  Hint "Note that `¬ P` should be read as `P → False`, so you can directly call `intro p` on it, even
+  though it might not look like an implication."
   intro p
+  Hint "Now you have to prove `False`. I guess that means you must be proving something by
+  contradiction. Or are you?"
+  Hint "If you're stuck, you could do `rw [Not] at {h}`. Maybe that helps."
+  Branch
+    rw [Not] at h
+    Hint "If you `apply {h}` the `False` magically dissappears again. Can you make
+    mathematical sense of these two steps?"
   apply h
   apply f
   exact p
 
-NewLemma not_iff_imp_false
+-- TODO: It this the right place? `repeat` is also introduced in `Multiplication World` so it might be
+-- nice to introduce it earlier on the `Function world`-branch.
+NewTactic «repeat»
+NewDefinition False Not
 
-Conclusion
+Conclusion "If you used `rw [Not]` or `rw [Not] at h` anywhere, go through your proof in
-"
+the \"Editor Mode\" and delete them all. Observe that your proof still works."
-
-"

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

@@ -1,6 +1,5 @@
 import NNG.Metadata
 import NNG.MyNat.Addition
-import NNG.MyNat.Theorems.Proposition
 
 Game "NNG"
 World "Proposition"
@@ -11,16 +10,16 @@ open MyNat
 
 Introduction
 "
-Now move onto advanced proposition world, where you will see
+In Lean3 there was a tactic `cc` which stands for \"congruence closure\"
-how to prove goals such as `P ∧ Q` ($P$ and $Q$), `P ∨ Q` ($P$ or $Q$),
+which could solve all these mazes automatically. Currently this tactic has
-`P ↔ Q` ($P\\iff Q$).
+not been ported to Lean4, but it will eventually be available!
-You will need to learn five more tactics: `split`, `cases`,
+
-`left`, `right`, and `exfalso`,
+For now, you can try to do this final level manually to apprechiate the use of such
-but they are all straightforward, and furthermore they are
+automatisation ;)
-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. 
 "
+-- TODO:
+-- "Lean's "congruence closure" tactic `cc` is good at mazes. You might want to try it now.
+-- Perhaps I should have mentioned it earlier."
 
 Statement
 "There is a way through the following maze."
@@ -28,10 +27,30 @@ Statement
     (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)
     (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := by
-  -- cc -- TODO: `cc` is not ported yet.
+  Hint (hidden := true) "You should, once again, start with `intro a`."
-  sorry
+  intro a
+  Hint "Use a mixture of `apply` and `have` calls to find your way through the maze."
+  apply f15
+  apply f11
+  apply f9
+  apply f8
+  apply f5
+  apply f2
+  apply f1
+  exact a
+
+-- TODO: Once `cc` is implemented,
+-- NewTactic cc
 
 Conclusion
 "
-
+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: `constructor`, `rcases`,
+`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.
 "

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

@@ -28,7 +28,7 @@ Statement
   Hint "In order to use the tactic `rfl` you can enter it above and hit \"Execute\"."
   rfl
 
-NewTactic rfl
+NewTactic rfl simp -- TODO
 NewDefinition MyNat
 
 Conclusion

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

@@ -56,9 +56,11 @@ Statement
   writing a small `←` (`\\l`, i.e. backslash + small letter L + space)
   before `h` like this: `rw [← h]`."
   Branch
-    rewrite [← h]
+    simp? -- TODO: `simp` should not make progress.
+  Branch
+    rw [← h]
     Hint (hidden := true) "Now both sides are identical…"
-  rewrite [h]
+  rw [h]
   Hint (hidden := true) "Now both sides are identical…"
   rfl
 

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

@@ -50,6 +50,8 @@ Statement
   rw [add_succ]
   Hint "Now you see a term of the form `… + 0`, so you can use `add_zero`."
   Hint (hidden := true) "Explicitely, type `rw [add_zero]`!"
+  Branch
+    simp? -- TODO
   rw [add_zero]
   Hint (hidden := true) "Finally both sides are identical."
   rfl

server/nng/NNG/Metadata.lean

@@ -1,5 +1,18 @@
 import GameServer.Commands
-import NNG.Doc.Tactics
+
-import NNG.Doc.Lemmas
+import NNG.MyNat.Definition
+
 import NNG.Doc.Definitions
-import NNG.Modifications.Tactics
+import NNG.Doc.Lemmas
+import NNG.Doc.Tactics
+
+import NNG.Tactic.Induction
+import NNG.Tactic.Rfl
+import NNG.Tactic.Rw
+import Std.Tactic.RCases
+import Mathlib.Tactic.Have
+import Mathlib.Tactic.LeftRight
+
+-- TODO: Why does this not work here??
+-- We do not want `simp` to be able to do anything unless we unlock it manually.
+attribute [-simp] MyNat.succ.injEq

server/nng/NNG/MyNat/AddCommMonoid.lean

@@ -0,0 +1,15 @@
+import NNG.Metadata
+import NNG.MyNat.Addition
+
+namespace MyNat
+
+-- TODO: Do we need these instances?
+
+-- instance addSemigroup : AddSemigroup ℕ :=
+-- {
+--   zero := 0
+
+-- }
+-- MyNat.addMonoid        -- (after level 2)
+-- MyNat.addCommSemigroup -- (after level 4)
+-- MyNat.addCommMonoid    -- (after level 4)

server/nng/NNG/MyNat/Addition.lean

@@ -14,13 +14,9 @@ instance : Add MyNat where
 /--
 This theorem proves that if you add zero to a MyNat you get back the same number.
 -/
-
 theorem add_zero (a : MyNat) : a + 0 = a := by rfl
 
 /--
 This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat.
 -/
 theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
-
--- TODO: testing. Remove me
-axiom zero_add (n : ℕ) : 0 + n = n

server/nng/NNG/MyNat/AdvAddition.lean

@@ -1,13 +1,14 @@
-import NNG.Levels.Addition.Level_6
+import NNG.MyNat.Addition
 
 namespace MyNat
-open MyNat
 
-axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
+attribute [-simp] MyNat.succ.injEq
+example (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
+  simp
+  sorry
 
-axiom zero_ne_succ (a : ℕ) : zero ≠ succ a
+axiom succ_inj {a b : ℕ} : succ a = succ b → a = b
 
-axiom add_right_cancel (a t b : ℕ) : a + t = b + t → a = b
+axiom zero_ne_succ (a : ℕ) : 0 ≠ succ a
 
-axiom add_left_cancel (a b c : ℕ) : a + b = a + c → b = c
 

server/nng/NNG/MyNat/Definition.lean

@@ -1,11 +1,8 @@
---import Mathlib.Tactic.Basic
---import Mathlib.Tactic.Cases 
-
 /-- Our copy of the natural numbers called `MyNat`. -/
 inductive MyNat where
 | zero : MyNat
 | succ : MyNat → MyNat
-deriving BEq, DecidableEq, Inhabited
+-- deriving BEq, DecidableEq, Inhabited
 
 @[inherit_doc]
 notation "ℕ" => MyNat
@@ -35,3 +32,7 @@ instance : ToString MyNat where
 theorem zero_eq_0 : MyNat.zero = 0 := rfl
 
 def one : MyNat := MyNat.succ 0
+
+-- TODO: Why does this not work here??
+-- We do not want `simp` to be able to do anything unless we unlock it manually.
+attribute [-simp] MyNat.succ.injEq

server/nng/NNG/MyNat/Multiplication.lean

@@ -14,6 +14,3 @@ instance : Mul MyNat where
 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

server/nng/NNG/MyNat/Power.lean

@@ -1,4 +1,5 @@
 import NNG.MyNat.Multiplication
+
 namespace MyNat
 open MyNat
 
@@ -11,11 +12,15 @@ instance : Pow ℕ ℕ where
 
 -- notation a ^ b := pow a b
 
-example : (1 : ℕ) ^ (1 : ℕ) = 1 := rfl
+-- Important note: This here is the real `rfl`, not the weaker game version
+
+example : (1 : ℕ) ^ 1 = 1 := by rfl
+
+theorem pow_zero (m : ℕ) : m ^ 0 = 1 := by rfl
 
-lemma pow_zero (m : ℕ) : m ^ (0 : ℕ) = 1 := rfl
+theorem pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := by rfl
 
-lemma pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := rfl
+def two_eq_succ_one : (2 : ℕ) = succ 1 := by rfl
 
 end MyNat
 

server/nng/NNG/MyNat/Theorems/Proposition.lean

@@ -1 +0,0 @@
-theorem not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := by simp only

server/nng/NNG/Tactic/Induction.lean

@@ -1,33 +1,9 @@
 import Mathlib.Lean.Expr.Basic
-import NNG.MyNat.Addition
 import Lean.Elab.Tactic.Basic
-
+import NNG.MyNat.Definition
-/-!
-# Modified `rw`
-
-Modify `rw` to work like `rewrite`.
-
-This is mainly a copy of the implementation of `rewrite` in Lean core.
--/
 
 namespace MyNat
 
-open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic
-
-/--
-Modified `rw` tactic. For this game, `rw` works exactly like `rewrite`.
--/
-syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic
-
-@[tactic MyNat.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
-  let cfg ← elabRewriteConfig stx[1]
-  let loc   := expandOptLocation stx[3]
-  withRWRulesSeq stx[0] stx[2] fun symm term => do
-    withLocation loc
-      (rewriteLocalDecl term symm · cfg)
-      (rewriteTarget term symm cfg)
-      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
-
 /-!
 # Modified `induction` tactic
 
@@ -103,29 +79,4 @@ elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+)
 end Lean.Parser.Tactic
 
 
-/-! # `rfl` tactic
-
-Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
--/
-
-namespace MyNat
-
-open Lean Meta Elab Tactic
-
--- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
-
-/-- Modified `rfl` tactic.
 
-`rfl` closes goals of the form `A = A`.
-
-Note that teh version for this game is somewhat weaker than the real one. -/
-syntax (name := rfl) "rfl" : tactic
-
-@[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
-  liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure []
-
--- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
---   liftMetaTactic fun mvarId => do mvarId.refl; pure []
--- (with_reducible rfl)
-
-end MyNat

server/nng/NNG/Tactic/Rfl.lean

@@ -0,0 +1,31 @@
+import Mathlib.Lean.Expr.Basic
+import Lean.Elab.Tactic.Basic
+
+/-! # `rfl` tactic
+
+Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
+-/
+
+namespace MyNat
+
+open Lean Meta Elab Tactic
+
+-- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
+
+/-- Modified `rfl` tactic.
+
+`rfl` closes goals of the form `A = A`.
+
+Note that teh version for this game is somewhat weaker than the real one. -/
+syntax (name := rfl) "rfl" : tactic
+
+@[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
+  liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure []
+-- TODO: `rfl` should be able to prove `R ↔ R`!
+
+
+-- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
+--   liftMetaTactic fun mvarId => do mvarId.refl; pure []
+-- (with_reducible rfl)
+
+end MyNat

server/nng/NNG/Tactic/Rw.lean

@@ -0,0 +1,28 @@
+import Mathlib.Lean.Expr.Basic
+import Lean.Elab.Tactic.Basic
+
+/-!
+# Modified `rw`
+
+Modify `rw` to work like `rewrite`.
+
+This is mainly a copy of the implementation of `rewrite` in Lean core.
+-/
+
+namespace MyNat
+
+open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic
+
+/--
+Modified `rw` tactic. For this game, `rw` works exactly like `rewrite`.
+-/
+syntax (name := rewriteSeq) "rw" (config)? rwRuleSeq (location)? : tactic
+
+@[tactic MyNat.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
+  let cfg ← elabRewriteConfig stx[1]
+  let loc   := expandOptLocation stx[3]
+  withRWRulesSeq stx[0] stx[2] fun symm term => do
+    withLocation loc
+      (rewriteLocalDecl term symm · cfg)
+      (rewriteTarget term symm cfg)
+      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")

server/nng/NNG/Tactic/Simp.lean

@@ -0,0 +1,51 @@
+import Mathlib.Lean.Expr.Basic
+import Lean.Elab.Tactic.Basic
+import NNG.Tactic.Rfl
+
+/-! # `simp` tactic
+
+Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
+-/
+
+namespace MyNat
+
+open Lean Meta Elab Tactic
+
+-- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
+
+/--
+The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
+non-dependent hypotheses. It has many variants:
+- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
+- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
+  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.
+  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with
+  `f` are used. This provides a convenient way to unfold `f`.
+- `simp [*]` simplifies the main goal target using the lemmas tagged with the
+  attribute `[simp]` and all hypotheses.
+- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
+- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
+  with the attribute `[simp]`, but removes the ones named `idᵢ`.
+- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
+  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
+  `hᵢ` is introduced, but the old one remains in the local context.
+- `simp at *` simplifies all the hypotheses and the target.
+- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
+  other hypotheses.
+-/
+syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic
+
+/-
+  "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
+-/
+@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
+  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+  let usedSimps ← dischargeWrapper.with fun discharge? =>
+    simpLocation ctx discharge? (expandOptLocation stx[5])
+  if tactic.simp.trace.get (← getOptions) then
+    traceSimpCall stx usedSimps
+
+end MyNat
+
+