Add new left/right tactic practice world plus tactic docs

Game/Levels/LessOrEqual.lean

@@ -5,7 +5,8 @@ import Game.Levels.LessOrEqual.L03le_succ_self
 import Game.Levels.LessOrEqual.L04le_trans
 import Game.Levels.LessOrEqual.L05le_zero
 import Game.Levels.LessOrEqual.L06le_antisymm
-import Game.Levels.LessOrEqual.L07le_total
+import Game.Levels.LessOrEqual.L07or_symm
+import Game.Levels.LessOrEqual.L08le_total
 
 World "LessOrEqual"
 Title "≤ World"

Game/Levels/LessOrEqual/L06le_antisymm.lean

@@ -47,6 +47,7 @@ rfl
 A passing mathematician remarks that with antisymmetry as well,
 you have proved that `≤` is a *partial order* on `ℕ`.
 
-The next level, the boss level of this world, is to prove
-that `≤` is a total order.
+The boss level of this world is to prove
+that `≤` is a total order. Let's learn two more easy tactics
+first.
 "

Game/Levels/LessOrEqual/L07or_symm.lean

@@ -0,0 +1,72 @@
+import Game.Levels.LessOrEqual.L06le_antisymm
+
+World "LessOrEqual"
+Level 7
+Title "Dealing with `or`"
+
+namespace MyNat
+
+LemmaTab "≤"
+
+TacticDoc left "
+# Summary
+The `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.
+Use it when your hypotheses guarantee that the reason that `P ∨ Q`
+is true is because in fact `P` is true.
+
+Internally this tactic is just `apply`ing a theorem
+saying that $P\\implies P\\lor Q.$
+
+Note that this tactic can turn a solvable goal into an unsolvable
+one.
+"
+
+TacticDoc right "
+# Summary
+The `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.
+Use it when your hypotheses guarantee that the reason that `P ∨ Q`
+is true is because in fact `Q` is true.
+
+Internally this tactic is just `apply`ing a theorem
+saying that $Q\\implies P\\lor Q.$
+
+Note that this tactic can turn a solvable goal into an unsolvable
+one.
+"
+
+NewTactic left right
+
+Introduction "
+Totality of `≤` is the last level in this world. It says that
+if `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.
+But we haven't talked about `or` at all. Here's a run-through.
+
+1) The notation for \"or\" is `∨`. You won't need to type it, but you can
+type it with `\\or`.
+
+2) If you have an \"or\" statement in the *goal*, then two tactics made
+progress: `left` and `right`. But don't choose a direction unless your
+hypotheses guarantee that it's the correct one.
+
+3) If you have an \"or\" statement as a *hypothesis* `h`, then
+`cases h with h1 h2` will create two goals, one where you went left,
+and the other where you went right.
+"
+
+/-- If $x=37$ or $y=42$, then $y=42$ or $x=37$. -/
+Statement (x y : ℕ) (h : x = 37 ∨ y = 42) : y = 42 ∨ x = 37 := by
+  Hint "We don't know whether to go left or right yet. So start with `cases h with hx hy`."
+  cases h with hx hy
+  Hint "Now we can prove the `or` statement by proving the statement on the right,
+  so use the `right` tactic."
+  right
+  exact hx
+  Hint (hidden := true) "This time, use the `left` tactic."
+  left
+  exact hy
+
+LemmaTab "≤"
+
+Conclusion "
+Ready for the final boss of this world?
+"

Game/Levels/LessOrEqual/L08le_total.lean

@@ -0,0 +1,56 @@
+import Game.Levels.LessOrEqual.L07or_symm
+
+World "LessOrEqual"
+Level 8
+Title "x ≤ y or y ≤ x"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_total as "le_total" in "≤" "
+`le_total x y` is a proof that `x ≤ y` or `y ≤ x`.
+"
+
+NewLemma MyNat.le_total
+
+Introduction "
+This is I think the toughest level yet.
+"
+
+/-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
+Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
+  Hint (hidden := true) "Start with `induction y with d hd`."
+  induction y with d hd
+  right
+  exact zero_le x
+  Hint (hidden := true) "Try `cases hd with h1 h2`."
+  cases hd with h1 h2
+  left
+  cases h1 with e h1
+  rw [h1]
+  use e + 1
+  rw [succ_eq_add_one, add_assoc]
+  rfl
+  Hint (hidden := true) "Now `cases h2 with e h2`."
+  cases h2 with e h2
+  Hint (hidden := true) "You still don't know which way to go, so do `cases e with a`."
+  cases e with a
+  rw [h2]
+  left
+  rw [add_zero]
+  use 1
+  exact succ_eq_add_one d
+  right
+  use a
+  rw [add_succ] at h2
+  rw [succ_add]
+  exact h2
+
+LemmaTab "≤"
+
+Conclusion "
+A passing mathematician remarks that with you've just proved that `ℕ` is totally
+ordered.
+"
+
+-- **TODO** add "if you want to prove it's a totally ordered ring, go
+-- to advanced mult world"