use cases instead of tauto (so we can introduce tauto elsewhere)

Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean

@@ -10,46 +10,24 @@ LemmaTab "Peano"
 namespace MyNat
 
 Introduction
-" We have still not proved that if `a + b = 0` then `a = 0` and also `b = 0`. Let's finish this
+" 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
+## A new tactic: `cases`
 
-If you have a hypothesis `h : False` then you are done, because a false statement implies
-any statement. You can use the `tauto` tactic to finish your proof.
+The `cases` tactic will split an object or hypothesis up into the possible ways
+that it could have been created.
 
-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.
+For example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,
+but 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. There are two ways to make
+a number: it's either zero or a successor. So you will end up with two goals, one
+with `b = 0` and one with `b = succ d`.
 
-"
-
-TacticDoc tauto "
-# Summary
-
-The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by
-truth tables).
-
-## Example
-
-If you have `False` as a hypothesis, then `tauto` will solve
-the goal. This is because a false hypothesis implies any hypothesis.
-
-## Example
+Another example: if you have a hypothesis `h : False` then you are done, because a false statement implies
+any statement. Here `cases h` will close the goal, because there are *no* ways to
+make a proof of `False`! So you will end up with no goals, meaning you have proved everything.
 
-If your goal is `True`, then `tauto` will solve the goal.
-
-## Example
-
-If you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will
-solve the goal because it can prove `False` from your hypotheses, and thus
-prove the goal (as `False` implies anything).
-
-## Example
-
-If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then
-`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.
-If you switch the goal and hypothesis in this example, `tauto` would solve it too.
 "
 
 TacticDoc cases "
@@ -63,12 +41,6 @@ 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`
@@ -79,8 +51,20 @@ or a successor.
 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`.
+
+## Example
+
+If `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,
+because there are no ways to make a proof of `False`! And if you have no goals left,
+you have finished the level.
+
+## 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`.
 "
-NewTactic tauto cases
+NewTactic cases
 
 LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in "+" "
   A proof that $a+b=0 \\implies a=0$.
@@ -91,7 +75,7 @@ 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,
+  Hint "Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,
   so start with `cases b with d`."
   cases b with d
   intro h
@@ -101,6 +85,6 @@ Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
   rw [add_succ] at h
   symm at h
   apply zero_ne_succ at h
-  tauto
+  cases h
 
 Conclusion "Well done!"

Game/Levels/Algorithm/L06is_zero.lean

@@ -22,7 +22,7 @@ and `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`,
 Last Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have
 this opposite version too, which can be proved in the same way.
 
-If you can turn your goal into `True`, then the `tauto` tactic will solve it.
+If you can turn your goal into `True`, then the `triv` tactic will solve it.
 "
 
 LemmaDoc MyNat.is_zero_zero as "is_zero_zero" in "Peano"
@@ -42,6 +42,15 @@ LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Peano"
 
 NewLemma MyNat.is_zero_zero MyNat.is_zero_succ
 
+TacticDoc triv "
+# Summary
+
+`triv` will solve any goal of the form `True`.
+
+"
+
+NewTactic triv
+
 /-- $\operatorname{succ}(a) \neq 0$. -/
 Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   Hint "Start with `intro h` (remembering that `X ≠ Y` is just notation
@@ -52,4 +61,4 @@ Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   rw [← is_zero_succ a]
   rw [h]
   rw [is_zero_zero]
-  tauto
+  triv

Game/Levels/Implication/L11two_add_two_ne_five.lean

@@ -33,7 +33,8 @@ exact h
 
 Even though Lean is a theorem prover, right now it's pretty clear that we have not
 developed enough material to make it an adequate calculator. In Algorithm
-World we will develop machinery which makes questions like this much easier,
-and goals like $20 + 20 ≠ 41$ feasible. But to get to Algorithm World you'll
-have to make it through Advanced Addition World. Click \"Leave World\" to
-go there."
+World, a more computer-sciency world, we will develop machinery which makes
+questions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.
+Alternatively you can do more mathematics in Advanced Addition World, where we prove
+the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and
+decide your route."