edits in LE world

Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean

@@ -12,14 +12,49 @@ Introduction
 " We have still not proved that if `a + b = 0` then `a = 0` and `b = 0`. Let's finish this
 world by proving one of these in this level, and the other in the next.
 
+## Two new tactics
+
 If you have a hypothesis `h : False` then you are done, because a false statement implies
 any statement. You can use the `contradiction` tactic to finish your proof.
+
+Sometimes you just want to deal with the two cases `b = 0` and `b = succ d` separately,
+and don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.
+In this situation you can use `cases b with d` instead.
+
 "
 
 TacticDoc contradiction "
 The `contradiction` tactic will solve any goal, if you have a hypothesis `h : False`.
 "
-NewTactic contradiction
+TacticDoc cases "
+## Summary
+
+If `n` is a number, then `cases n with d` will break the goal into two goals,
+one with `n = 0` and the other with `n = succ d`.
+
+If `h` is a proof (for example a hypothesis), then `cases h with...` will break the
+proof up into the pieces used to prove it.
+
+## Example
+
+If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`
+and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is
+`∃ c, b = a + c`.
+
+## Example
+
+If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,
+one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This
+corresponds to the mathematical idea that every natural number is either `0`
+or a successor.
+
+## Example
+
+If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal
+into two goals, one with a hypothesis `hp : P` and the other with a
+hypothesis `hq : Q`.
+"
+NewTactic contradiction cases
 
 LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in "Add" "
   A proof that $a+b=0 \\implies a=0$.
@@ -30,14 +65,14 @@ LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in
 
 /-- If $a+b=0$ then $a=0$. -/
 Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
-  Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately, so start with `induction b with d hd`
+  Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately, but so start with `induction b with d hd`
   but just ignore the inductive hypothesis in the `succ d` case :-)"
-  induction b with d _ -- don't even both naming inductive hypo
+  cases b with d -- zero not 0
   intro h
+  change a + 0 = 0 at h -- **TODO** fix this
   rw [add_zero] at h
   exact h
   intro h
---  clear hd -- **TODO** remove after `cases`
   rw [add_succ] at h
   symm at h
   apply zero_ne_succ at h

Game/Levels/LessOrEqual/L03le_succ_self.lean

@@ -6,6 +6,10 @@ Title "x ≤ succ x"
 
 namespace MyNat
 
+LemmaDoc MyNat.le_succ_self as "le_succ_self" in "≤" "
+`le_succ_self x` is a proof that `x ≤ succ x`.
+"
+
 /-- If $x$ is a number, then $x \\le \\mathoperator{succ}(x)$. -/
 Statement le_succ_self (x : ℕ) : x ≤ succ x := by
   use 1

Game/Levels/LessOrEqual/L04le_zero.lean

@@ -6,13 +6,17 @@ Title "x ≤ 0 → x = 0"
 
 namespace MyNat
 
+LemmaDoc MyNat.le_zero as "le_zero" in "≤" "
+`le_zero x` is a proof of `x ≤ 0 → x = 0`.
+"
+
 Introduction "
 In this level, our inequality is a *hypothesis*. We have not seen this before.
 
 "
 /-- If $x \leq 0$, then $x=0$. -/
 Statement le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by
-  cases' hx with y hy
+  cases hx with y hy
   symm at hy
   apply eq_zero_of_add_right_eq_zero at hy
   exact hy