NewLemma -> NewTheorem (global) and "x" -> /-- x -/ (in tutorial and …

…addition)

Game/Levels/Addition/L01zero_add.lean

@@ -30,11 +30,13 @@ will ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because
 See if you can do your first induction proof in Lean.
 "
 
-TheoremDoc MyNat.zero_add as "zero_add" in "+" "
+/--
 `zero_add x` is the proof of `0 + x = x`.
 
 `zero_add` is a `simp` lemma, because replacing `0 + x` by `x`
-is almost always what you want to do if you're simplifying an expression."
+is almost always what you want to do if you're simplifying an expression.
+-/
+TheoremDoc MyNat.zero_add as "zero_add" in "+"
 
 /-- For all natural numbers $n$, we have $0 + n = n$. -/
 Statement zero_add (n : ℕ) : 0 + n = n := by
@@ -61,7 +63,7 @@ Statement zero_add (n : ℕ) : 0 + n = n := by
 
 attribute [simp] zero_add
 
-TacticDoc induction "
+/--
 ## Summary
 
 If `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`
@@ -96,4 +98,5 @@ Conclusion
   `add_zero` and `zero_add`!
 
   Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`.
-"
+-/
+TacticDoc induction

Game/Levels/Addition/L02succ_add.lean

@@ -16,8 +16,10 @@ we have the problem that we are adding `b` to things, so we need
 to use induction to split into the cases where `b = 0` and `b` is a successor.
 "
 
+/--
+`succ_add a b` is a proof that `succ a + b = succ (a + b)`.
+-/
 TheoremDoc MyNat.succ_add as "succ_add" in "+"
-"`succ_add a b` is a proof that `succ a + b = succ (a + b)`."
 
 /--
 For all natural numbers $a, b$, we have

Game/Levels/Addition/L03add_comm.lean

@@ -15,8 +15,8 @@ Look in your inventory to see the proofs you have available.
 These should be enough.
 "
 
+/-- `add_comm x y` is a proof of `x + y = y + x`. -/
 TheoremDoc MyNat.add_comm as "add_comm" in "+"
-"`add_comm x y` is a proof of `x + y = y + x`."
 
 /-- On the set of natural numbers, addition is commutative.
 In other words, if `a` and `b` are arbitrary natural numbers, then

Game/Levels/Addition/L04add_assoc.lean

@@ -19,10 +19,13 @@ Introduction
   That's true, but we didn't prove it yet. Let's prove it now by induction.
 "
 
-TheoremDoc MyNat.add_assoc as "add_assoc" in "+" "`add_assoc a b c` is a proof
+/--
+`add_assoc a b c` is a proof
 that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints
 as `a + b + c`, because the notation for addition is defined to be left
-associative. "
+associative.
+-/
+TheoremDoc MyNat.add_assoc as "add_assoc" in "+"
 
 /-- On the set of natural numbers, addition is associative.
 In other words, if $a, b$ and $c$ are arbitrary natural numbers, we have

Game/Levels/Addition/L05add_right_comm.lean

@@ -23,11 +23,12 @@ will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`
 will only do rewrites of the form `b + c = c + b`.
 "
 
-TheoremDoc MyNat.add_right_comm as "add_right_comm" in "+"
-"`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`.
+/-- `add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`
 
 In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed
-as `a + b + c = a + c + b`."
+as `a + b + c = a + c + b`.
+-/
+TheoremDoc MyNat.add_right_comm as "add_right_comm" in "+"
 
 /-- If $a, b$ and $c$ are arbitrary natural numbers, we have
 $(a + b) + c = (a + c) + b$. -/

Game/Levels/Algorithm/L05pred.lean

@@ -35,7 +35,7 @@ TheoremDoc MyNat.pred_succ as "pred_succ" in "Peano"
 `pred_succ n` is a proof of `pred (succ n) = n`.
 "
 
-NewLemma MyNat.pred_succ
+NewTheorem MyNat.pred_succ
 
 /-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/
 Statement (a b : ℕ) (h : succ a = succ b) : a = b := by

Game/Levels/Algorithm/L06is_zero.lean

@@ -42,7 +42,7 @@ TheoremDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Peano"
 `succ_ne_zero a` is a proof of `succ a ≠ 0`.
 "
 
-NewLemma MyNat.is_zero_zero MyNat.is_zero_succ
+NewTheorem MyNat.is_zero_zero MyNat.is_zero_succ
 
 TacticDoc triv "
 # Summary

Game/Levels/Implication/L04succ_inj.lean

