tutorial revamped

Game/Levels/Tutorial/L06twoaddone.lean

@@ -1,6 +1,6 @@
 import Game.Metadata
 import Game.MyNat.Addition
-import Game.Levels.Tutorial.L03three_eq_sss0
+import Game.Levels.Tutorial.L05add_succ
 World "Tutorial"
 Level 6
 Title "2+1=3"
@@ -14,12 +14,9 @@ namespace MyNat
 
 /-- $2+2=4$. -/
 Statement two_add_one_eq_three : (2 : ℕ) + 1 = 3 := by
-  Hint (hidden := true) "`rw [one_eq_succ_zero]` unlocks `add_succ`"
-  rw [one_eq_succ_zero]
-  Hint (hidden := true) "Now you can `rw [add_succ]`"
-  rw [add_succ]
-  rw [add_zero]
+  Hint (hidden := true) "`rw [one_eq_succ_zero]` unlocks `add_succ` but `succ_eq_add_one` is even more useful"
   rw [three_eq_succ_two]
+  rw [succ_eq_add_one]
   rfl
 
 LemmaDoc MyNat.two_add_one_eq_three as "two_add_one_eq_three" in "Add"
@@ -30,6 +27,8 @@ LemmaTab "Add"
 
 
 Conclusion
-"
+" Did you spot the two-rewrite proof? `rw [three_eq_succ_two, succ_eq_add_one]`
+and then `rfl`?
+
   Do you think you're ready for `2 + 2 = 4`?
 "

Game/Levels/Tutorial/L07twoaddtwo.lean

@@ -31,13 +31,41 @@ Statement : (2 : ℕ) + 2 = 4 := by
   rw [four_eq_succ_three]
   rfl
 
+/-- $2+2=4$. -/
+Statement foo : (2 : ℕ) + 2 = 4 := by
+  rw [two_eq_succ_one, add_succ, one_eq_succ_zero, add_succ, add_zero, four_eq_succ_three,
+    three_eq_succ_two, two_eq_succ_one, one_eq_succ_zero]
+  rfl
+
 Conclusion
 "
+
+  Here are some example proofs. Copy and paste them into editor mode if you want
+  to inspect how they work.
+
+```
+  nth_rewrite 2 [two_eq_succ_one]
+  rw [add_succ]
+  rw [two_add_one_eq_three]
+  rw [four_eq_succ_three]
+  rfl
+```
+
+```
+  rw [four_eq_succ_three]
+  rw [← two_add_one_eq_three]
+  rw [← add_succ]
+  rw [← two_eq_succ_one]
+  rfl
+```
+
+```
+  rw [two_eq_succ_one, add_succ, one_eq_succ_zero, add_succ, add_zero, four_eq_succ_three,
+    three_eq_succ_two, two_eq_succ_one, one_eq_succ_zero]
+  rfl
+```
+
+
 You have finished tutorial world! If you're happy, let's move onto Addition World,
 and learn about proof by induction.
-
-## Inspection time
-
-If you want to examine your proofs, toggle \"Editor mode\" and click somewhere
-inside the proof to see the state of Lean's brain at that point.
 "

Game/Levels/Tutorial/simp_doc_being_moved.txt

@@ -0,0 +1,14 @@
+
+TacticDoc simp "The simplifier. `rw` on steroids.
+
+A bunch of lemmas like `add_zero : ∀ a, a + 0 = a`
+are tagged with the `@[simp]` tag. If the `simp` tactic
+is run by the user, the simplifier will try and rewrite
+as many of the lemmas tagged `@[simp]` as it can.
+
+`simp` is a *finishing tactic*. After you run `simp`,
+the goal should be closed. If it is not, it is best
+practice to write `simp?` instead and then replace the
+output with the appropriate `simp only` call. Inappropriate
+use of `simp` can make for very slow code.
+"