From 0353657b3e66bf0567a180f5e4e810bc860ea39e Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 18 Mar 2024 16:33:57 +0100
Subject: [PATCH] improve hints in Implication lvl 2. #45

---
 .i18n/Game.pot                         | 17 +++++++++++++----
 Game/Levels/Implication/L02exact2.lean | 13 ++++++++++---
 2 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/.i18n/Game.pot b/.i18n/Game.pot
index ac49b2f..40b607c 100644
--- a/.i18n/Game.pot
+++ b/.i18n/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.6.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Mon Mar 11 19:40:35 2024\n"
+"POT-Creation-Date: Mon Mar 18 16:33:40 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -1627,11 +1627,20 @@ msgid "Assuming $0+x=(0+y)+2$, we have $x=y+2$."
 msgstr ""
 
 #: Game.Levels.Implication.L02exact2
-msgid "Rewrite `zero_add` at `h` twice, to change `h` into the goal."
+msgid "You can use `rw [zero_add] at h` to rewrite at `«{h}»` instead\n"
+"of at the goal."
 msgstr ""
 
 #: Game.Levels.Implication.L02exact2
-msgid "Now you could finish with `rw [h]` then `rfl`, but `exact h`\n"
+msgid "Do that again!\n"
+"\n"
+"`rw [zero_add] at «{h}»` tries to fill in\n"
+"the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n"
+"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+msgstr ""
+
+#: Game.Levels.Implication.L02exact2
+msgid "Now you could finish with `rw [«{h}»]` then `rfl`, but `exact «{h}»`\n"
 "does it in one line."
 msgstr ""
 
@@ -1913,7 +1922,7 @@ msgid "We still can't prove `2 + 2 ≠ 5` because we have not talked about the\n
 "Here `False` is a generic false proposition, and `→` is Lean's notation\n"
 "for "implies". In logic we learn\n"
 "that `True → False` is false, but `False → False` is true. Hence\n"
-"`X → false` is the logical opposite of `X`.\n"
+"`X → False` is the logical opposite of `X`.\n"
 "\n"
 "Even though `a ≠ b` does not look like an implication,\n"
 "you should treat it as an implication. The next two levels will show you how.\n"
diff --git a/Game/Levels/Implication/L02exact2.lean b/Game/Levels/Implication/L02exact2.lean
index 94c5bf3..e2766c2 100644
--- a/Game/Levels/Implication/L02exact2.lean
+++ b/Game/Levels/Implication/L02exact2.lean
@@ -11,9 +11,16 @@ use rewrites to fix things up."
 
 /-- Assuming $0+x=(0+y)+2$, we have $x=y+2$. -/
 Statement (x : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
-  Hint "Rewrite `zero_add` at `h` twice, to change `h` into the goal."
-  repeat rw [zero_add] at h
-  Hint "Now you could finish with `rw [h]` then `rfl`, but `exact h`
+  Hint "You can use `rw [zero_add] at h` to rewrite at `{h}` instead
+  of at the goal."
+  rw [zero_add] at h
+  Hint (hidden := true) "Do that again!
+
+  `rw [zero_add] at {h}` tries to fill in
+  the arguments to `zero_add` (finding `{x}`) then it replaces all occurences of
+  `0 + {x}` it finds. Therefor, it did not rewrite `0 + {y}`, yet."
+  rw [zero_add] at h
+  Hint "Now you could finish with `rw [{h}]` then `rfl`, but `exact {h}`
   does it in one line."
   exact h