@@ -47,7 +47,7 @@ in Lean it can be proved using `pred`, a mathematically
 pathological function.
 "
 
-NewLemma MyNat.succ_inj
+NewTheorem MyNat.succ_inj
 
 /-- If $x+1=4$ then $x=3$. -/
 Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by

Game/Levels/Implication/L09zero_ne_succ.lean

@@ -18,7 +18,7 @@ Here `False` is a generic false statement. This means that
 you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`.
 "
 
-NewLemma MyNat.zero_ne_succ
+NewTheorem MyNat.zero_ne_succ
 
 Introduction "
 As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to

Game/Levels/LessOrEqual/Level_1.lean

@@ -67,7 +67,7 @@ Statement --one_add_le_self
   rfl
 
 NewTactic use -- ring
-NewLemma MyNat.le_iff_exists_add
+NewTheorem MyNat.le_iff_exists_add
 TheoremTab "Inequality"
 
 Conclusion "Now look at your proof. We're going to remove a line.

Game/Levels/Multiplication/L01mul_one.lean

@@ -42,7 +42,7 @@ TheoremDoc MyNat.mul_succ as "mul_succ" in "*"
 `mul_succ a b` is the proof that `a * succ b = a * b + a`.
 "
 
-NewLemma MyNat.mul_zero MyNat.mul_succ
+NewTheorem MyNat.mul_zero MyNat.mul_succ
 
 TheoremDoc MyNat.mul_one as "mul_one" in "*" "
 `mul_one m` is the proof that `m * 1 = m`.

Game/Levels/Power/L01zero_pow_zero.lean

@@ -34,7 +34,7 @@ TheoremDoc MyNat.pow_zero as "pow_zero" in "^" "
 defining exponentiation in this game.
 "
 
-NewLemma MyNat.pow_zero
+NewTheorem MyNat.pow_zero
 
 TheoremDoc MyNat.zero_pow_zero as "zero_pow_zero" in "^" "
 Mathematicians sometimes argue that `0 ^ 0 = 0` is also

Game/Levels/Power/L02zero_pow_succ.lean

@@ -14,7 +14,7 @@ TheoremDoc MyNat.pow_succ as "pow_succ" in "^" "
 two axioms defining exponentiation in this game.
 "
 
-NewLemma MyNat.pow_succ
+NewTheorem MyNat.pow_succ
 
 TheoremDoc MyNat.zero_pow_succ as "zero_pow_succ" in "^" "
 Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if

Game/Levels/Tutorial/L03two_eq_ss0.lean

@@ -36,7 +36,7 @@ TheoremDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "012"
 "`four_eq_succ_three` is a proof of `4 = succ 3`."
 
 NewDefinition MyNat
-NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two
+NewTheorem MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two
   MyNat.four_eq_succ_three
 
 Introduction

Game/Levels/Tutorial/L05add_zero.lean

@@ -24,8 +24,8 @@ NewDefinition Add
 
 TheoremTab "+"
 
-TheoremDoc MyNat.add_zero as "add_zero" in "+"
-"`add_zero a` is a proof that `a + 0 = a`.
+/--
+`add_zero a` is a proof that `a + 0 = a`.
 
 ## Summary
 
@@ -43,10 +43,12 @@ to input.
 A mathematician sometimes thinks of `add_zero`
 as \"one thing\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.
 This is just another way of saying that it's a function which
-can eat any number n and will return a proof that `n + 0 = n`."
+can eat any number n and will return a proof that `n + 0 = n`.
+-/
+TheoremDoc MyNat.add_zero as "add_zero" in "+"
 
 
-TacticDoc «repeat» "
+/--
 ## Summary
 
 `repeat t` repeatedly applies the tactic `t`
@@ -59,9 +61,10 @@ tactic, it just speeds things up sometimes.
 `a + 0 + (0 + (0 + 0)) = b + 0 + 0`
 into the goal
 `a = b`.
-"
+-/
+TacticDoc «repeat»
 
-NewLemma MyNat.add_zero
+NewTheorem MyNat.add_zero
 
 Introduction
 "

Game/Levels/Tutorial/L07add_succ.lean

@@ -10,10 +10,10 @@ TheoremTab "012"
 
 namespace MyNat
 
+/-- `add_succ a b` is the proof of `a + succ b = succ (a + b)`. -/
 TheoremDoc MyNat.add_succ as "add_succ" in "+"
-"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
 
-NewLemma MyNat.add_succ
+NewTheorem MyNat.add_succ
 
 TheoremDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "+"
 "`succ_eq_add_one n` is the proof that `succ n = n + 1`."