From 18e0aec41dc63b71c774a40fbb551cedd7b209dc Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 18 Mar 2024 16:40:56 +0100
Subject: [PATCH] use variable escaping in hints in LE-world

---
 Game/Levels/LessOrEqual/L01le_refl.lean  |  2 +-
 Game/Levels/LessOrEqual/L04le_trans.lean |  6 +++---
 Game/Levels/LessOrEqual/L07or_symm.lean  |  2 +-
 Game/Levels/LessOrEqual/L08le_total.lean | 16 ++++++++--------
 4 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/Game/Levels/LessOrEqual/L01le_refl.lean b/Game/Levels/LessOrEqual/L01le_refl.lean
index ae41bb4..a27e6b5 100644
--- a/Game/Levels/LessOrEqual/L01le_refl.lean
+++ b/Game/Levels/LessOrEqual/L01le_refl.lean
@@ -58,7 +58,7 @@ TheoremDoc MyNat.le_refl as "le_refl" in "≤"
 
 /-- If $x$ is a number, then $x \le x$. -/
 Statement le_refl (x : ℕ) : x ≤ x := by
-  Hint "The reason `x ≤ x` is because `x = x + 0`.
+  Hint "The reason `{x} ≤ {x}` is because `{x} = {x} + 0`.
   So you should start this proof with `use 0`."
   use 0
   Hint "You can probably take it from here."
diff --git a/Game/Levels/LessOrEqual/L04le_trans.lean b/Game/Levels/LessOrEqual/L04le_trans.lean
index 3d9d1f3..0617b17 100644
--- a/Game/Levels/LessOrEqual/L04le_trans.lean
+++ b/Game/Levels/LessOrEqual/L04le_trans.lean
@@ -30,10 +30,10 @@ The `cases` tactic can be used to take `hxy` apart.
 
 /-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
 Statement le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
-  Hint "Start with `cases hxy with a ha`."
+  Hint "Start with `cases {hxy} with a ha`."
   cases hxy with a ha
-  Hint "Now `ha` is a proof that `y = x + a`, and `hxy` has vanished. Similarly, you can destruct
-  `hyz` into its parts with `cases hyz with b hb`."
+  Hint "Now `{ha}` is a proof that `{y} = {x} + {a}`, and `hxy` has vanished. Similarly, you can destruct
+  `{hyz}` into its parts with `cases {hyz} with b hb`."
   cases hyz with b hb
   Hint "Now you need to figure out which number to `use`. See if you can take it from here."
   use a + b
diff --git a/Game/Levels/LessOrEqual/L07or_symm.lean b/Game/Levels/LessOrEqual/L07or_symm.lean
index c60066b..e6fbbc2 100644
--- a/Game/Levels/LessOrEqual/L07or_symm.lean
+++ b/Game/Levels/LessOrEqual/L07or_symm.lean
@@ -58,7 +58,7 @@ 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`."
+  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."
diff --git a/Game/Levels/LessOrEqual/L08le_total.lean b/Game/Levels/LessOrEqual/L08le_total.lean
index 56eed81..a8e50ae 100644
--- a/Game/Levels/LessOrEqual/L08le_total.lean
+++ b/Game/Levels/LessOrEqual/L08le_total.lean
@@ -21,11 +21,11 @@ and click on \"Show more help!\"
 
 /-- If $x$ and $y$ are numbers, then either $x \leq y$ or $y \leq x$. -/
 Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
-  Hint (hidden := true) "Start with `induction y with d hd`."
+  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`."
+  Hint (hidden := true) "Try `cases {hd} with h1 h2`."
   cases hd with h1 h2
   left
   cases h1 with e h1
@@ -33,20 +33,20 @@ Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
   use e + 1
   rw [succ_eq_add_one, add_assoc]
   rfl
-  Hint (hidden := true) "Now `cases h2 with e he`."
-  cases h2 with e h2
-  Hint (hidden := true) "You still don't know which way to go, so do `cases e with a`."
+  Hint (hidden := true) "Now `cases {h2} with e he`."
+  cases h2 with e he
+  Hint (hidden := true) "You still don't know which way to go, so do `cases {e} with a`."
   cases e with a
-  rw [h2]
+  rw [he]
   left
   rw [add_zero]
   use 1
   exact succ_eq_add_one d
   right
   use a
-  rw [add_succ] at h2
+  rw [add_succ] at he
   rw [succ_add]
-  exact h2
+  exact he
 
 TheoremTab "≤"