adding conclusions

Game/Levels/Division/Level_1.lean

@@ -11,9 +11,9 @@ namespace MyNat
 
 Introduction
 "
-  In this section, we will prove that 1 ∣ n for all n ∈ ℕ. `a | b` is
-  shorthand for `there existsw a number c such that `b = c * a``, so
-  you should be looking to use the `use' tactic in these kinds of proof.
+  In this level, we will prove that 1 ∣ n for all n ∈ ℕ. `a | b` is
+  shorthand for `there exists a number c such that `b = c * a`, because of
+  `exists`, the use statment will be useful here.
 
 "
 
@@ -28,3 +28,9 @@ Statement one_dvd
   use n
   rw [one_mul]
   rfl
+
+
+Conclusion
+"
+  Congratulations! You have proven your first theorem about division.
+"

Game/Levels/Division/Level_2.lean

@@ -10,8 +10,9 @@ namespace MyNat
 
 Introduction
 "
-  In this section, we will prove that n ∣ n for any natural number n. In other words, 'divides' is
-  a reflexive relation on the natural numebrs.
+  In this level, we will prove that n ∣ n for any natural number n.
+  In other words, 'divides' is a reflexive relation on the natural
+  numebrs.
 "
 
 LemmaDoc MyNat.dvd_refl as "dvd_refl" in "∣" "
@@ -20,7 +21,13 @@ LemmaDoc MyNat.dvd_refl as "dvd_refl" in "∣" "
 
 Statement dvd_refl
     (n : ℕ) : n ∣ n := by
-  Hint "This is true because `n = n * 1`"
+  Hint "This is true because `n = n * 1`."
   use 1
   rw [mul_one]
   rfl
+
+Conclusion
+"
+  Well Done, this was the first step in proving that `∣` is a partial order. We
+  will prove the other properties in the next few levels.
+"

Game/Levels/Division/Level_3.lean

@@ -11,7 +11,8 @@ namespace MyNat
 
 Introduction
 "
-
+  In this level, we will prove that `divides` is antisymmetric. i.e the
+  only way that we can have `a | b` and `b | a ` is if a = b.
 "
 
 LemmaDoc MyNat.dvd_antisymm as "dvd_antisymm" in "∣" "
@@ -20,10 +21,9 @@ LemmaDoc MyNat.dvd_antisymm as "dvd_antisymm" in "∣" "
 
 Statement dvd_antisymm
     (a b : ℕ) (h1 : a ∣ b) (h2 : b ∣ a): a = b := by
-  Hint "You will need to expand what `h1` and `h2` actually mean. You may find `rcases` helpful"
+  Hint "You will need to expand what `h1` and `h2` actually mean. You may find `rcases` helpful."
   rcases h1 with ⟨c, hc⟩
   rcases h2 with ⟨d, hd⟩
-  -- need to cancel b's:
   rw [hd] at hc
   by_cases hb : b = 0
   · rw [hb] at hd

Game/Levels/Division/Level_4.lean

@@ -8,8 +8,9 @@ namespace MyNat
 
 Introduction
 "
-  In this section, we will prove that ∣ is transitive. This will complete the proof that ∣ is a
-  partial order on ℕ.
+  In this level, we will prove that ∣ is transitive. That is, if
+  `a ∣ b` and `b ∣ c`, then `a ∣c ` This will complete the proof
+  that ∣ is a partial order on ℕ.
 "
 
 LemmaDoc MyNat.dvd_trans as "dvd_trans" in "∣" "
@@ -21,15 +22,18 @@ Statement dvd_trans
   Hint "Here, like the last level, you may find `rcases` helpful."
   rcases hbc with ⟨m, hm⟩
   rcases hab with ⟨n, rfl⟩
-  -- b = na, c = mb
-  -- c = mna
-  Hint "Now, since we are looking show `a ∣ c`, which is an existience hypothesis, a `use` tactic
-  would be a good choice."
+  Hint "Now, since we are looking show `a ∣ c`, which is an existience hypothesis, the `use`
+  tactic would be a good choice."
   use (m * n)
   Hint "Now the goal is clear, its just a case of finding the correct rewrites."
   rw [hm]
   rw [mul_assoc]
   rw [mul_comm n m]
   rfl
 
+Conclusion
+"
+  Great work. We have succedfully proven that `∣` is a partial order on ℕ.
+"
+
 LemmaTab "∣"

Game/Levels/Division/Level_5.lean

@@ -10,7 +10,7 @@ namespace MyNat
 
 Introduction
 "
-  In this section, we will prove that if d ∣ a, then d ∣ ab.
+  In this level, we will prove that if d ∣ a, then d ∣ ab.
 "
 
 LemmaDoc MyNat.dvd_mul_right as "dvd_mul_right" in "∣" "

Game/Levels/Division/Level_6.lean

@@ -25,7 +25,7 @@ Statement dvd_add_right
   cases d with d
   · use 0
     rw [zero_mul] at *
-    rw[zero_mul] at he
+    rw [zero_mul] at he
     rw [zero_add] at he
     exact he
   · have : 1 ≤ succ d := by sorry

Game/Levels/Hard/level_1.lean

@@ -10,7 +10,7 @@ namespace MyNat
 
 Introduction
 "
-  We beign with a problem which has been proven, Fermat's Last Theorem.
+  We beign with a problem which has been proven, but not in Lean, Fermat's Last Theorem.
 "
 
 LemmaDoc MyNat.FLT as "FLT" in "Hard" "
@@ -22,5 +22,10 @@ Statement FLT
   sorry
 
 
+Conclusion
+"
+  Well that was impressive, you shoud wtite a paper about it.
+"
+
 
 end MyNat

Game/Levels/Hard/level_3.lean

@@ -22,3 +22,4 @@ LemmaDoc MyNat.Golbach as "Golbach" in "Hard" "
 
 Statement Golbach : ∀ (n : ℕ), n ≥ 2 → ∃ (a b : ℕ), (Prime a) ∧ (Prime b) ∧ (n = a + b) := by
   sorry
+

Game/Levels/Prime/Level_1.lean

@@ -24,11 +24,15 @@ LemmaDoc MyNat.prime_two as "prime_two" in "Prime" "
 
 Statement prime_two :
   Prime 2 := by
+  Hint "You may want to know what `Prime 2` actually means. For this, you can use
+  `unfold Prime`."
   unfold Prime
+  Hint "Use `constructor` to split up the `∧` statment into two goals."
   constructor
   use 0
   rw [add_zero]
   rfl
+  Hint "You have done the easy half, now for the tough part."
   intros a ha
   have : a ≤ 2 := by exact dvd_two_leq_two a ha
   have h : a = 0 ∨ a = 1 ∨ a = 2 := by exact le_two a this
@@ -39,4 +43,5 @@ Statement prime_two :
     cases hb
   · exact h
 
+
 end MyNat