diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot
index 58d74d68..cc446d3b 100644
--- a/.i18n/en/Game.pot
+++ b/.i18n/en/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.23.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: 2025-09-27\n"
+"POT-Creation-Date: 2026-09-11\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -144,16 +144,6 @@ msgid "# Summary\n"
 "will add §12 as a hypothesis."
 msgstr ""
 
-#. §0: `≤`
-#: Game.Levels.LessOrEqual.L11le_two
-msgid "Nice!\n"
-"\n"
-"The next step in the development of order theory is to develop\n"
-"the theory of the interplay between §0 and multiplication.\n"
-"If you've already done Multiplication World, you're now ready for\n"
-"Advanced Multiplication World. Click on \"Home\" to access it."
-msgstr ""
-
 #. §0: `a + b + c`
 #. §1: `(a + b) + c`
 #. §2: `+`
@@ -189,27 +179,6 @@ msgstr ""
 msgid "mul_ne_zero"
 msgstr ""
 
-#. §0: ```
-#. intro h
-#. rw [add_succ, add_succ, add_zero] at h
-#. repeat apply succ_inj at h
-#. apply zero_ne_succ at h
-#. exact h
-#. ```
-#. §1: $20 + 20 ≠ 41$
-#: Game.Levels.Implication.L11two_add_two_ne_five
-msgid "Here's my proof:\n"
-"§0\n"
-"\n"
-"Even though Lean is a theorem prover, right now it's pretty clear that we have not\n"
-"developed enough material to make it an adequate calculator. In Algorithm\n"
-"World, a more computer-sciency world, we will develop machinery which makes\n"
-"questions like this much easier, and goals like §1 feasible.\n"
-"Alternatively you can do more mathematics in Advanced Addition World, where we prove\n"
-"the lemmas needed to get a working theory of inequalities. Click \"Home\" and\n"
-"decide your route."
-msgstr ""
-
 #. §0: `2 + 2 = 4`
 #: Game.Levels.Tutorial
 msgid "Welcome to tutorial world! In this world we learn the basics\n"
@@ -287,6 +256,19 @@ msgid "In this level we're going to prove that §0, where §1 is a secret natura
 "back to \"Typewriter mode\" by clicking the §16 button in the top right.)"
 msgstr ""
 
+#. §0: `apply`
+#. §1: `P → Q`
+#. §2: `P → Q`
+#. §3: `P`
+#. §4: `Q`
+#. §5: `intro`
+#: Game.Levels.Implication.L06intro
+msgid "We have seen how to §0 theorems and assumptions\n"
+"of the form §1. But what if our *goal* is of the form §2?\n"
+"To prove this goal, we need to know how to say \"let's assume §3 and deduce §4\".\n"
+"In Lean, we do this with the §5 tactic."
+msgstr ""
+
 #. §0: `∨`
 #. §1: `x = 0 ∨ x = 1 ∨ x = 2`
 #. §2: `x = 0 ∨ (x = 1 ∨ x = 2)`
@@ -310,6 +292,19 @@ msgstr ""
 msgid "Induction on §0 or §1 -- it's all the same in this one."
 msgstr ""
 
+#. §0: `rw [zero_add] at «{h}»`
+#. §1: `zero_add`
+#. §2: `«{x}»`
+#. §3: `0 + «{x}»`
+#. §4: `0 + «{y}»`
+#: Game.Levels.Implication.L02exact2
+msgid "Do that again!\n"
+"\n"
+"§0 tries to fill in\n"
+"the arguments to §1 (finding §2) then it replaces all occurrences of\n"
+"§3 it finds. Therefore, it did not rewrite §4, yet."
+msgstr ""
+
 #: Game.Levels.Power.L05pow_two
 msgid "Note: this lemma will be useful for the final boss!"
 msgstr ""
@@ -383,13 +378,6 @@ msgid "You can use §0 to rewrite at §1 instead\n"
 "of at the goal."
 msgstr ""
 
-#. §0: `add_comm`
-#. §1: `b`
-#. §2: `d`
-#: Game.Levels.Algorithm.L02add_algo1
-msgid "Finally use a targeted §0 to switch §1 and §2"
-msgstr ""
-
 #. §0: `repeat t`
 #. §1: `t`
 #. §2: `repeat rw [add_zero]`
@@ -410,6 +398,18 @@ msgid "## Summary\n"
 "§4."
 msgstr ""
 
+#. §0: `x + 1 = 4`
+#. §1: `x = 3`
+#. §2: `apply`
+#: Game.Levels.Implication.L05succ_inj2
+msgid "In the last level, we manipulated the hypothesis §0\n"
+"  until it became the goal §1. In this level we'll manipulate\n"
+"  the goal until it becomes our hypothesis! In other words, we\n"
+"  will \"argue backwards\". The §2 tactic can do this too.\n"
+"  Again I will walk you through this one (assuming you're in\n"
+"  \"Typewriter mode\")."
+msgstr ""
+
 #: Game.Levels.Addition
 msgid "Addition World"
 msgstr ""
@@ -725,6 +725,19 @@ msgstr ""
 msgid "Now you can §0."
 msgstr ""
 
+#. §0: `h2`
+#. §1: `x = 37`
+#. §2: `y = 42`
+#. §3: `apply`
+#. §4: `apply`
+#: Game.Levels.Implication.L03apply
+msgid "In this level, the hypothesis §0 is an *implication*. It says\n"
+"that *if* §1 *then* §2. We can use this\n"
+"hypothesis with the §3 tactic. Remember you can click on\n"
+"§4 or any other tactic on the right to see a detailed explanation\n"
+"of what it does, with examples."
+msgstr ""
+
 #. §0: $37$
 #. §1: $x$
 #. §2: $q$
@@ -764,12 +777,12 @@ msgid "Here's a two-line proof:\n"
 "§0"
 msgstr ""
 
-#. §0: `zero_add x`
-#. §1: `0 + x = x`
+#. §0: `zero_add n`
+#. §1: `0 + n = n`
 #. §2: `zero_add`
 #. §3: `simp`
-#. §4: `0 + x`
-#. §5: `x`
+#. §4: `0 + n`
+#. §5: `n`
 #: Game.Levels.Addition.L01zero_add
 msgid "§0 is the proof of §1.\n"
 "\n"
@@ -1002,22 +1015,24 @@ msgid "In this game you recreate the natural numbers §0 from the Peano axioms,\
 "This is a good first introduction to Lean!"
 msgstr ""
 
-#. §0: `Add a b`
-#. §1: `a + b`
-#. §2: `add_zero a : a + 0 = a`
-#. §3: `add_succ a b : a + succ b = succ (a + b)`
-#. §4: `zero_add a : 0 + a = a`
-#: Game.Levels.Tutorial.L05add_zero
-msgid "§0, with notation §1, is\n"
-"the usual sum of natural numbers. Internally it is defined\n"
-"via the following two hypotheses:\n"
-"\n"
-"* §2\n"
-"\n"
-"* §3\n"
-"\n"
-"Other theorems about naturals, such as §4, are proved\n"
-"by induction using these two basic theorems."
+#. §0: `y`
+#. §1: `add_left_eq_self`
+#. §2: `add_right_cancel`
+#. §3: `</>`
+#. §4: `>_`
+#. §5: ```
+#. nth_rewrite 2 [← zero_add y]
+#. exact add_right_cancel x 0 y
+#. ```
+#: Game.Levels.AdvAddition.L03add_left_eq_self
+msgid "Did you use induction on §0?\n"
+"Here's a two-line proof of §1 which uses §2.\n"
+"If you want to inspect it, you can go into \"Editor mode\" by clicking §3 in the top right\n"
+"and then just cut and paste the proof and move your cursor around it\n"
+"to see the hypotheses and goal at any given point\n"
+"(although you'll lose your own proof this way). Click §4 to get\n"
+"back to \"Typewriter mode\".\n"
+"§5"
 msgstr ""
 
 #. §0: $x+1=4$
@@ -1164,23 +1179,6 @@ msgstr ""
 msgid "We don't know whether to go left or right yet. So start with §0."
 msgstr ""
 
-#. §0: $2$
-#. §1: $2 = 37 × 42.$
-#. §2: $2$
-#. §3: $2$
-#. §4: `mul_left_ne_zero`
-#. §5: `one_le_of_ne_zero`
-#. §6: `mul_le_mul_right`
-#: Game.Levels.AdvMultiplication.L05le_mul_right
-msgid "One day this game will have a Prime Number World, with a final boss\n"
-"of proving that §0 is prime.\n"
-"To do this, we will have to rule out things like §1\n"
-"We will do this by proving that any factor of §2 is at most §3,\n"
-"which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n"
-"until it becomes the goal, using §4, §5 and\n"
-"§6."
-msgstr ""
-
 #. §0: `False`
 #. §1: `True`
 #. §2: `is_zero (succ a)`
@@ -1306,16 +1304,6 @@ msgid "It's all over! You have proved a theorem which has tripped up\n"
 "But wait! This boss is stirring...and mutating into a second more powerful form!"
 msgstr ""
 
-#. §0: $a$
-#. §1: $b$
-#. §2: $c$
-#. §3: $(a + b) \\times c = ac + bc$
-#: Game.Levels.Multiplication.L08add_mul
-msgid "Addition is distributive over multiplication.\n"
-"In other words, for all natural numbers §0, §1 and §2, we have\n"
-"§3."
-msgstr ""
-
 #. §0: `one_mul m`
 #. §1: `1 * m = m`
 #: Game.Levels.Multiplication.L05one_mul
@@ -1372,16 +1360,8 @@ msgid "Now you have two goals. Once you proved the first, you will jump to the s
 "as long as it is of the form §1."
 msgstr ""
 
-#. §0: `x + 1 = 4`
-#. §1: `x = 3`
-#. §2: `apply`
-#: Game.Levels.Implication.L05succ_inj2
-msgid "In the last level, we manipulated the hypothesis §0\n"
-"  until it became the goal §1. In this level we'll manipulate\n"
-"  the goal until it becomes our hypothesis! In other words, we\n"
-"  will \"argue backwards\". The §2 tactic can do this too.\n"
-"  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+#: Game.Levels.Addition.L02succ_add
+msgid "Well done! You now have enough tools to tackle the main boss of this world."
 msgstr ""
 
 #. §0: `add_zero c`
@@ -1653,17 +1633,21 @@ msgstr ""
 msgid "succ_add"
 msgstr ""
 
-#. §0: `rw [zero_add] at «{h}»`
-#. §1: `zero_add`
-#. §2: `«{x}»`
-#. §3: `0 + «{x}»`
-#. §4: `0 + «{y}»`
-#: Game.Levels.Implication.L02exact2
-msgid "Do that again!\n"
+#. §0: `add_comm`
+#. §1: `b`
+#. §2: `d`
+#: Game.Levels.Algorithm.L02add_algo1
+msgid "Finally use a targeted §0 to switch §1 and §2."
+msgstr ""
+
+#. §0: `≤`
+#: Game.Levels.LessOrEqual.L11le_two
+msgid "Nice!\n"
 "\n"
-"§0 tries to fill in\n"
-"the arguments to §1 (finding §2) then it replaces all occurrences of\n"
-"§3 it finds. Therefor, it did not rewrite §4, yet."
+"The next step in the development of order theory is to develop\n"
+"the theory of the interplay between §0 and multiplication.\n"
+"If you've already done Multiplication World, you're now ready for\n"
+"Advanced Multiplication World. Click on \"Home\" to access it."
 msgstr ""
 
 #. §0: `a`
@@ -1718,52 +1702,6 @@ msgid "In this world we define §0 and prove standard facts\n"
 "Click on \"Start\" to proceed."
 msgstr ""
 
-#: Game
-msgid "*Game version: 4.3*\n"
-"\n"
-"*Recent additions: bug fixes*\n"
-"\n"
-"## Progress saving\n"
-"\n"
-"The game stores your progress in your local browser storage.\n"
-"If you delete it, your progress will be lost!\n"
-"\n"
-"Warning: In most browsers, deleting cookies will also clear the local storage\n"
-"(or \"local site data\"). Make sure to download your game progress first!\n"
-"\n"
-"## Credits\n"
-"\n"
-"* **Creators:** Kevin Buzzard, Jon Eugster\n"
-"* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n"
-"* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n"
-"* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n"
-"* **Additional thanks:** All the student beta testers, all the schools\n"
-"who invited Kevin to speak, and all the schoolkids who asked him questions\n"
-"about the material.\n"
-"\n"
-"## Resources\n"
-"\n"
-"* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n"
-"* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n"
-"\n"
-"## Problems?\n"
-"\n"
-"Please ask any questions about this game in the\n"
-"[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\n"
-"the stream \"New Members\". The community will happily help. Note that\n"
-"the Lean Zulip chat is a professional research forum.\n"
-"Please use your full real name there, stay on topic, and be nice. If you're\n"
-"looking for somewhere less formal (e.g. you want to post natural number\n"
-"game memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n"
-"\n"
-"Alternatively, if you experience issues / bugs you can also open github issues:\n"
-"\n"
-"* For issues with the game engine, please open an\n"
-"[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n"
-"* For issues about the game's content, please open an\n"
-"[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo."
-msgstr ""
-
 #. §0: $a$
 #. §1: $m$
 #. §2: $n$
@@ -1774,37 +1712,6 @@ msgstr ""
 msgid "For all naturals §0, §1, §2, we have §3."
 msgstr ""
 
-#. §0: ```lean
-#. nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.
-#. rw [add_succ]
-#. rw [one_eq_succ_zero]
-#. rw [add_succ, add_zero] -- two rewrites at once
-#. rw [← three_eq_succ_two] -- change `succ 2` to `3`
-#. rw [← four_eq_succ_three]
-#. rfl
-#. ```
-#. §1: `</>`
-#. §2: `>_`
-#. §3: `induction`
-#: Game.Levels.Tutorial.L08twoaddtwo
-msgid "Here is an example proof of 2+2=4 showing off various techniques.\n"
-"\n"
-"§0\n"
-"\n"
-"Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\n"
-"on the §1 button in the top right. You can now see your proof\n"
-"written as several lines of code. Move your cursor between lines to see\n"
-"the goal state at any point. Now cut and paste your code elsewhere if you\n"
-"want to save it, and paste the above proof in instead. Move your cursor\n"
-"around to investigate. When you've finished, click the §2 button in the top right to\n"
-"move back into \"Typewriter mode\".\n"
-"\n"
-"You have finished tutorial world!\n"
-"Click \"Home\" to go back to the\n"
-"overworld, and select Addition World, where you will learn\n"
-"about the §3 tactic."
-msgstr ""
-
 #: Game.Levels.AdvMultiplication.L09mul_left_cancel
 msgid "mul_left_cancel"
 msgstr ""
@@ -1934,233 +1841,6 @@ msgstr ""
 msgid "Let's now learn about Peano's second axiom for addition, §0."
 msgstr ""
 
-#. §0: `h2`
-#. §1: `x = 37`
-#. §2: `y = 42`
-#. §3: `apply`
-#. §4: `apply`
-#: Game.Levels.Implication.L03apply
-msgid "In this level, the hypotheses §0 is an *implication*. It says\n"
-"that *if* §1 *then* §2. We can use this\n"
-"hypothesis with the §3 tactic. Remember you can click on\n"
-"§4 or any other tactic on the right to see a detailed explanation\n"
-"of what it does, with examples."
-msgstr ""
-
-#. §0: `add_comm b c`
-#. §1: `b + c = c + b`
-#. §2: `a + b + c = a + c + b`
-#. §3: `rw [add_comm b c]`
-#. §4: `(a + b) + c = (a + c) + b`
-#. §5: `b + c`
-#. §6: `add_right_comm`
-#. §7: `add_assoc`
-#. §8: `add_comm`
-#. §9: `rw [add_comm b]`
-#. §10: `b + ? = ? + b`
-#. §11: `rw [add_comm b c]`
-#. §12: `b + c = c + b`
-#: Game.Levels.Addition.L05add_right_comm
-msgid "§0 is a proof that §1. But if your goal\n"
-"is §2 then §3 will not\n"
-"work! Because the goal means §4 so there\n"
-"is no §5 term *directly* in the goal.\n"
-"\n"
-"Use associativity and commutativity to prove §6.\n"
-"You don't need induction. §7 moves brackets around,\n"
-"and §8 moves variables around.\n"
-"\n"
-"Remember that you can do more targeted rewrites by\n"
-"adding explicit variables as inputs to theorems. For example §9\n"
-"will only do rewrites of the form §10, and §11\n"
-"will only do rewrites of the form §12."
-msgstr ""
-
-#. §0: `h`
-#. §1: `X = Y`
-#. §2: `rw [h]`
-#. §3: `X`
-#. §4: `Y`
-#. §5: `rw [← h]`
-#. §6: `Y`
-#. §7: `X`
-#. §8: `\\left `
-#. §9: `\\l`
-#. §10: `rw [h1, h2]`
-#. §11: `rw [h] at h2`
-#. §12: `X`
-#. §13: `Y`
-#. §14: `h2`
-#. §15: `rw [h] at h1 h2 ⊢`
-#. §16: `X`
-#. §17: `Y`
-#. §18: `⊢`
-#. §19: `\\|-`
-#. §20: `repeat rw [add_zero]`
-#. §21: `? + 0`
-#. §22: `?`
-#. §23: `? + 0`
-#. §24: `nth_rewrite 2 [h]`
-#. §25: `X`
-#. §26: `Y`
-#. §27: `h : x = y + y`
-#. §28: ```
-#. succ (x + 0) = succ (y + y)
-#. ```
-#. §29: `rw [add_zero]`
-#. §30: `succ x = succ (y + y)`
-#. §31: `rw [h]`
-#. §32: `succ (y + y) = succ (y + y)`
-#. §33: `rfl`
-#. §34: `rw`
-#. §35: ```
-#. h1 : x = y + 3
-#. h2 : 2 * y = x
-#. ```
-#. §36: `rw [h1] at h2`
-#. §37: `h2`
-#. §38: `h2 : 2 * y = y + 3`
-#. §39: `rw h`
-#. §40: `h`
-#. §41: `A = B`
-#. §42: `h`
-#. §43: `rw`
-#. §44: `rw [P = Q]`
-#. §45: `P = Q`
-#. §46: `h : P = Q`
-#. §47: `rw [h]`
-#. §48: `rw`
-#. §49: `h : A = B`
-#. §50: `A`
-#. §51: `rw [h]`
-#. §52: `B`
-#. §53: `A`
-#. §54: `add_zero`
-#. §55: `? + 0 = ?`
-#. §56: `add_zero`
-#. §57: `?`
-#. §58: `rw`
-#. §59: `x + 0`
-#. §60: `?`
-#. §61: `x`
-#. §62: `x + 0`
-#. §63: `x`
-#. §64: `rw [add_zero]`
-#. §65: `(0 + 0) + (x + 0) + (0 + 0) + (x + 0)`
-#. §66: `0 + (x + 0) + 0 + (x + 0)`
-#. §67: `b + c + a = b + (a + c)`
-#. §68: `a + c`
-#. §69: `c + a`
-#. §70: `rw [add_comm]`
-#. §71: `rw [add_comm a c]`
-#. §72: `a + c`
-#. §73: `c + a`
-#. §74: `add_comm`
-#. §75: `?1 + ?2 = ?2 + ?1`
-#. §76: `add_comm a`
-#. §77: `a + ? = ? + a`
-#. §78: `add_comm a c`
-#. §79: `a + c = c + a`
-#. §80: `h : X = Y`
-#. §81: `rw [h]`
-#. §82: `X`
-#. §83: `Y`
-#. §84: `X`
-#. §85: `Y`
-#. §86: `nth_rewrite 37 [h]`
-#: Game.Levels.Tutorial.L02rw
-msgid "## Summary\n"
-"\n"
-"If §0 is a proof of an equality §1, then §2 will change\n"
-"all §3s in the goal to §4s. It's the way to \\\\\"substitute in\\\\\".\n"
-"\n"
-"## Variants\n"
-"\n"
-"* §5 (changes §6s to §7s; get the back arrow by typing §8 or §9.)\n"
-"\n"
-"* §10 (a sequence of rewrites)\n"
-"\n"
-"* §11 (changes §12s to §13s in hypothesis §14)\n"
-"\n"
-"* §15 (changes §16s to §17s in two hypotheses and the goal;\n"
-"get the §18 symbol with §19.)\n"
-"\n"
-"* §20 will keep changing §21 to §22\n"
-"until there are no more matches for §23.\n"
-"\n"
-"* §24 will change only the second §25 in the goal to §26.\n"
-"\n"
-"### Example:\n"
-"\n"
-"If you have the assumption §27 and your goal is\n"
-"§28\n"
-"\n"
-"then\n"
-"\n"
-"§29\n"
-"\n"
-"will change the goal into §30, and then\n"
-"\n"
-"§31\n"
-"\n"
-"will change the goal into §32, which\n"
-"can be solved with §33.\n"
-"\n"
-"### Example:\n"
-"\n"
-"You can use §34 to change a hypothesis as well.\n"
-"For example, if you have two hypotheses\n"
-"§35\n"
-"then §36 will turn §37 into §38.\n"
-"\n"
-"## Common errors\n"
-"\n"
-"* You need the square brackets. §39 is never correct.\n"
-"\n"
-"* If §40 is not a *proof* of an *equality* (a statement of the form §41),\n"
-"for example if §42 is a function or an implication,\n"
-"then §43 is not the tactic you want to use. For example,\n"
-"§44 is never correct: §45 is the theorem *statement*,\n"
-"not the proof. If §46 is the proof, then §47 will work.\n"
-"\n"
-"## Details\n"
-"\n"
-"The §48 tactic is a way to do \\\\\"substituting in\\\\\". There\n"
-"are two distinct situations where you can use this tactic.\n"
-"\n"
-"1) Basic usage: if §49 is an assumption or\n"
-"the proof of a theorem, and if the goal contains one or more §50s, then §51\n"
-"will change them all to §52s. The tactic will error\n"
-"if there are no §53s in the goal.\n"
-"\n"
-"2) Advanced usage: Assumptions coming from theorem proofs\n"
-"often have missing pieces. For example §54\n"
-"is a proof that §55 because §56 really is a function,\n"
-"and §57 is the input. In this situation §58 will look through the goal\n"
-"for any subterm of the form §59, and the moment it\n"
-"finds one it fixes §60 to be §61 then changes all §62s to §63s.\n"
-"\n"
-"Exercise: think about why §64 changes the term\n"
-"§65 to\n"
-"§66\n"
-"\n"
-"If you can't remember the name of the proof of an equality, look it up in\n"
-"the list of lemmas on the right.\n"
-"\n"
-"## Targeted usage\n"
-"\n"
-"If your goal is §67 and you want to rewrite §68\n"
-"to §69, then §70 will not work because Lean finds another\n"
-"addition first and swaps those inputs instead. Use §71 to\n"
-"guarantee that Lean rewrites §72 to §73. This works because\n"
-"§74 is a proof that §75, §76 is a proof\n"
-"that §77, and §78 is a proof that §79.\n"
-"\n"
-"If §80 then §81 will turn all §82s into §83s.\n"
-"If you only want to change the 37th occurrence of §84\n"
-"to §85 then do §86."
-msgstr ""
-
 #. §0: $a, b,\\ldots h$
 #. §1: $(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$
 #: Game.Levels.Algorithm.L03add_algo2
@@ -2459,6 +2139,52 @@ msgid "## Summary\n"
 "as mathematicians are concerned, and who cares what the definition of addition is).*"
 msgstr ""
 
+#: Game
+msgid "*Game version: 4.3*\n"
+"\n"
+"*Recent additions: bug fixes*\n"
+"\n"
+"## Progress saving\n"
+"\n"
+"The game stores your progress in your local browser storage.\n"
+"If you delete it, your progress will be lost!\n"
+"\n"
+"Warning: In most browsers, deleting cookies will also clear the local storage\n"
+"(or \"local site data\"). Make sure to download your game progress first!\n"
+"\n"
+"## Credits\n"
+"\n"
+"* **Creators:** Kevin Buzzard, Jon Eugster\n"
+"* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n"
+"* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n"
+"* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n"
+"* **Additional thanks:** All the student beta testers, all the schools\n"
+"who invited Kevin to speak, and all the schoolkids who asked him questions\n"
+"about the material.\n"
+"\n"
+"## Resources\n"
+"\n"
+"* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n"
+"* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n"
+"\n"
+"## Problems?\n"
+"\n"
+"Please ask any questions about this game in the\n"
+"[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\n"
+"the stream \"New Members\". The community will happily help. Note that\n"
+"the Lean Zulip chat is a professional research forum.\n"
+"Please use your full real name there, stay on topic, and be nice. If you're\n"
+"looking for somewhere less formal (e.g. you want to post natural number\n"
+"game memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n"
+"\n"
+"Alternatively, if you experience issues / bugs you can also open github issues:\n"
+"\n"
+"* For issues with the game engine, please open an\n"
+"[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n"
+"* For issues about the game's content, please open an\n"
+"[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo."
+msgstr ""
+
 #. §0: `b = 0`
 #. §1: `a * b = 0`
 #. §2: `X ≠ 0`
@@ -2588,12 +2314,214 @@ msgstr ""
 msgid "Many people find §0 easy, but some find §1 confusing.\n"
 "If you find it confusing, then just argue forwards.\n"
 "\n"
-"You can read more about the §2 tactic in its documentation, which you can view by\n"
-"clicking on the tactic in the list on the right."
-msgstr ""
-
-#: Game.Levels.Algorithm.L03add_algo2
-msgid "Let's now make our own tactic to do this."
+"You can read more about the §2 tactic in its documentation, which you can view by\n"
+"clicking on the tactic in the list on the right."
+msgstr ""
+
+#. §0: $2$
+#. §1: $2 = 37 × 42$
+#. §2: $2$
+#. §3: $2$
+#. §4: `mul_left_ne_zero`
+#. §5: `one_le_of_ne_zero`
+#. §6: `mul_le_mul_right`
+#: Game.Levels.AdvMultiplication.L05le_mul_right
+msgid "One day this game will have a Prime Number World, with a final boss\n"
+"of proving that §0 is prime.\n"
+"To do this, we will have to rule out things like §1.\n"
+"We will do this by proving that any factor of §2 is at most §3,\n"
+"which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n"
+"until it becomes the goal, using §4, §5 and\n"
+"§6."
+msgstr ""
+
+#: Game.Levels.Algorithm.L03add_algo2
+msgid "Let's now make our own tactic to do this."
+msgstr ""
+
+#. §0: `h`
+#. §1: `X = Y`
+#. §2: `rw [h]`
+#. §3: `X`
+#. §4: `Y`
+#. §5: `rw [← h]`
+#. §6: `Y`
+#. §7: `X`
+#. §8: `\\left `
+#. §9: `\\l`
+#. §10: `rw [h1, h2]`
+#. §11: `rw [h] at h2`
+#. §12: `X`
+#. §13: `Y`
+#. §14: `h2`
+#. §15: `rw [h] at h1 h2 ⊢`
+#. §16: `X`
+#. §17: `Y`
+#. §18: `⊢`
+#. §19: `\\|-`
+#. §20: `repeat rw [add_zero]`
+#. §21: `? + 0`
+#. §22: `?`
+#. §23: `? + 0`
+#. §24: `nth_rewrite 2 [h]`
+#. §25: `X`
+#. §26: `Y`
+#. §27: `h : x = y + y`
+#. §28: ```
+#. succ (x + 0) = succ (y + y)
+#. ```
+#. §29: `rw [add_zero]`
+#. §30: `succ x = succ (y + y)`
+#. §31: `rw [h]`
+#. §32: `succ (y + y) = succ (y + y)`
+#. §33: `rfl`
+#. §34: `rw`
+#. §35: ```
+#. h1 : x = y + 3
+#. h2 : 2 * y = x
+#. ```
+#. §36: `rw [h1] at h2`
+#. §37: `h2`
+#. §38: `h2 : 2 * y = y + 3`
+#. §39: `rw h`
+#. §40: `h`
+#. §41: `A = B`
+#. §42: `h`
+#. §43: `rw`
+#. §44: `rw [P = Q]`
+#. §45: `P = Q`
+#. §46: `h : P = Q`
+#. §47: `rw [h]`
+#. §48: `rw`
+#. §49: `h : A = B`
+#. §50: `A`
+#. §51: `rw [h]`
+#. §52: `B`
+#. §53: `A`
+#. §54: `add_zero`
+#. §55: `? + 0 = ?`
+#. §56: `add_zero`
+#. §57: `?`
+#. §58: `rw`
+#. §59: `x + 0`
+#. §60: `?`
+#. §61: `x`
+#. §62: `x + 0`
+#. §63: `x`
+#. §64: `rw [add_zero]`
+#. §65: `(0 + 0) + (x + 0) + (0 + 0) + (x + 0)`
+#. §66: `0 + (x + 0) + 0 + (x + 0)`
+#. §67: `b + c + a = b + (a + c)`
+#. §68: `a + c`
+#. §69: `c + a`
+#. §70: `rw [add_comm]`
+#. §71: `rw [add_comm a c]`
+#. §72: `a + c`
+#. §73: `c + a`
+#. §74: `add_comm`
+#. §75: `?1 + ?2 = ?2 + ?1`
+#. §76: `add_comm a`
+#. §77: `a + ? = ? + a`
+#. §78: `add_comm a c`
+#. §79: `a + c = c + a`
+#. §80: `h : X = Y`
+#. §81: `rw [h]`
+#. §82: `X`
+#. §83: `Y`
+#. §84: `X`
+#. §85: `Y`
+#. §86: `nth_rewrite 37 [h]`
+#: Game.Levels.Tutorial.L02rw
+msgid "## Summary\n"
+"\n"
+"If §0 is a proof of an equality §1, then §2 will change\n"
+"all §3s in the goal to §4s. It's the way to \\\\\"substitute in\\\\\".\n"
+"\n"
+"## Variants\n"
+"\n"
+"* §5 (changes §6s to §7s; get the back arrow by typing §8 or §9.)\n"
+"\n"
+"* §10 (a sequence of rewrites)\n"
+"\n"
+"* §11 (changes §12s to §13s in hypothesis §14)\n"
+"\n"
+"* §15 (changes §16s to §17s in two hypotheses and the goal;\n"
+"get the §18 symbol with §19.)\n"
+"\n"
+"* §20 will keep changing §21 to §22\n"
+"until there are no more matches for §23.\n"
+"\n"
+"* §24 will change only the second §25 in the goal to §26.\n"
+"\n"
+"### Example:\n"
+"\n"
+"If you have the assumption §27 and your goal is\n"
+"§28\n"
+"\n"
+"then\n"
+"\n"
+"§29\n"
+"\n"
+"will change the goal into §30, and then\n"
+"\n"
+"§31\n"
+"\n"
+"will change the goal into §32, which\n"
+"can be solved with §33.\n"
+"\n"
+"### Example:\n"
+"\n"
+"You can use §34 to change a hypothesis as well.\n"
+"For example, if you have two hypotheses\n"
+"§35\n"
+"then §36 will turn §37 into §38.\n"
+"\n"
+"## Common errors\n"
+"\n"
+"* You need the square brackets. §39 is never correct.\n"
+"\n"
+"* If §40 is not a *proof* of an *equality* (a statement of the form §41),\n"
+"for example if §42 is a function or an implication,\n"
+"then §43 is not the tactic you want to use. For example,\n"
+"§44 is never correct: §45 is the theorem *statement*,\n"
+"not the proof. If §46 is the proof, then §47 will work.\n"
+"\n"
+"## Details\n"
+"\n"
+"The §48 tactic is a way to do \\\\\"substituting in\\\\\". There\n"
+"are two distinct situations where you can use this tactic.\n"
+"\n"
+"1) Basic usage: if §49 is an assumption or\n"
+"the proof of a theorem, and if the goal contains one or more §50s, then §51\n"
+"will change them all to §52s. The tactic will error\n"
+"if there are no §53s in the goal.\n"
+"\n"
+"2) Advanced usage: Assumptions coming from theorem proofs\n"
+"often have missing pieces. For example §54\n"
+"is a proof that §55 because §56 really is a function,\n"
+"and §57 is the input. In this situation §58 will look through the goal\n"
+"for any subterm of the form §59, and the moment it\n"
+"finds one it fixes §60 to be §61 then changes all §62s to §63s.\n"
+"\n"
+"Exercise: think about why §64 changes the term\n"
+"§65 to\n"
+"§66\n"
+"\n"
+"If you can't remember the name of the proof of an equality, look it up in\n"
+"the list of lemmas on the right.\n"
+"\n"
+"## Targeted usage\n"
+"\n"
+"If your goal is §67 and you want to rewrite §68\n"
+"to §69, then §70 will not work because Lean finds another\n"
+"addition first and swaps those inputs instead. Use §71 to\n"
+"guarantee that Lean rewrites §72 to §73. This works because\n"
+"§74 is a proof that §75, §76 is a proof\n"
+"that §77, and §78 is a proof that §79.\n"
+"\n"
+"If §80 then §81 will turn all §82s into §83s.\n"
+"If you only want to change the 37th occurrence of §84\n"
+"to §85 then do §86."
 msgstr ""
 
 #: Game.Levels.AdvAddition.L06add_left_eq_zero
@@ -2625,20 +2553,6 @@ msgstr ""
 msgid "Natural Number Game"
 msgstr ""
 
-#. §0: ```
-#. rw [add_comm]
-#. exact add_right_eq_zero b a
-#. ```
-#. §1: `≤`
-#: Game.Levels.AdvAddition.L06add_left_eq_zero
-msgid "How about this for a proof:\n"
-"\n"
-"§0\n"
-"\n"
-"That's the end of Advanced Addition World! You'll need these theorems\n"
-"for the next world, §1 World. Click on \"Home\" to access it."
-msgstr ""
-
 #. §0: `n`
 #. §1: `cases n with d`
 #. §2: `n = 0`
@@ -2904,6 +2818,37 @@ msgid "You can start a proof by induction on §0 by typing:\n"
 "§1."
 msgstr ""
 
+#. §0: ```lean
+#. nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.
+#. rw [add_succ]
+#. rw [one_eq_succ_zero]
+#. rw [add_succ, add_zero] -- two rewrites at once
+#. rw [← three_eq_succ_two] -- change `succ 2` to `3`
+#. rw [← four_eq_succ_three]
+#. rfl
+#. ```
+#. §1: `</>`
+#. §2: `>_`
+#. §3: `induction`
+#: Game.Levels.Tutorial.L08twoaddtwo
+msgid "Here is an example proof of 2+2=4 showing off various techniques.\n"
+"\n"
+"§0\n"
+"\n"
+"Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\n"
+"on the §1 button in the top right. You can now see your proof\n"
+"written as several lines of code. Move your cursor between lines to see\n"
+"the goal state at any point. Now cut and paste your code elsewhere if you\n"
+"want to save it, and paste the above proof in instead. Move your cursor\n"
+"around to investigate. When you've finished, click the §2 button in the top right to\n"
+"move back into \"Typewriter mode\".\n"
+"\n"
+"You have finished tutorial world!\n"
+"Click \"Home\" to go back to the\n"
+"overworld, and select Addition World, where you will learn\n"
+"about the §3 tactic."
+msgstr ""
+
 #. §0: `Pow a b`
 #. §1: `a ^ b`
 #. §2: `pow_zero a : a ^ 0 = 1`
@@ -2950,12 +2895,6 @@ msgid "Totality of §0 is the boss level of this world, and it's coming up next.
 "and the other where you went right."
 msgstr ""
 
-#. §0: `one_eq_succ_zero`
-#. §1: `1 = succ 0`
-#: Game.Levels.Tutorial.L03two_eq_ss0
-msgid "§0 is a proof of §1.\""
-msgstr ""
-
 #: Game.Levels.Addition.L01zero_add
 msgid "zero_add"
 msgstr ""
@@ -2973,8 +2912,18 @@ msgid "We've just seen that §0, but if §1\n"
 "is a successor, then §2. We prove that here."
 msgstr ""
 
-#. §0: `zero_mul x`
-#. §1: `0 * x = 0`
+#. §0: $a$
+#. §1: $b$
+#. §2: $c$
+#. §3: $(a + b) \\times c = ac + bc$
+#: Game.Levels.Multiplication.L08add_mul
+msgid "Multiplication is distributive over addition.\n"
+"In other words, for all natural numbers §0, §1 and §2, we have\n"
+"§3."
+msgstr ""
+
+#. §0: `zero_mul m`
+#. §1: `0 * m = 0`
 #. §2: `zero_mul`
 #. §3: `simp`
 #: Game.Levels.Multiplication.L02zero_mul
@@ -2999,6 +2948,27 @@ msgid "If you have completed Algorithm World then you can use the §0 tactic\n"
 "here. If not then I'll talk you through a manual approach."
 msgstr ""
 
+#. §0: $2y=2(x+7)$
+#. §1: `h`
+#. §2: $y = x + 7$
+#. §3: `h`
+#. §4: `h`
+#. §5: `x`
+#. §6: `rfl`
+#. §7: $y$
+#. §8: `h`
+#. §9: `rw`
+#: Game.Levels.Tutorial.L02rw
+msgid "In this level the *goal* is §0 but to help us we\n"
+"have an *assumption* §1 saying that §2. Check that you can see §3 in\n"
+"your list of assumptions. Lean thinks of §4 as being a secret proof of the\n"
+"assumption, rather like §5 is a secret number.\n"
+"\n"
+"Before we can use §6, we have to \"substitute in for §7\".\n"
+"We do this in Lean by *rewriting* the goal with §8,\n"
+"using the §9 tactic."
+msgstr ""
+
 #. §0: `zero_ne_succ n`
 #. §1: `0 ≠ succ n`
 #. §2: `a ≠ b`
@@ -3045,8 +3015,9 @@ msgstr ""
 msgid "If §0 then §1 or §2 or §3."
 msgstr ""
 
-#. §0: `two_eq_succ_one`
-#. §1: `2 = succ 1`
+#. §0: `one_eq_succ_zero`
+#. §1: `1 = succ 0`
+#: Game.Levels.Tutorial.L03two_eq_ss0
 #: Game.Levels.Tutorial.L03two_eq_ss0
 #: Game.Levels.Tutorial.L03two_eq_ss0
 #: Game.Levels.Tutorial.L03two_eq_ss0
@@ -3158,6 +3129,20 @@ msgstr ""
 msgid "§0 is a proof that if §1 then §2 or §3 or §4."
 msgstr ""
 
+#. §0: ```
+#. rw [add_comm]
+#. exact add_right_eq_zero b a
+#. ```
+#. §1: `≤`
+#: Game.Levels.AdvAddition.L06add_left_eq_zero
+msgid "How about this for a proof:\n"
+"\n"
+"§0\n"
+"\n"
+"That's the end of Advanced Addition World! You'll need these theorems\n"
+"for the next world, §1 World. Click on \"Home\" to access it."
+msgstr ""
+
 #. §0: `Mul a b`
 #. §1: `a * b`
 #. §2: `mul_zero a : a * 0 = 0`
@@ -3988,10 +3973,6 @@ msgid "We know §0 is a proof of §1 -- but what\n"
 "the proof §11; now try proving §12."
 msgstr ""
 
-#: Game.Levels.Addition.L02succ_add
-msgid "Well done! You now have enough tools to tackle the main boss of this level."
-msgstr ""
-
 #. §0: `use`
 #. §1: `use`
 #: Game.Levels.LessOrEqual.L03le_succ_self
@@ -4085,27 +4066,6 @@ msgid "How should we define §0? Just like addition, we need to give definitions
 "Let's get started."
 msgstr ""
 
-#. §0: $2y=2(x+7)$
-#. §1: `h`
-#. §2: $y = x + 7$
-#. §3: `h`
-#. §4: `h`
-#. §5: `x`
-#. §6: `rfl`
-#. §7: $y$
-#. §8: `h`
-#. §9: `rw`
-#: Game.Levels.Tutorial.L02rw
-msgid "In this level the *goal* is §0 but to help us we\n"
-"have an *assumption* §1 saying that §2. Check that you can see §3 in\n"
-"your list of assumptions. Lean thinks of §4 as being a secret proof of the\n"
-"assumption, rather like §5 is a secret number.\n"
-"\n"
-"Before we can use §6, we have to \"substitute in for §7\".\n"
-"We do this in Lean by *rewriting* the proof §8,\n"
-"using the §9 tactic."
-msgstr ""
-
 #. §0: ```
 #. symm
 #. exact zero_ne_one
@@ -4135,21 +4095,37 @@ msgid "Now you could finish with §0 then §1, but §2\n"
 "does it in one line."
 msgstr ""
 
-#: Game.Levels.Power.L10FLT
-msgid "Fermat's Last Theorem"
+#. §0: `add_comm b c`
+#. §1: `b + c = c + b`
+#. §2: `a + b + c = a + c + b`
+#. §3: `rw [add_comm b c]`
+#. §4: `(a + b) + c = (a + c) + b`
+#. §5: `b + c`
+#. §6: `add_right_comm`
+#. §7: `add_assoc`
+#. §8: `add_comm`
+#. §9: `rw [add_comm b]`
+#. §10: `b + ? = ? + b`
+#. §11: `rw [add_comm b c]`
+#. §12: `b + c = c + b`
+#: Game.Levels.Addition.L05add_right_comm
+msgid "§0 is a proof that §1. But if your goal\n"
+"is §2 then §3 will not\n"
+"work! Because the goal means §4 so there\n"
+"is no §5 term *directly* in the goal.\n"
+"\n"
+"Use associativity and commutativity to prove §6.\n"
+"You don't need induction. §7 moves brackets around,\n"
+"and §8 moves variables around.\n"
+"\n"
+"Remember that you can do more targeted rewrites by\n"
+"adding explicit variables as inputs to theorems. For example §9\n"
+"will only do rewrites of the form §10, and §11\n"
+"will only do rewrites of the form §12."
 msgstr ""
 
-#. §0: `apply`
-#. §1: `P → Q`
-#. §2: `P → Q`
-#. §3: `P`
-#. §4: `Q`
-#. §5: `intro`
-#: Game.Levels.Implication.L06intro
-msgid "We have seen how to §0 theorems and assumptions\n"
-"of the form §1. But what if our *goal* is of the form §2?\n"
-"To prove this goal, we need to know how to say \"let's assume §3 and deduce §4\"\n"
-"in Lean. We do this with the §5 tactic."
+#: Game.Levels.Power.L10FLT
+msgid "Fermat's Last Theorem"
 msgstr ""
 
 #. §0: $x$
@@ -4211,39 +4187,6 @@ msgid "Very well done.\n"
 "The final few levels in this world are much easier."
 msgstr ""
 
-#. §0: `y`
-#. §1: `add_left_eq_self`
-#. §2: `add_right_cancel`
-#. §3: `</>`
-#. §4: `>_`
-#. §5: ```
-#. nth_rewrite 2 [← zero_add y]
-#. exact add_right_cancel x 0 y
-#. ```
-#: Game.Levels.AdvAddition.L03add_left_eq_self
-msgid "Did you use induction on §0?\n"
-"Here's a two-line proof of §1 which uses §2.\n"
-"If you want to inspect it, you can go into editor mode by clicking §3 in the top right\n"
-"and then just cut and paste the proof and move your cursor around it\n"
-"to see the hypotheses and goal at any given point\n"
-"(although you'll lose your own proof this way). Click §4 to get\n"
-"back to command line mode.\n"
-"§5"
-msgstr ""
-
-#. §0: `a = 0`
-#. §1: `x + a = x`
-#: Game.Levels.Addition.L05add_right_comm
-msgid "You've now seen all the tactics you need to beat the final boss of the game.\n"
-"You can begin the journey towards this boss by entering Multiplication World.\n"
-"\n"
-"Or you can go off the beaten track and learn some new tactics in Implication\n"
-"World. These tactics let you prove more facts about addition, such as\n"
-"how to deduce §0 from §1.\n"
-"\n"
-"Click \"Home\" and make your choice."
-msgstr ""
-
 #: Game.Levels.LessOrEqual.L05le_zero
 msgid "It's \"intuitively obvious\" that there are no numbers less than zero,\n"
 "but to prove it you will need a result which you showed in advanced\n"
@@ -4432,6 +4375,24 @@ msgid "This level is more important than you think; it plays\n"
 "a useful role when battling a big boss later on."
 msgstr ""
 
+#. §0: `Add a b`
+#. §1: `a + b`
+#. §2: `add_zero a : a + 0 = a`
+#. §3: `add_succ a b : a + succ b = succ (a + b)`
+#. §4: `zero_add a : 0 + a = a`
+#: Game.Levels.Tutorial.L05add_zero
+msgid "§0, with notation §1, is\n"
+"the usual sum of natural numbers. Internally it is defined\n"
+"via the following two hypotheses:\n"
+"\n"
+"* §2\n"
+"\n"
+"* §3\n"
+"\n"
+"Other theorems about naturals, such as §4, are proved\n"
+"by induction using these two basic theorems."
+msgstr ""
+
 #. §0: `cases h2 with h0 h1`
 #: Game.Levels.AdvMultiplication.L06mul_right_eq_one
 msgid "Now §0 and deal with the two\n"
@@ -4487,6 +4448,19 @@ msgstr ""
 msgid "Advanced Multiplication World"
 msgstr ""
 
+#. §0: `a = 0`
+#. §1: `x + a = x`
+#: Game.Levels.Addition.L05add_right_comm
+msgid "You've now seen all the tactics you need to beat the final boss of the game.\n"
+"You can begin the journey towards this boss by entering Multiplication World.\n"
+"\n"
+"Or you can go off the beaten track and learn some new tactics in Implication\n"
+"World. These tactics let you prove more facts about addition, such as\n"
+"how to deduce §0 from §1.\n"
+"\n"
+"Click \"Home\" and make your choice."
+msgstr ""
+
 #. §0: $2$
 #. §1: $0$
 #: Game.Levels.Tutorial.L03two_eq_ss0
@@ -4550,6 +4524,27 @@ msgstr ""
 msgid "pow_one"
 msgstr ""
 
+#. §0: ```
+#. intro h
+#. rw [add_succ, add_succ, add_zero] at h
+#. repeat apply succ_inj at h
+#. apply zero_ne_succ at h
+#. exact h
+#. ```
+#. §1: $20 + 20 ≠ 41$
+#: Game.Levels.Implication.L11two_add_two_ne_five
+msgid "Here's my proof:\n"
+"§0\n"
+"\n"
+"Even though Lean is a theorem prover, right now it's pretty clear that we have not\n"
+"developed enough material to make it an adequate calculator. In Algorithm\n"
+"World, a more computer-sciency world, we will develop machinery which makes\n"
+"questions like this much easier, and goals like §1 feasible.\n"
+"Alternatively you can do more mathematics in Advanced Addition World, where we prove\n"
+"the lemmas needed to get a working theory of inequalities. Click \"Home\" and\n"
+"decide your route."
+msgstr ""
+
 #. §0: `rw [two_eq_succ_one, one_eq_succ_zero]`
 #. §1: `rfl`
 #: Game.Levels.Tutorial.L03two_eq_ss0
diff --git a/.i18n/fr/Game.json b/.i18n/fr/Game.json
index c56421f7..b0049ef4 100644
--- a/.i18n/fr/Game.json
+++ b/.i18n/fr/Game.json
@@ -218,10 +218,10 @@
  "`add_left_cancel a b n` est le théorème que $n+a=n+b\\implies a=b$.\nVous pouvez le prouver par induction sur `n` ou le déduire de `add_right_cancel`.",
  "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$":
  "`add_left_cancel a b n` est le théorème que $n+a=n+b \\implies a=b.$",
- "`add_comm a b` is a proof of `a + b = b + a`.":
- "`add_comm a b` est une preuve de `a + b = b + a`.",
  "`add_comm b c` is a proof that `b + c = c + b`. But if your goal\nis `a + b + c = a + c + b` then `rw [add_comm b c]` will not\nwork! Because the goal means `(a + b) + c = (a + c) + b` so there\nis no `b + c` term *directly* in the goal.\n\nUse associativity and commutativity to prove `add_right_comm`.\nYou don't need induction. `add_assoc` moves brackets around,\nand `add_comm` moves variables around.\n\nRemember that you can do more targeted rewrites by\nadding explicit variables as inputs to theorems. For example `rw [add_comm b]`\nwill only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\nwill only do rewrites of the form `b + c = c + b`.":
  "`add_comm b c` est une preuve que `b + c = c + b`. Mais si votre but\nest `a + b + c = a + c + b` alors `rw [add_comm b c]` ne\nfonctionnera pas ! Parce que le but signifie `(a + b) + c = (a + c) + b` donc il n'y a\npas de terme `b + c` *directement* dans le but.\n\nUtilisez l'associativité et la commutativité pour prouver `add_right_comm`.\nVous n'avez pas besoin d'induction. `add_assoc` déplace les parenthèses,\net `add_comm` échange les variables.\n\nRappelez-vous que vous pouvez faire des réécritures plus ciblées en\najoutant des variables explicites comme entrées aux théorèmes. Par exemple `rw [add_comm b]`\nne fera que des réécritures de la forme `b + ? = ? + b`, et `rw [add_comm b c]`\nne fera que des réécritures de la forme `b + c = c + b`.",
+ "`add_comm a b` is a proof of `a + b = b + a`.":
+ "`add_comm a b` est une preuve de `a + b = b + a`.",
  "`add_assoc a b c` is a proof\nthat `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\nas `a + b + c`, because the notation for addition is defined to be left\nassociative.":
  "`add_assoc a b c` est une preuve\nque `(a + b) + c = a + (b + c)`. Notez que dans Lean `(a + b) + c` s'affiche\ncomme `a + b + c`, car la notation pour l'addition est définie comme étant\nassociative à gauche.",
  "`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\nmeans \"there exists\". So `a ≤ b` means that there exists\na number `c` such that `b = a + c`. This definition works\nbecause there are no negative numbers in this game.\n\nTo *prove* an \"exists\" statement, use the `use` tactic.\nLet's see an example.":
@@ -277,8 +277,8 @@
  "Pourquoi n'avons-nous pas simplement défini `succ n` comme `n + 1` ? Parce que nous n'avons pas\nencore *défini* l'addition ! Nous ferons cela au niveau suivant.",
  "What do you think of this two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` doesn't just take hypotheses, it will eat any proof which exists\nin the system.":
  "Que pensez-vous de cette solution en deux lignes :\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` ne prend pas seulement des hypothèses, il acceptera toute preuve existante\ndans le système.",
- "Well done! You now have enough tools to tackle the main boss of this level.":
- "Bien joué ! Vous avez maintenant suffisamment d'outils pour affronter le boss principal de ce niveau.",
+ "Well done! You now have enough tools to tackle the main boss of this world.":
+ "Bien joué ! Vous avez maintenant suffisamment d'outils pour affronter le boss principal de ce monde.",
  "Well done!": "Bien joué !",
  "Welcome to tutorial world! In this world we learn the basics\nof proving theorems. The boss level of this world\nis the theorem `2 + 2 = 4`.\n\nYou prove theorems by solving puzzles using tools called *tactics*.\nThe aim is to prove the theorem by applying tactics\nin the right order.\n\nLet's learn some basic tactics. Click on \"Start\" below\nto begin your quest.":
  "Bienvenue dans le monde tutoriel ! Dans ce monde, nous apprenons les bases\nde la preuve de théorèmes. Le niveau boss de ce monde\nest le théorème `2 + 2 = 4`.\n\nVous prouvez des théorèmes en résolvant des énigmes à l'aide d'outils appelés *tactiques*.\nLe but est de prouver le théorème en appliquant des tactiques\ndans le bon ordre.\n\nApprenons quelques tactiques de base. Cliquez sur \"Commencer\" ci-dessous\npour débuter votre quête.",
@@ -309,12 +309,12 @@
  "We now start work on an algorithm to do addition more efficiently. Recall that\nwe defined addition by recursion, saying what it did on `0` and successors.\nIt is an axiom of Lean that recursion is a valid\nway to define functions from types such as the naturals.\n\nLet's define a new function `pred` from the naturals to the naturals, which\nattempts to subtract 1 from the input. The definition is this:\n\n```\npred 0 := 37\npred (succ n) := n\n```\n\nWe cannot subtract one from 0, so we just return a junk value. As well as this\ndefinition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\nLet's use this lemma to prove `succ_inj`, the theorem which\nPeano assumed as an axiom and which we have already used extensively without justification.":
  "Nous commençons maintenant à travailler sur un algorithme pour faire l'addition plus efficacement. Rappelons que\nnous avons défini l'addition par une formule de récurrence, en disant ce qu'elle fait sur `0` et les successeurs.\nC'est un axiome de Lean que la récursion est une manière valide\nde définir des fonctions à partir de types comme les naturels.\n\nDéfinissons une nouvelle fonction `pred` des naturels vers les naturels, qui\ntente de soustraire 1 de l'entrée. La définition est :\n\n```\npred 0 := 37\npred (succ n) := n\n```\n\nNous ne pouvons pas soustraire un de 0, donc nous renvoyons simplement une valeur quelconque. En plus de cette\ndéfinition, nous créons également un nouveau lemme `pred_succ`, qui dit que `pred (succ n) = n`.\nUtilisons ce lemme pour prouver `succ_inj`, le théorème que\nPeano a supposé comme axiome et que nous avons déjà largement utilisé sans justification.",
  "We now have enough to state a mathematically accurate, but slightly\nclunky, version of Fermat's Last Theorem.\n\nFermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\\not =z^m$.\nIf you didn't do inequality world yet then we can't talk about $m \\geq 3$,\nso we have to resort to the hack of using `n + 3` for `m`,\nwhich guarantees it's big enough. Similarly instead of `x > 0` we\nuse `a + 1`.\n\nThis level looks superficially like other levels we have seen,\nbut the shortest solution known to humans would translate into\nmany millions of lines of Lean code. The author of this game,\nKevin Buzzard, is working on translating the proof by Wiles\nand Taylor into Lean, although this task will take many years.\n\n## CONGRATULATIONS!\n\nYou've finished the main quest of the natural number game!\nIf you would like to learn more about how to use Lean to\nprove theorems in mathematics, then take a look\nat [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\nan interactive textbook which you can read in your browser,\nand which explains how to work with many more mathematical concepts in Lean.":
- "Nous avons maintenant suffisamment de connaissance pour énoncer une version mathématiquement exacte, mais un peu\nmaladroite, du \"grand théorème de Fermat\".\n\nLe dernier théorème de Fermat énonce que si $x,y,z>0$ et $m \\geq 3$ alors $x^m+y^m\\not =z^m$.\nSi vous n'avez pas encore fait le monde des inégalités, nous ne pouvons pas parler de $m \\geq 3$,\nnous devons donc recourir à l'astuce d'utiliser `n + 3` pour `m`,\nce qui garantit qu'il est assez grand. De même, au lieu de `x > 0` nous\nutilisons `a + 1`.\n\nCe niveau ressemble superficiellement à d'autres niveaux que nous avons vus,\nmais la solution la plus courte connue des humains se traduirait par\nplusieurs millions de lignes de code Lean. L'auteur de ce jeu,\nKevin Buzzard, travaille à traduire la preuve de Wiles\net Taylor dans Lean, même si cette tâche prendra de nombreuses années.\n\n## FÉLICITATIONS !\n\nVous avez terminé la quête principale du jeu des nombres naturels !\nSi vous souhaitez en savoir plus sur l'utilisation de Lean pour\nprouver des théorèmes en mathématiques, jetez un œil\nà [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\nun manuel interactif que vous pouvez lire dans votre navigateur,\net qui explique comment travailler avec beaucoup d'autres concepts mathématiques dans Lean.",
+ "Nous avons maintenant suffisamment de connaissances pour énoncer une version mathématiquement exacte, mais un peu\nmaladroite, du \"grand théorème de Fermat\".\n\nLe dernier théorème de Fermat énonce que si $x,y,z>0$ et $m \\geq 3$ alors $x^m+y^m\\not =z^m$.\nSi vous n'avez pas encore fait le monde des inégalités, nous ne pouvons pas parler de $m \\geq 3$,\nnous devons donc recourir à l'astuce d'utiliser `n + 3` pour `m`,\nce qui garantit qu'il est assez grand. De même, au lieu de `x > 0` nous\nutilisons `a + 1`.\n\nCe niveau ressemble superficiellement à d'autres niveaux que nous avons vus,\nmais la solution la plus courte connue des humains se traduirait par\nplusieurs millions de lignes de code Lean. L'auteur de ce jeu,\nKevin Buzzard, travaille à traduire la preuve de Wiles\net Taylor dans Lean, même si cette tâche prendra de nombreuses années.\n\n## FÉLICITATIONS !\n\nVous avez terminé la quête principale du jeu des nombres naturels !\nSi vous souhaitez en savoir plus sur l'utilisation de Lean pour\nprouver des théorèmes en mathématiques, jetez un œil\nà [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\nun manuel interactif que vous pouvez lire dans votre navigateur,\net qui explique comment travailler avec beaucoup d'autres concepts mathématiques dans Lean.",
  "We now have enough to prove that multiplication is associative,\nthe boss level of multiplication world. Good luck!":
  "Nous avons maintenant assez de matière pour prouver que la multiplication est associative,\nle niveau boss du monde de la multiplication. Bonne chance !",
  "We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\nif we have a hypothesis `succ n = 0`? It's the wrong way around!\n\nThe `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\nto `y ≠ x`. And `symm at h`\ndoes the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\nthe proof `zero_ne_one`; now try proving $1 \\neq 0$.":
  "Nous savons que `zero_ne_succ n` est une preuve de `0 = succ n → False` -- mais que faire\nsi nous avons une hypothèse `succ n = 0` ? C'est dans le mauvais sens !\n\nLa tactique `symm` change un but `x = y` en `y = x`, et un but `x ≠ y`\nen `y ≠ x`. Et `symm at h`\nfait la même chose pour une hypothèse `h`. Nous avons prouvé $0 \\neq 1$ et nous avions appelé\nla preuve `zero_ne_one` ; maintenant essayez de prouver $1 \\neq 0$.",
- "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\nin Lean. We do this with the `intro` tactic.":
+ "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".\nIn Lean, we do this with the `intro` tactic.":
  "Nous avons vu comment utiliser `apply` sur des théorèmes et des hypothèses\nde la forme `P → Q`. Mais que faire si notre *but* est de la forme `P → Q` ?\nPour prouver ce but, nous devons savoir dire \"supposons `P` et déduisons `Q`\"\ndans Lean. Nous faisons cela avec la tactique `intro`.",
  "We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.":
  "Nous avons donné une preuve assez peu satisfaisante de `2 + 2 ≠ 5` plus tôt ; maintenant donnez-en une meilleure.",
@@ -344,7 +344,7 @@
  "Ce monde introduit l'exponentiation. Si vous voulez définir `37 ^ n`\nalors, comme toujours, vous devrez savoir ce que vaut `37 ^ 0`, et\nce que vaut `37 ^ (succ d)`, sachant seulement `37 ^ d`.\n\nVous pouvez probablement deviner les noms des théorèmes généraux :\n\n  * `pow_zero (a : ℕ) : a ^ 0 = 1`\n  * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n\nEn utilisant uniquement ceux-ci, pourrez-vous passer le niveau boss final ?\n\nLes niveaux de ce monde ont été conçus par Sian Carey, une étudiante UROP\nà l'Imperial College de Londres, financée par une bourse Mary Lister McCammon\ndurant l'été 2019. Merci à Sian et également à Imperial\nCollege pour l'avoir financée.",
  "This time, use the `left` tactic.":
  "Cette fois, utilisez la tactique `left`.",
- "This state is not provable! Did you maybe use `rw [add_left_eq_self] at h`\ninstead of `apply [add_left_eq_self] at h`? You can compare the two in the inventory.":
+ "This state is not provable! Did you maybe use `rw [add_left_eq_self] at h`\ninstead of `apply [add_left_eq_self] at h`? You can complare the two in the inventory.":
  "Cet état n'est pas prouvable ! Avez-vous peut-être utilisé `rw [add_left_eq_self] at h`\nau lieu de `apply [add_left_eq_self] at h` ? Vous pouvez comparer les deux dans l'inventaire.",
  "This level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy\nis to write both `a` and `b` as `succ` of something, deduce that `a * b` is\nalso `succ` of something, and then `apply zero_ne_succ`.":
  "Ce niveau prouve que si `a ≠ 0` et `b ≠ 0` alors `a * b ≠ 0`. Une stratégie\nconsiste à écrire `a` et `b` comme `succ` de quelque chose, à déduire que `a * b` est\naussi `succ` de quelque chose, puis à `apply zero_ne_succ`.",
@@ -450,7 +450,7 @@
  "Notre premier défi est `mul_comm x y : x * y = y * x`,\net nous voulons le prouver par induction. Le cas\nzéro aura besoin de `mul_zero` (que nous avons)\net de `zero_mul` (que nous n'avons pas), donc commençons\npar cela.",
  "One of the best named levels in the game, a savage `pow_pow`\nsub-boss appears as the music reaches a frenzy. What\nelse could there be to prove about powers after this?":
  "L'un des niveaux les mieux nommés du jeu, un sous-boss féroce `pow_pow` \napparaît alors que la musique atteint son paroxysme. Que\npourrait-il y avoir d'autre à prouver sur les puissances après cela ?",
- "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42.$\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
+ "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42$.\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
  "Un jour, ce jeu aura un monde des Nombres Premiers, avec un boss final\nprouvant que $2$ est premier.\nPour cela, nous devrons exclure des choses comme $2 = 37 × 42$.\nNous ferons cela en prouvant que tout facteur de $2$ est au plus $2$,\nen utilisant ce lemme. La preuve que j'ai en tête manipule l'hypothèse\njusqu'à ce qu'elle devienne le but, en utilisant `mul_left_ne_zero`, `one_le_of_ne_zero` et\n`mul_le_mul_right`.",
  "On the set of natural numbers, addition is commutative.\nIn other words, if `a` and `b` are arbitrary natural numbers, then\n$a + b = b + a$.":
  "Sur l'ensemble des nombres naturels, l'addition est commutative.\nAutrement dit, si `a` et `b` sont des nombres naturels arbitraires, alors\n$a + b = b + a$.",
@@ -532,6 +532,8 @@
  "Ma preuve :\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```",
  "Multiplication usually makes a number bigger, but multiplication by zero can make\nit smaller. Thus many lemmas about inequalities and multiplication need the\nhypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.\nTo help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\non the right to see what it does.":
  "La multiplication transforme généralement un nombre en un nombre plus grand, mais la multiplication par zéro peut le rendre\nplus petit. Ainsi, de nombreux lemmes sur les inégalités et la multiplication nécessitent l'\nhypothèse `a ≠ 0`. Voici un lemme clé qui nous permet d'utiliser cette hypothèse.\nPour la preuve, nous pouvons utiliser la tactique `tauto`. Cliquez sur le nom de la tactique\nà droite pour voir ce qu'elle fait.",
+ "Multiplication is distributive over addition.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
+ "La multiplication est distributive sur l'addition.\nAutrement dit, pour tous les nombres naturels $a$, $b$ et $c$, nous avons\n$(a + b) \\times c = ac + bc$.",
  "Multiplication is distributive over addition on the left.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$a(b + c) = ab + ac$.":
  "La multiplication est distributive sur l'addition à gauche.\nAutrement dit, pour tous les nombres naturels $a$, $b$ et $c$, nous avons\n$a(b + c) = ab + ac$.",
  "Multiplication is commutative.": "La multiplication est commutative.",
@@ -592,7 +594,7 @@
  "Dans ce jeu, vous recréez les nombres naturels $\\mathbb{N}$ à partir des axiomes de Peano,\nen apprenant les bases de la preuve de théorèmes dans Lean.\n\nC'est une excellente première introduction à Lean !",
  "In the next level, we'll do the same proof but backwards.":
  "Dans le niveau suivant, nous ferons la même preuve mais à l'envers.",
- "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  command line mode).":
+ "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  \"Typewriter mode\").":
  "Dans le dernier niveau, nous avons manipulé l'hypothèse `x + 1 = 4`\n  jusqu'à ce qu'elle devienne le but `x = 3`. Dans ce niveau, nous manipulerons\n  le but jusqu'à ce qu'il devienne notre hypothèse ! Autrement dit, nous\n  \"argumenterons à l'envers\". La tactique `apply` peut aussi faire cela.\n  Je vais encore vous guider à travers celui-ci (en supposant que vous êtes en\n  mode ligne de commande).",
  "In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\nfrom a false statement. The `tauto` tactic will close this goal.":
  "Dans le \"cas de base\", nous avons une hypothèse `ha : 0 ≠ 0`, et vous pouvez déduire n'importe quoi\nd'un énoncé faux. La tactique `tauto` fermera ce but.",
@@ -744,9 +746,9 @@
  "Fermat's Last Theorem": "Grand théorème de Fermat",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Chaque nombre dans Lean est soit $0$, soit un successeur. Nous savons comment ajouter $0$,\nmais nous devons comprendre comment ajouter des successeurs. Disons que nous savons déjà\nque `37 + d = q`. Que devrait être la réponse à `37 + succ d` ? Eh bien,\n`succ d` est un de plus que `d`, donc `37 + succ d` devrait être `succ q`,\nle nombre un de plus que `q`. Plus généralement, `x + succ d` devrait\nêtre `succ (x + d)`. Ajoutons cela comme lemme.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nSi vous voyez `... + succ ...` dans votre but, `rw [add_succ]` est\ngénéralement une bonne idée.\n\nProuvons maintenant que `succ n = n + 1`. Trouvez comment introduire `+ succ`\ndans notre situation, puis `rw [add_succ]`. Alternez entre les onglets `+` (addition) et\n`012` (numéraux) sous \"Théorèmes\" à droite pour\nvoir quelles preuves vous pouvez réécrire.",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet.":
  "Faites-le encore !\n\n`rw [zero_add] at «{h}»` essaie de remplir\nles arguments de `zero_add` (trouvant `«{x}»`) puis remplace toutes les occurrences de\n`0 + «{x}»` qu'il trouve. Par conséquent, il n'a pas réécrit `0 + «{y}»` pour l'instant.",
- "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
+ "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to \"Typewriter mode\".\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "Avez-vous utilisé l'induction sur `y` ?\nVoici une preuve en deux lignes de `add_left_eq_self` qui utilise `add_right_cancel`.\nSi vous voulez l'inspecter, vous pouvez passer en mode éditeur en cliquant sur `</>` en haut à droite\npuis copier et coller la preuve et déplacer votre curseur autour\npour voir les hypothèses et le but à n'importe quel point\n(bien que vous perdiez ainsi votre propre preuve). Cliquez sur `>_` pour\nrevenir en mode ligne de commande.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
  "Dealing with `or`": "Gérer `or`",
  "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World (when someone gets around to\nimplementing it).":
@@ -787,8 +789,6 @@
  "Advanced Addition World": "Monde de l'Addition Avancée",
  "Advanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts about multiplication, such as `x * y = 1 → x = 1`, and\n`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.":
  "Le Monde de l'Addition Avancée a prouvé diverses implications\nimpliquant l'addition, telles que `x + y = 0 → x = 0` et `x + y = x → y = 0`.\nCes lemmes ont été utilisés pour prouver des faits de base sur ≤ dans le Monde ≤.\n\nDans le Monde de la Multiplication Avancée, nous prouvons des résultats\nanalogues sur la multiplication, tels que `x * y = 1 → x = 1`, et\n`x * y = x → y = 1` (en supposant `x ≠ 0` pour ce dernier résultat). Cela nous préparera\nau Monde de la Divisibilité.\n\nLe Monde de la Multiplication est plus complexe que le Monde de l'Addition. De la même\nmanière, le Monde de la Multiplication Avancée est plus complexe que le Monde de l'Addition Avancée.\nUne raison est que certains résultats intermédiaires ne sont vrais\nque sous l'hypothèse supplémentaire qu'une des variables est non nulle.\nCela crée des complications inattendues.",
- "Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
- "L'addition est distributive sur la multiplication.\nAutrement dit, pour tous les nombres naturels $a$, $b$ et $c$, nous avons\n$(a + b) \\times c = ac + bc$.",
  "Addition World": "Monde de l'Addition",
  "Adding zero": "Ajouter zéro",
  "A two-line proof is\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nWe now have all the tools necessary to set up the basic theory of divisibility of naturals.":
@@ -877,4 +877,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "# Aperçu\n\nNotre tactique maison `simp_add` résoudra tout but de\nla forme `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "# Aperçu\n\nLe simplificateur de Lean, `simp`, réécrira chaque lemme\nmarqué `simp` et chaque lemme fourni par l'utilisateur, autant que possible.\nDe plus, il tentera d'ordonner les variables dans un ordre interne si on lui donne\ndes lemmes comme `add_comm`, afin de ne pas tomber dans une boucle infinie."}
+ "# Aperçu\n\nLe simplificateur de Lean, `simp`, réécrira chaque lemme\nmarqué `simp` et chaque lemme fourni par l'utilisateur, autant que possible.\nDe plus, il tentera d'ordonner les variables dans un ordre interne si on lui donne\ndes lemmes comme `add_comm`, afin de ne pas tomber dans une boucle infinie."}
\ No newline at end of file
diff --git a/.i18n/fr/Game.po b/.i18n/fr/Game.po
index 5960fc57..19c20097 100644
--- a/.i18n/fr/Game.po
+++ b/.i18n/fr/Game.po
@@ -1263,10 +1263,10 @@ msgstr ""
 "sur n'importe quel `succ` dans le but ou les hypothèses pour voir exactement ce qu'il prend."
 
 #: Game.Levels.Addition.L02succ_add
-msgid "Well done! You now have enough tools to tackle the main boss of this level."
+msgid "Well done! You now have enough tools to tackle the main boss of this world."
 msgstr ""
 "Bien joué ! Vous avez maintenant suffisamment d'outils pour affronter le boss principal de ce "
-"niveau."
+"monde."
 
 #: Game.Levels.Addition.L03add_comm
 msgid "add_comm (level boss)"
@@ -1822,11 +1822,11 @@ msgstr "`add_mul a b c` est une preuve que $(a+b)c=ac+bc$."
 
 #: Game.Levels.Multiplication.L08add_mul
 msgid ""
-"Addition is distributive over multiplication.\n"
+"Multiplication is distributive over addition.\n"
 "In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
 "$(a + b) \\times c = ac + bc$."
 msgstr ""
-"L'addition est distributive sur la multiplication.\n"
+"La multiplication est distributive sur l'addition.\n"
 "Autrement dit, pour tous les nombres naturels $a$, $b$ et $c$, nous avons\n"
 "$(a + b) \\times c = ac + bc$."
 
@@ -2448,7 +2448,7 @@ msgid ""
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n"
-"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+"`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "Faites-le encore !\n"
 "\n"
@@ -2703,7 +2703,7 @@ msgid ""
 "  the goal until it becomes our hypothesis! In other words, we\n"
 "  will \"argue backwards\". The `apply` tactic can do this too.\n"
 "  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+"  \"Typewriter mode\")."
 msgstr ""
 "Dans le dernier niveau, nous avons manipulé l'hypothèse `x + 1 = 4`\n"
 "  jusqu'à ce qu'elle devienne le but `x = 3`. Dans ce niveau, nous manipulerons\n"
@@ -2784,8 +2784,8 @@ msgstr ""
 msgid ""
 "We have seen how to `apply` theorems and assumptions\n"
 "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
-"To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\n"
-"in Lean. We do this with the `intro` tactic."
+"To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".\n"
+"In Lean, we do this with the `intro` tactic."
 msgstr ""
 "Nous avons vu comment utiliser `apply` sur des théorèmes et des hypothèses\n"
 "de la forme `P → Q`. Mais que faire si notre *but* est de la forme `P → Q` ?\n"
@@ -3841,11 +3841,11 @@ msgstr "$x + y = y\\implies x=0.$"
 msgid ""
 "Did you use induction on `y`?\n"
 "Here's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\n"
-"If you want to inspect it, you can go into editor mode by clicking `</>` in the top right\n"
+"If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right\n"
 "and then just cut and paste the proof and move your cursor around it\n"
 "to see the hypotheses and goal at any given point\n"
 "(although you'll lose your own proof this way). Click `>_` to get\n"
-"back to command line mode.\n"
+"back to \"Typewriter mode\".\n"
 "```\n"
 "nth_rewrite 2 [← zero_add y]\n"
 "exact add_right_cancel x 0 y\n"
@@ -5042,7 +5042,7 @@ msgstr ""
 msgid ""
 "One day this game will have a Prime Number World, with a final boss\n"
 "of proving that $2$ is prime.\n"
-"To do this, we will have to rule out things like $2 = 37 × 42.$\n"
+"To do this, we will have to rule out things like $2 = 37 × 42$.\n"
 "We will do this by proving that any factor of $2$ is at most $2$,\n"
 "which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n"
 "until it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n"
diff --git a/.i18n/it/Game.json b/.i18n/it/Game.json
index 1fe5aa5d..18fa3b48 100644
--- a/.i18n/it/Game.json
+++ b/.i18n/it/Game.json
@@ -219,10 +219,10 @@
  "`add_left_cancel a b n` è il teorema che dice $n+a=n+b\\implies a=b$.\nPuoi dimostrarlo facendo induzione su `n` oppure puoi dedurlo tramite `add_right_cancel`.",
  "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$":
  "`add_left_cancel a b n` è il teorema $n+a=n+b \\implies a=b.$",
- "`add_comm a b` is a proof of `a + b = b + a`.":
- "`add_comm a b` è la dimostrazione di `a + b = b + a`.",
  "`add_comm b c` is a proof that `b + c = c + b`. But if your goal\nis `a + b + c = a + c + b` then `rw [add_comm b c]` will not\nwork! Because the goal means `(a + b) + c = (a + c) + b` so there\nis no `b + c` term *directly* in the goal.\n\nUse associativity and commutativity to prove `add_right_comm`.\nYou don't need induction. `add_assoc` moves brackets around,\nand `add_comm` moves variables around.\n\nRemember that you can do more targeted rewrites by\nadding explicit variables as inputs to theorems. For example `rw [add_comm b]`\nwill only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\nwill only do rewrites of the form `b + c = c + b`.":
  "`add_comm b c` è una dimostrazione di `b + c = c + b`. Ma se il goal\nè `a + b + c = a + c + b`, `rw [add_comm b c]` non funzionerà!\nQuesto perché il goal sta in realtà per `(a + b) + c = (a + c) + b`, e se guardi bene questo goal non include\nil termine `b + c` *direttamente*.\n\nUsa l'associatività e la commutatività per dimostrare `add_right_comm`.\nNon è necessario procedere per induzione. `add_assoc` sposta le parentesi,\ne `add_comm` sposta le variabili.\n\nRicorda che puoi fare sostituzioni mirate fornendo\nesplicitamente le variabili in input ai teoremi. Ad esempio `rw [add_comm b]`\nfarà solo sostituzioni della forma `b + ? = ? + b`, e `rw [add_comm b c]`\nfarà solo sostituzioni della forma `b + c = c + b`.",
+ "`add_comm a b` is a proof of `a + b = b + a`.":
+ "`add_comm a b` è la dimostrazione di `a + b = b + a`.",
  "`add_assoc a b c` is a proof\nthat `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\nas `a + b + c`, because the notation for addition is defined to be left\nassociative.":
  "`add_assoc a b c` è la dimostrazione\ndi `(a + b) + c = a + (b + c)`. Ricordati che in Lean `(a + b) + c` viene\nstampato come `a + b + c`, perché la notazione dell'addizione è left \nassociative.",
  "`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\nmeans \"there exists\". So `a ≤ b` means that there exists\na number `c` such that `b = a + c`. This definition works\nbecause there are no negative numbers in this game.\n\nTo *prove* an \"exists\" statement, use the `use` tactic.\nLet's see an example.":
@@ -277,7 +277,7 @@
  "Come mai non abbiamo definito `succ n` semplicemente come `n + 1`? Perché non abbiamo\nancora *definito* il concetto di addizione! Provvederemo nel prossimo livello.",
  "What do you think of this two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` doesn't just take hypotheses, it will eat any proof which exists\nin the system.":
  "Guarda il mio two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` non prende soltanto ipotesi, puoi passargli qualsiasi dimostrazione\ndefinita nel gioco.",
- "Well done! You now have enough tools to tackle the main boss of this level.":
+ "Well done! You now have enough tools to tackle the main boss of this world.":
  "Ottimo lavoro! Ora sei abbastanza pratico per affrontare il boss principale di questo mondo.",
  "Well done!": "Ottimo lavoro!",
  "Welcome to tutorial world! In this world we learn the basics\nof proving theorems. The boss level of this world\nis the theorem `2 + 2 = 4`.\n\nYou prove theorems by solving puzzles using tools called *tactics*.\nThe aim is to prove the theorem by applying tactics\nin the right order.\n\nLet's learn some basic tactics. Click on \"Start\" below\nto begin your quest.":
@@ -314,7 +314,7 @@
  "Adesso abbiamo abbastanza informazioni per dimostrare che la moltiplicazione è associativa,\nil boss del Mondo Moltiplicazione. Avanti guerriero!",
  "We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\nif we have a hypothesis `succ n = 0`? It's the wrong way around!\n\nThe `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\nto `y ≠ x`. And `symm at h`\ndoes the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\nthe proof `zero_ne_one`; now try proving $1 \\neq 0$.":
  "Abbiamo visto che `zero_ne_succ n` è la dimostrazione di `0 = succ n → False` --  ma come possiamo applicarla\nall'ipotesi `succ n = 0`? È la stessa uguaglianza, solo con i due lati scambiati!\n\nLa tattica `symm` ci viene in soccorso: riscrive un goal `x = y` in `y = x`, e un goal `x ≠ y`\nin `y ≠ x`. `symm at h`\nè la versione che opera sull'ipotesi `h`. Abbiamo dimostrato poco fa $0 \\neq 1$ e chiamato\nla sua dimostrazione `zero_ne_one`; ora prova a dimostrare $1 \\neq 0$.",
- "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\nin Lean. We do this with the `intro` tactic.":
+ "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".\nIn Lean, we do this with the `intro` tactic.":
  "Abbiamo visto come fare `apply` di teoremi e ipotesi\ndella forma `P → Q`. Ma come ci comportiamo se è il *goal* ad avere la forma `P → Q`?\nPer dimostrare questo tipo di goal, ci serve un modo per dire a Lean \"supponiamo `P` e deduciamo `Q`\".\nLo possiamo fare con la tattica `intro`.",
  "We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.":
  "La dimostrazione che abbiamo dato prima per `2 + 2 ≠ 5` non è stata molto elegante; danne una più carina.",
@@ -448,8 +448,8 @@
  "La prima sfida è dimostrare `mul_comm x y : x * y = y * x`,\ne vogliamo farlo per induzione. Per dimostrare il caso\nbase utilizzeremo `mul_zero` (che abbiamo come assioma)\ne `zero_mul`, che non abbiamo ancora, dunque partiamo\nda quest'ultimo.",
  "One of the best named levels in the game, a savage `pow_pow`\nsub-boss appears as the music reaches a frenzy. What\nelse could there be to prove about powers after this?":
  "Con il suo nome accattivante, il mini-boss `pow_pow`\nsalta nel ring e la musica si fa ancora più intensa. Cos'altro c'è da\ndimostrare sulle potenze dopo di lui?!",
- "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42.$\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
- "Un giorno questo gioco avrà il Mondo Numeri Primi, il cui boss finale\nsarà dimostrare che $2$ è un numero primo.\nMa per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42.$\nLo faremo dimostrando che ogni fattore di $2$ è al più $2$,\nche avremo gratis grazie a questo lemma. La dimostrazione che ho in mente io manipola l'ipotesi finché\nnon ha la forma del goal, usando `mul_left_ne_zero`, `one_le_of_ne_zero` e\n`mul_le_mul_right`.",
+ "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42$.\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
+ "Un giorno questo gioco avrà il Mondo Numeri Primi, il cui boss finale\nsarà dimostrare che $2$ è un numero primo.\nMa per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42$.\nLo faremo dimostrando che ogni fattore di $2$ è al più $2$,\nche avremo gratis grazie a questo lemma. La dimostrazione che ho in mente io manipola l'ipotesi finché\nnon ha la forma del goal, usando `mul_left_ne_zero`, `one_le_of_ne_zero` e\n`mul_le_mul_right`.",
  "On the set of natural numbers, addition is commutative.\nIn other words, if `a` and `b` are arbitrary natural numbers, then\n$a + b = b + a$.":
  "L'addizione è commutativa sull'insieme dei naturali.\nEquivalentemente, se `a` e `b` sono due numeri naturali qualsiasi, allora\n$a + b = b + a$.",
  "On the set of natural numbers, addition is associative.\nIn other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n$ (a + b) + c = a + (b + c). $":
@@ -528,6 +528,8 @@
  "La mia dimostrazione:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```",
  "Multiplication usually makes a number bigger, but multiplication by zero can make\nit smaller. Thus many lemmas about inequalities and multiplication need the\nhypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.\nTo help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\non the right to see what it does.":
  "La moltiplicazione normalmente fa crescere un numero, ma moltiplicare per zero lo rende\npiù piccolo, o meglio, lo azzera. Ecco perché gran parte dei teoremi che mischiano le disuguaglianze con la moltiplicazione necessitano\nl'ipotesi `a ≠ 0`. Questo livello è un lemma chiave che ci permette di mettere a frutto questa ipotesi.\nPer aiutarci nella dimostrazione, possiamo usare la tattica `tauto`. Clicca sul nome della tattica\nsulla destra per una descrizione dettagliata di cosa fa.",
+ "Multiplication is distributive over addition.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
+ "La moltiplicazione gode della proprietà distributiva sull'addizione.\nEquivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n$(a + b) \\times c = ac + bc$.",
  "Multiplication is distributive over addition on the left.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$a(b + c) = ab + ac$.":
  "La moltiplicazione è distributiva a sinistra rispetto all'addizione.\nEquivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n$a(b + c) = ab + ac$.",
  "Multiplication is commutative.": "La moltiplicazione è commutativa.",
@@ -586,7 +588,7 @@
  "In questo gioco ricreerai l'insieme dei numeri naturali $\\mathbb{N}$ partendo dagli assiomi di Peano,\ne lungo il percorso imparerai le basi del *theorem proving* su Lean.\n\nQuesto gioco è un'ottima introduzione a Lean!",
  "In the next level, we'll do the same proof but backwards.":
  "Nel livello successivo, dimostreremo lo stesso enunciato, al contrario.",
- "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  command line mode).":
+ "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  \"Typewriter mode\").":
  "Nell'ultimo livello abbiamo manipolato l'ipotesi `x + 1 = 4`\n  per farla coincidere con il goal `x = 3`. In questo livello manipoleremo\n  il goal per farlo combaciare con una delle ipotesi! Si puo dire che\n  \"ragioneremo all'indietro\". È ancora la tattica `apply` che ce lo consente.\n  Ti guiderò io anche in questa dimostrazione (assicurati di essere in modalità\n  interattiva).",
  "In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\nfrom a false statement. The `tauto` tactic will close this goal.":
  "Nel \"caso base\" abbiamo un'ipotesi `ha : 0 ≠ 0`, e sappiamo che puoi dedurre qualsiasi cosa\nda una proposizione falsa. La tattica `tauto` chiuderà il goal.",
@@ -738,9 +740,9 @@
  "Fermat's Last Theorem": "L'ultimo teorema di Fermat",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Ogni numero in Lean è $0$ oppure il successore di un altro numero. Abbiamo già visto come aggiungere $0$,\ne ci rimane da capire come aggiungere un successore. Ipotizziamo di sapere\nche vale l'uguaglianza `37 + d = q`. A cosa dovrebbe essere uguale `37 + succ d`? Beh,\n`succ d` è un'unità più grande di `d`, quindi `37 + succ d` dovrebbe essere `succ q`,\nossia un'unità più grande di `q`. In generale `x + succ d` dovrebbe\ndare `succ (x + d)`. Formalizziamo questo ragionamento in un lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nQuando vedi `... + succ ...` nel goal, eseguire `rw [add_succ]` è una\nbuona idea.\n\nDimostriamo ora che `succ n = n + 1`. Cerca di introdurre un `+ succ` nel\ngoal, poi esegui `rw [add_succ]`. Controlla entrambi i tab `+` (addizione) e\n`012` (numeri) nella sezione \"Teoremi\" a destra\nper vedere quali teoremi da riscrivere hai a disposizione.",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet.":
  "Ripeti lo stesso comando!\n\n`rw [zero_add] at «{h}»` ha completato automaticamente\nla chiamata a `zero_add` (trovando l'argomento `«{x}»`) e poi ha sostituito tutte le occorrenze di\n`0 + «{x}»` in un solo colpo. Dunque non ha toccato `0 + «{y}»` ancora, perciò dovresti ripetere il comando.",
- "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
+ "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to \"Typewriter mode\".\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "Per caso hai fatto induzione su `y`?\nEcco una dimostrazione in due righe `add_left_eq_self` che sfrutta `add_right_cancel`.\nSe vuoi vedere come funziona, vai in editor mode cliccando su `</>` in alto a destra,\ncopia e incolla la mia dimostrazione e muoviti tra le linee con il cursore\nper vedere le ipotesi e il goal in ogni punto\n(prima salva la tua dimostrazione però, altrimenti la perdi). Premi su `>_` per\ntornare alla modalità command line.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
  "Dealing with `or`": "Come ragionare con `or`",
  "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World (when someone gets around to\nimplementing it).":
@@ -781,8 +783,6 @@
  "Advanced Addition World": "Mondo Addizione Avanzata",
  "Advanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts about multiplication, such as `x * y = 1 → x = 1`, and\n`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.":
  "Nel Mondo *Addizione* Avanzata abbiamo dimostrato varie implicazioni\nsull'addizione, ad esempio `x + y = 0 → x = 0` e `x + y = x → y = 0`.\nIn seguito abbiamo usato questi lemmi per dimostrare fatti basilari su ≤ nel Mondo ≤.\n\nNel Mondo Moltiplicazione Avanzata dimostreremo dei fatti\nanaloghi sulla moltiplicazione, ad esempio `x * y = 1 → x = 1`, e\n`x * y = x → y = 1` (assumendo che `x ≠ 0` nel secondo enunciato). Questi saranno propedeutici\nper il Mondo Divisibilità.\n\nIl Mondo Moltiplicazione è più complesso del Mondo Addizione. Allo stesso modo,\nil Mondo Moltiplicazione Avanzata è più complesso del Mondo Addizione Avanzata.\nLa maggiore complessità di questo mondo è dovuta al fatto che certi teoremi valgono a condizione che una delle variabili non possa assumere il valore zero (sia non-nulla).\nQuesto ulteriore vincolo ha dei risvolti inaspettati.",
- "Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
- "L'addizione gode della proprietà distributiva sulla moltiplicazione.\nEquivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n$(a + b) \\times c = ac + bc$.",
  "Addition World": "Mondo Addizione",
  "Adding zero": "Sommare zero",
  "A two-line proof is\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nWe now have all the tools necessary to set up the basic theory of divisibility of naturals.":
@@ -803,8 +803,8 @@
  "2 + 2 ≠ 5": "2 + 2 ≠ 5",
  "1 ≠ 0": "1 ≠ 0",
  "0 ≤ x": "0 ≤ x",
- "*Game version: 4.3*\n\n*Recent additions: bug fixes*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
- "*Versione del gioco: 4.2*\n\n*Aggiunti di recente: rimozione di bug*\n\n## Salvataggio del gioco\n\nIl gioco salva il tuo progresso nella memoria locale del browser.\nSe svuoti la memoria del browser, perderai anche i dati del gioco! (le tue preziose dimostrazioni!)\n\nAttenzione: nella maggior parte dei browser, eliminando i cookies si elimina anche la memoria di un sito\n(o \"i dati locali del sito\"). In ogni caso, assicurati di esportare il tuo progresso del gioco!\n\n## Riconoscimenti\n\n* **Autori:** Kevin Buzzard, Jon Eugster\n* **Versione originale per Lean3:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Livelli extra:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Traduzione italiana**: Federico Dal Pio Luogo\n* **Grazie anche a:** Gli studenti che si sono offerti come beta testers, tutte le scuole\nche hanno invitato Kevin a parlare, e gli studenti che gli hanno fatto domande\nsul materiale.\n\n## Risorse\n\n* La [chat di Lean su Zulip](https://leanprover.zulipchat.com/)\n* Il [gioco originale per Lean3](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n\n## Problemi?\n\nRivolgi le tue domande sul gioco nella\n[chat di Lean su Zulip](https://leanprover.zulipchat.com/), utilizzando\nlo stream \"New Members\". I membri della comunità sono felici di aiutare. Nota che\nla chat di Lean su Zulip è un forum professionale di ricerca.\nPerciò usa il tuo nome reale e per intero, rimani in tema, e sii cortese. Se cerchi\nun forum più informale (dove puoi ad esempio postare\ni meme sui numeri naturali) allora il [server Discord di Lean](https://discord.gg/WZ9bs9UCvx) fa per te.\n\nIn alternativa, se il gioco funziona male o dovessi trovare un bug puoi aprire una issue su github:\n\n* Per problemi relativi al game engine, apri una\n[issue sul repo lean4game](https://github.com/leanprover-community/lean4game/issues).\n* Per problemi relativi ai contenuti del the gioco, apri una\n[issue sul repo NNG](https://github.com/hhu-adam/NNG4/issues).",
+ "*Game version: 4.3*\n\n*Recent additions: bug fixes*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
+ "*Versione del gioco: 4.2*\n\n*Aggiunti di recente: rimozione di bug*\n\n## Salvataggio del gioco\n\nIl gioco salva il tuo progresso nella memoria locale del browser.\nSe svuoti la memoria del browser, perderai anche i dati del gioco! (le tue preziose dimostrazioni!)\n\nAttenzione: nella maggior parte dei browser, eliminando i cookies si elimina anche la memoria di un sito\n(o \"i dati locali del sito\"). In ogni caso, assicurati di esportare il tuo progresso del gioco!\n\n## Riconoscimenti\n\n* **Autori:** Kevin Buzzard, Jon Eugster\n* **Versione originale per Lean3:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Livelli extra:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Traduzione italiana**: Federico Dal Pio Luogo\n* **Grazie anche a:** Gli studenti che si sono offerti come beta testers, tutte le scuole\nche hanno invitato Kevin a parlare, e gli studenti che gli hanno fatto domande\nsul materiale.\n\n## Risorse\n\n* La [chat di Lean su Zulip](https://leanprover.zulipchat.com/)\n* Il [gioco originale per Lean3](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problemi?\n\nRivolgi le tue domande sul gioco nella\n[chat di Lean su Zulip](https://leanprover.zulipchat.com/), utilizzando\nlo stream \"New Members\". I membri della comunità sono felici di aiutare. Nota che\nla chat di Lean su Zulip è un forum professionale di ricerca.\nPerciò usa il tuo nome reale e per intero, rimani in tema, e sii cortese. Se cerchi\nun forum più informale (dove puoi ad esempio postare\ni meme sui numeri naturali) allora il [server Discord di Lean](https://discord.gg/WZ9bs9UCvx) fa per te.\n\nIn alternativa, se il gioco funziona male o dovessi trovare un bug puoi aprire una issue su github:\n\n* Per problemi relativi al game engine, apri una\n[issue sul repo lean4game](https://github.com/leanprover-community/lean4game/issues).\n* Per problemi relativi ai contenuti del the gioco, apri una\n[issue sul repo NNG](https://github.com/hhu-adam/NNG4/issues).",
  "$x=37\\implies x=37$.": "$x=37\\implies x=37$.",
  "$x+y=x\\implies y=0$.": "$x+y=x\\implies y=0$.",
  "$x+1=y+1 \\implies x=y$.": "$x+1=y+1 \\implies x=y$.",
@@ -873,4 +873,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "# Overview\n\nLa nostra tattica casalinga `simp_add` risolverà qualsiasi goal\ndel tipo `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "# Overview\n\nIl semplificatore di Lean, `simp`, riscriverà ogni\nlemma con il tag `simp` e ogni lemma dato dall'utente, finché può.\nNon solo, cercherà di ordinare le variabili secondo la sua logica interna affinché non entri\nin un loop infinito quando utilizza lemmi come `add_comm`"}
+ "# Overview\n\nIl semplificatore di Lean, `simp`, riscriverà ogni\nlemma con il tag `simp` e ogni lemma dato dall'utente, finché può.\nNon solo, cercherà di ordinare le variabili secondo la sua logica interna affinché non entri\nin un loop infinito quando utilizza lemmi come `add_comm`"}
\ No newline at end of file
diff --git a/.i18n/it/Game.po b/.i18n/it/Game.po
index 9ed3342b..8d4fde40 100644
--- a/.i18n/it/Game.po
+++ b/.i18n/it/Game.po
@@ -548,7 +548,7 @@ msgstr ""
 msgid ""
 "One day this game will have a Prime Number World, with a final boss\n"
 "of proving that $2$ is prime.\n"
-"To do this, we will have to rule out things like $2 = 37 × 42.$\n"
+"To do this, we will have to rule out things like $2 = 37 × 42$.\n"
 "We will do this by proving that any factor of $2$ is at most $2$,\n"
 "which we will do using this lemma. The proof I have in mind manipulates the "
 "hypothesis\n"
@@ -558,7 +558,7 @@ msgid ""
 msgstr ""
 "Un giorno questo gioco avrà il Mondo Numeri Primi, il cui boss finale\n"
 "sarà dimostrare che $2$ è un numero primo.\n"
-"Ma per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42.$\n"
+"Ma per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42$.\n"
 "Lo faremo dimostrando che ogni fattore di $2$ è al più $2$,\n"
 "che avremo gratis grazie a questo lemma. La dimostrazione che ho in mente io "
 "manipola l'ipotesi finché\n"
@@ -815,7 +815,7 @@ msgid ""
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all "
 "occurrences of\n"
-"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+"`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "Ripeti lo stesso comando!\n"
 "\n"
@@ -1122,11 +1122,11 @@ msgstr "`mul_zero m` è la dimostrazione di `m * 0 = 0`."
 
 #: Game.Levels.Multiplication.L08add_mul
 msgid ""
-"Addition is distributive over multiplication.\n"
+"Multiplication is distributive over addition.\n"
 "In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
 "$(a + b) \\times c = ac + bc$."
 msgstr ""
-"L'addizione gode della proprietà distributiva sulla moltiplicazione.\n"
+"La moltiplicazione gode della proprietà distributiva sull'addizione.\n"
 "Equivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n"
 "$(a + b) \\times c = ac + bc$."
 
@@ -4400,7 +4400,7 @@ msgid ""
 "  the goal until it becomes our hypothesis! In other words, we\n"
 "  will \"argue backwards\". The `apply` tactic can do this too.\n"
 "  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+"  \"Typewriter mode\")."
 msgstr ""
 "Nell'ultimo livello abbiamo manipolato l'ipotesi `x + 1 = 4`\n"
 "  per farla coincidere con il goal `x = 3`. In questo livello manipoleremo\n"
@@ -4893,8 +4893,8 @@ msgid ""
 "We have seen how to `apply` theorems and assumptions\n"
 "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
 "To prove this goal, we need to know how to say \"let's assume `P` and deduce "
-"`Q`\"\n"
-"in Lean. We do this with the `intro` tactic."
+"`Q`\".\n"
+"In Lean, we do this with the `intro` tactic."
 msgstr ""
 "Abbiamo visto come fare `apply` di teoremi e ipotesi\n"
 "della forma `P → Q`. Ma come ci comportiamo se è il *goal* ad avere la forma "
@@ -5039,7 +5039,7 @@ msgstr "Sia $x$ un numero, allora $x \\le \\operatorname{succ}(x)$."
 
 #: Game.Levels.Addition.L02succ_add
 msgid ""
-"Well done! You now have enough tools to tackle the main boss of this level."
+"Well done! You now have enough tools to tackle the main boss of this world."
 msgstr ""
 "Ottimo lavoro! Ora sei abbastanza pratico per affrontare il boss principale "
 "di questo mondo."
@@ -5526,12 +5526,12 @@ msgid ""
 "Did you use induction on `y`?\n"
 "Here's a two-line proof of `add_left_eq_self` which uses "
 "`add_right_cancel`.\n"
-"If you want to inspect it, you can go into editor mode by clicking `</>` in "
+"If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in "
 "the top right\n"
 "and then just cut and paste the proof and move your cursor around it\n"
 "to see the hypotheses and goal at any given point\n"
 "(although you'll lose your own proof this way). Click `>_` to get\n"
-"back to command line mode.\n"
+"back to \"Typewriter mode\".\n"
 "```\n"
 "nth_rewrite 2 [← zero_add y]\n"
 "exact add_right_cancel x 0 y\n"
diff --git a/.i18n/uk/Game.json b/.i18n/uk/Game.json
index 6c46fd4f..e0de3010 100644
--- a/.i18n/uk/Game.json
+++ b/.i18n/uk/Game.json
@@ -216,10 +216,10 @@
  "`add_left_cancel a b n` це теорема про те, що $n+a=n+b\\implies a=b$.\nВи можете довести її за допомогою індукції по `n` або ви можете вивести це з `add_right_cancel`.",
  "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$":
  "`add_left_cancel a b n` це теорема про те, що $n+a=n+b \\implies a=b.$",
- "`add_comm a b` is a proof of `a + b = b + a`.":
- "`add_comm a b` є доказом `a + b = b + a`.",
  "`add_comm b c` is a proof that `b + c = c + b`. But if your goal\nis `a + b + c = a + c + b` then `rw [add_comm b c]` will not\nwork! Because the goal means `(a + b) + c = (a + c) + b` so there\nis no `b + c` term *directly* in the goal.\n\nUse associativity and commutativity to prove `add_right_comm`.\nYou don't need induction. `add_assoc` moves brackets around,\nand `add_comm` moves variables around.\n\nRemember that you can do more targeted rewrites by\nadding explicit variables as inputs to theorems. For example `rw [add_comm b]`\nwill only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\nwill only do rewrites of the form `b + c = c + b`.":
  "`add_comm b c` є доказом того, що `b + c = c + b`. Але якщо ваша мета\nце `a + b + c = a + c + b`, тоді `rw [add_comm b c]` неспрацює!\nТому що мета означає `(a + b) + c = (a + c) + b` так що в меті\n*безпосередньо* немає члена `b + c`.\n\nВикористовуйте асоціативність і комутативність, щоб підтвердити `add_right_comm`.\nВам не потрібна індукція. `add_assoc` пересуває дужки,\nа `add_comm` переміщує змінні.\n\nПам’ятайте, що ви можете робити більш цілеспрямовані перезаписи за допомогою\nдодавання явних змінних як вхідних даних до теорем. Наприклад `rw [add_comm b]`\nвиконуватиме лише перезапис у формі `b + ? = ? + b` і `rw [add_comm b c]`\nвиконуватиме лише перезапис у формі `b + c = c + b`.",
+ "`add_comm a b` is a proof of `a + b = b + a`.":
+ "`add_comm a b` є доказом `a + b = b + a`.",
  "`add_assoc a b c` is a proof\nthat `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\nas `a + b + c`, because the notation for addition is defined to be left\nassociative.":
  "`add_assoc a b c` є доказом\nщо `(a + b) + c = a + (b + c)`. Зверніть увагу, що в Lean друкується `(a + b) + c`\nяк `a + b + c`, тому що нотація для додавання визначена ліво-\nасоціативно.",
  "`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\nmeans \"there exists\". So `a ≤ b` means that there exists\na number `c` such that `b = a + c`. This definition works\nbecause there are no negative numbers in this game.\n\nTo *prove* an \"exists\" statement, use the `use` tactic.\nLet's see an example.":
@@ -275,8 +275,8 @@
  "Чому ми просто не визначили `succ n` як `n + 1`? Тому що ми не маємо\nще навіть *визначення* додаванню! Ми зробимо це на наступному рівні.",
  "What do you think of this two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` doesn't just take hypotheses, it will eat any proof which exists\nin the system.":
  "Що ви думаєте про цей дворядковий доказ:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` не просто приймає гіпотези, він з'їдає будь-які наявні докази\nв системі.",
- "Well done! You now have enough tools to tackle the main boss of this level.":
- "Гарна робота! Тепер у вас достатньо інструментів, щоб боротися з головним босом цього рівня.",
+ "Well done! You now have enough tools to tackle the main boss of this world.":
+ "Гарна робота! Тепер у вас достатньо інструментів, щоб боротися з головним босом цього світу.",
  "Well done!": "Гарна робота!",
  "Welcome to tutorial world! In this world we learn the basics\nof proving theorems. The boss level of this world\nis the theorem `2 + 2 = 4`.\n\nYou prove theorems by solving puzzles using tools called *tactics*.\nThe aim is to prove the theorem by applying tactics\nin the right order.\n\nLet's learn some basic tactics. Click on \"Start\" below\nto begin your quest.":
  "Ласкаво просимо до навчального світу! У цьому світі ми вивчаємо основи\nдоведення теорем. Рівневим босом цього світу\nє теорема `2 + 2 = 4`.\n\nВи доводите теореми, вирішуючи головоломки за допомогою інструментів під назвою *тактики*.\nМета полягає в тому, щоб довести теорему шляхом застосування тактики\nу правильному порядку.\n\nДавайте навчимося деяким основним тактикам. Натисніть «Почати» нижче\nщоб почати свою пригоду.",
@@ -312,7 +312,7 @@
  "Тепер у нас достатньо всього, щоб довести, що множення асоціативне,\nбосовий рівень світу множення. Удачі!",
  "We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\nif we have a hypothesis `succ n = 0`? It's the wrong way around!\n\nThe `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\nto `y ≠ x`. And `symm at h`\ndoes the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\nthe proof `zero_ne_one`; now try proving $1 \\neq 0$.":
  "Ми знаємо, що `zero_ne_succ n` є доказом `0 = succ n → False` -- але що\nякщо ми маємо гіпотезу `succ n = 0`? Це неправильний шлях!\n\nТактика `symm` змінює ціль `x = y` на `y = x`, а ціль `x ≠ y`\nна `y ≠ x`. І `symm у h`\nробить те саме для гіпотези `h`. Ми довели $0 \\neq 1$ і назвали\nдоказ `zero_ne_one`; тепер спробуйте довести $1 \\neq 0$.",
- "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\nin Lean. We do this with the `intro` tactic.":
+ "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".\nIn Lean, we do this with the `intro` tactic.":
  "Ми побачили, як `apply`-іти теореми та припущення\nвиду `P → Q`. Але що, якщо наша *мета* має форму `P → Q`?\nЩоб підтвердити цю мету, нам потрібно знати, як сказати \"давайте припустимо `P` і виведемо `Q`\"\nв Lean. Ми робимо це за допомогою тактики `intro`.",
  "We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.":
  "Раніше ми надали досить незадовільний доказ `2 + 2 ≠ 5`; тепер давайте зробимо кращій.",
@@ -446,8 +446,8 @@
  "Нашою першою місією є `mul_comm x y : x * y = y * x`,\nі ми хочемо довести це індукцією. Нульовий\nвипадок буде потребувати `mul_zero` (який у нас є)\nі `zero_mul` (якого ми не маємо), тож давайте\nпонемо з нього.",
  "One of the best named levels in the game, a savage `pow_pow`\nsub-boss appears as the music reaches a frenzy. What\nelse could there be to prove about powers after this?":
  "Один із найкращих іменованих рівнів у грі, дикий `pow_pow`\nпідбос з'являється у той час коли музика досягає піку. Що\nще можна було б довести про ступені після цього?",
- "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42.$\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
- "Одного разу в цій грі з’явиться світ простих чисел із останнім босом\nдоведення того, що $2$ є простим числом.\nДля цього нам доведеться виключити такі речі, як $2 = 37 × 42.$\nМи зробимо це, довівши, що будь-який множник $2$ не перевищує $2$,\nщо ми зробимо, використовуючи цю лему. Доказ, який я маю на увазі, маніпулює гіпотезою\nпоки це не стане метою, використовуючи `mul_left_ne_zero`, `one_le_of_ne_zero` та\n`mul_le_mul_right`.",
+ "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42$.\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
+ "Одного разу в цій грі з’явиться світ простих чисел із останнім босом\nдоведення того, що $2$ є простим числом.\nДля цього нам доведеться виключити такі речі, як $2 = 37 × 42$.\nМи зробимо це, довівши, що будь-який множник $2$ не перевищує $2$,\nщо ми зробимо, використовуючи цю лему. Доказ, який я маю на увазі, маніпулює гіпотезою\nпоки це не стане метою, використовуючи `mul_left_ne_zero`, `one_le_of_ne_zero` та\n`mul_le_mul_right`.",
  "On the set of natural numbers, addition is commutative.\nIn other words, if `a` and `b` are arbitrary natural numbers, then\n$a + b = b + a$.":
  "На множині натуральних чисел додавання комутативне.\nІншими словами, якщо `a` і `b` це довільні натуральні числа, то\n$a + b = b + a$.",
  "On the set of natural numbers, addition is associative.\nIn other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n$ (a + b) + c = a + (b + c). $":
@@ -526,6 +526,8 @@
  "Мій доказ:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```",
  "Multiplication usually makes a number bigger, but multiplication by zero can make\nit smaller. Thus many lemmas about inequalities and multiplication need the\nhypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.\nTo help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\non the right to see what it does.":
  "Множення зазвичай збільшує число, але множення на нуль може зробити\nйого меншим. Тому багато лем про нерівності та множення потребують\nгіпотези `a ≠ 0`. Ось ключова лема, яка дозволяє нам використовувати цю гіпотезу.\nЩоб допомогти нам із доказом, ми можемо використати тактику `tauto`. Натисніть на назву тактики\nправоруч, щоб побачити, що вона робить.",
+ "Multiplication is distributive over addition.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
+ "Множення діє дістрібутивно над додаванням.\nІншими словами, для всіх натуральних чисел $a$, $b$ і $c$ маємо\n$(a + b) \\times c = ac + bc$.",
  "Multiplication is distributive over addition on the left.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$a(b + c) = ab + ac$.":
  "Множення дістрібутивно над додаванням зліва.\nІншими словами, для всіх натуральних чисел $a$, $b$ і $c$ маємо\n$a(b + c) = ab + ac$.",
  "Multiplication is commutative.": "Множення комутативне.",
@@ -586,7 +588,7 @@
  "У цій грі ви відтворюєте натуральні числа $\\mathbb{N}$ із аксіом Пеано,\nвивчаючи основи доведення теорем в Lean.\n\nЦе хороший перший крок у Lean!",
  "In the next level, we'll do the same proof but backwards.":
  "На наступному рівні ми виконаємо той самий доказ, але в зворотному напрямку.",
- "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  command line mode).":
+ "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  \"Typewriter mode\").":
  "На останньому рівні ми маніпулювали гіпотезою `x + 1 = 4`\n  поки вона не стало метою `x = 3`. На цьому рівні ми будемо маніпулювати\n  мету, поки вона не стане нашою гіпотезою! Іншими словами, ми\n  буде «аргументувати у зворотньому напрямку». Тактика `apply` також може це зробити.\n  Я знову проведу вас через цей шлях (якщо ви в\n  режимі командного рядка).",
  "In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\nfrom a false statement. The `tauto` tactic will close this goal.":
  "У «базовому випадку» ми маємо гіпотезу `ha : 0 ≠ 0`, і ви можете вивести будь-що\nіз хибного твердження. Тактика `tauto` закриє цю мету.",
@@ -736,9 +738,9 @@
  "Fermat's Last Theorem": "Остання теорема Ферма",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Кожне число в Lean є або $0$, або наступним значенням (наступником). Ми знаємо, як додати $0$,\nале нам потрібно зрозуміти, як додати наступників. Скажімо, ми вже знаємо\nщо `37 + d = q`. Якою має бути відповідь на `37 + succ d`? Гаразд,\n`succ d` на одиницю більший за `d`, тому `37 + succ d` має бути `succ q`,\nчисло на один більше за `q`. Більш загально `x + succ d` повинен\nбути `succ (x + d)`. Додамо це як лему.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nЯкщо ви побачите `... + succ ...` у своїй меті, `rw [add_succ]`\nзазвичай хороша ідея.\n\nДавайте тепер доведемо, що `succ n = n + 1`. З’ясуйте, як додати `+ succ`\nу фокус, а потім зробіть `rw [add_succ]`. Перемикайте між вкладками `+` (додавання) і\n`012` (цифри) у розділі \"Теореми\" праворуч\nі подивіться, які докази ви можете переписати.",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet.":
  "Зробіть це ще раз!\n\n`rw [zero_add] в «{h}»` намагається заповнити\nаргументи `zero_add` (знаходження `«{x}»`), потім вона замінює всі знайдені входження\n`0 + «{x}»`. Таким чином тактика не переписує `0 + «{y}»`.",
- "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
+ "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to \"Typewriter mode\".\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "Ви використовували індукцію на `y`?\nОсь дворядковий доказ `add_left_eq_self`, який використовує `add_right_cancel`.\nЯкщо ви хочете перевірити його, ви можете перейти в режим редактора, натиснувши `</>` у верхньому правому куті\nа потім просто виріжте та вставте доказ і перемістіть курсор навколо нього\nщоб побачити гіпотези та мету в будь-якій точці\n(хоча таким чином ви втратите свій власний доказ). Натисніть `>_`, щоб\nповернутися назад до режиму командного рядка.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
  "Dealing with `or`": "Робота з `or`",
  "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World (when someone gets around to\nimplementing it).":
@@ -779,8 +781,6 @@
  "Advanced Addition World": "Світ розширеного додавання",
  "Advanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts about multiplication, such as `x * y = 1 → x = 1`, and\n`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.":
  "Світ розширенного *додаванн* довів різні імплікації\nвключаючі додавання, наприклад `x + y = 0 → x = 0` і `x + y = x → y = 0`.\nЦі леми були використані для доведення основних фактів про ≤ у Світі ≤.\n\nУ Світі розширенного множення ми доводимо аналогічни\nфакти про множення, наприклад `x * y = 1 → x = 1`, і\n`x * y = x → y = 1` (припускаючи, що `x ≠ 0` в останньому результаті). Це підготує\nнас для світу ділення.\n\nСвіт множення складніший за світ додавання. У тому самому\nсенсі, світ розширеного множення є складнішим, ніж світ розширеного додавання.\nОднією з причин цього є те, що є лише певні проміжні результати\nє вірними лише за умови додаткової гіпотези, що одна зі змінних не дорівнює нулю.\nЦе викликає деякі несподівані додаткові повороти.",
- "Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
- "Додавання діє дістрібутивно над множенням.\nІншими словами, для всіх натуральних чисел $a$, $b$ і $c$ маємо\n$(a + b) \\times c = ac + bc$.",
  "Addition World": "Світ додавання",
  "Adding zero": "Додавання нуля",
  "A two-line proof is\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nWe now have all the tools necessary to set up the basic theory of divisibility of naturals.":
@@ -799,8 +799,8 @@
  "2 + 2 ≠ 5": "2 + 2 ≠ 5",
  "1 ≠ 0": "1 ≠ 0",
  "0 ≤ x": "0 ≤ x",
- "*Game version: 4.3*\n\n*Recent additions: bug fixes*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
- "*Версія гри: 4.3*\n\n*Останні доповнення: виправлення помилок*\n\n## Збереження прогресу\n\nГра зберігає ваш прогрес у локальному сховищі браузера.\nЯкщо ви видалите його, ваш прогрес буде втрачено!\n\nПопередження: у більшості браузерів видалення файлів cookie також очищає локальне сховище\n(або «дані локального сайту»). Обов’язково спершу скачайте свій прогрес гри!\n\n## Подяки\n\n* **Творці:** Кевін Баззард, Джон Югстер\n* **Оригінальна версія Lean3:** Кевін Баззард, Мохаммад Педрамфар\n* **Ігровий рушій:** Олександр Бенткамп, Джон Югстер, Патрік Массо\n* **Додаткові рівні:** Сіан Кері, Іван Фарабелла, Арчі Браун.\n* **Додаткова подяка:** Усім учням-бета-тестерам, усім школам\nякі запросли Кевіна виступити, і всіх школярів, які ставили йому запитання\nпро матеріал.\n\n## Ресурси\n\n* Форум [Lean Zulip chat](https://leanprover.zulipchat.com/).\n* [Оригінальна версія Lean3](https://github.com/ImperialCollegeLondon/natural_number_game/) (більше не підтримується)\n\n## Проблеми?\n\nБудь ласка, задавайте будь-які запитання щодо цієї гри на\nфорумі [Zulip чату Lean](https://leanprover.zulipchat.com/), наприклад у\nпотік «New Members». Громада з радістю допоможе. Зауважте, що\nчат Lean Zulip — це професійний дослідницький форум.\nБудь ласка, використовуйте тут своє повне справжнє ім’я, не відривайтесь від теми та будьте чемними. Якщо ви\nшукаєте десь менш формальне (наприклад, ви хочете опублікувати меми гри в натуральні числа),\nто перейдіть до [Lean діскорду](https://discord.gg/WZ9bs9UCvx).\n\nКрім того, якщо у вас виникли проблеми / помилки, ви також можете відкрити проблеми на github:\n\n* Якщо у вас виникли проблеми з ігровим двигуном, відкрийте\n[проблема в репозиторії lean4game](https://github.com/leanprover-community/lean4game/issues).\n* Якщо у вас виникли питання щодо вмісту гри, відкрийте\n[проблема в NNG](https://github.com/hhu-adam/NNG4/issues) репі.",
+ "*Game version: 4.3*\n\n*Recent additions: bug fixes*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
+ "*Версія гри: 4.3*\n\n*Останні доповнення: виправлення помилок*\n\n## Збереження прогресу\n\nГра зберігає ваш прогрес у локальному сховищі браузера.\nЯкщо ви видалите його, ваш прогрес буде втрачено!\n\nПопередження: у більшості браузерів видалення файлів cookie також очищає локальне сховище\n(або «дані локального сайту»). Обов’язково спершу скачайте свій прогрес гри!\n\n## Подяки\n\n* **Творці:** Кевін Баззард, Джон Югстер\n* **Оригінальна версія Lean3:** Кевін Баззард, Мохаммад Педрамфар\n* **Ігровий рушій:** Олександр Бенткамп, Джон Югстер, Патрік Массо\n* **Додаткові рівні:** Сіан Кері, Іван Фарабелла, Арчі Браун.\n* **Додаткова подяка:** Усім учням-бета-тестерам, усім школам\nякі запросли Кевіна виступити, і всіх школярів, які ставили йому запитання\nпро матеріал.\n\n## Ресурси\n\n* Форум [Lean Zulip chat](https://leanprover.zulipchat.com/).\n* [Оригінальна версія Lean3](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (більше не підтримується)\n\n## Проблеми?\n\nБудь ласка, задавайте будь-які запитання щодо цієї гри на\nфорумі [Zulip чату Lean](https://leanprover.zulipchat.com/), наприклад у\nпотік «New Members». Громада з радістю допоможе. Зауважте, що\nчат Lean Zulip — це професійний дослідницький форум.\nБудь ласка, використовуйте тут своє повне справжнє ім’я, не відривайтесь від теми та будьте чемними. Якщо ви\nшукаєте десь менш формальне (наприклад, ви хочете опублікувати меми гри в натуральні числа),\nто перейдіть до [Lean діскорду](https://discord.gg/WZ9bs9UCvx).\n\nКрім того, якщо у вас виникли проблеми / помилки, ви також можете відкрити проблеми на github:\n\n* Якщо у вас виникли проблеми з ігровим двигуном, відкрийте\n[проблема в репозиторії lean4game](https://github.com/leanprover-community/lean4game/issues).\n* Якщо у вас виникли питання щодо вмісту гри, відкрийте\n[проблема в NNG](https://github.com/hhu-adam/NNG4/issues) репі.",
  "$x=37\\implies x=37$.": "$x=37\\implies x=37$.",
  "$x+y=x\\implies y=0$.": "$x+y=x\\implies y=0$.",
  "$x+1=y+1 \\implies x=y$.": "$x+1=y+1 \\implies x=y$.",
@@ -869,4 +869,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "# Огляд\n\nНаша саморобна тактика `simp_add` вирішить довільні цілі\nу формі `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "# Огляд\n\nСпрощувач Lean, `simp`, перепише кожну лему\nз тегом `simp` і кожну лему, надану користувачем, настількі, наскільки це можливо.\nКрім того, він намагатиметься впорядкувати змінні у внутрішньому порядку, якщо йому буде скормлено\nлеми, такі як `add_comm`, щоб він не перейшов в нескінченний цикл."}
+ "# Огляд\n\nСпрощувач Lean, `simp`, перепише кожну лему\nз тегом `simp` і кожну лему, надану користувачем, настількі, наскільки це можливо.\nКрім того, він намагатиметься впорядкувати змінні у внутрішньому порядку, якщо йому буде скормлено\nлеми, такі як `add_comm`, щоб він не перейшов в нескінченний цикл."}
\ No newline at end of file
diff --git a/.i18n/uk/Game.po b/.i18n/uk/Game.po
index d396bfe5..172c4055 100644
--- a/.i18n/uk/Game.po
+++ b/.i18n/uk/Game.po
@@ -1345,10 +1345,10 @@ msgstr ""
 
 #: Game.Levels.Addition.L02succ_add
 msgid ""
-"Well done! You now have enough tools to tackle the main boss of this level."
+"Well done! You now have enough tools to tackle the main boss of this world."
 msgstr ""
 "Гарна робота! Тепер у вас достатньо інструментів, щоб боротися з головним "
-"босом цього рівня."
+"босом цього світу."
 
 #: Game.Levels.Addition.L03add_comm
 msgid "add_comm (level boss)"
@@ -1921,11 +1921,11 @@ msgstr "`add_mul a b c` є доказом того, що $(a+b)c=ac+bc$."
 
 #: Game.Levels.Multiplication.L08add_mul
 msgid ""
-"Addition is distributive over multiplication.\n"
+"Multiplication is distributive over addition.\n"
 "In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
 "$(a + b) \\times c = ac + bc$."
 msgstr ""
-"Додавання діє дістрібутивно над множенням.\n"
+"Множення діє дістрібутивно над додаванням.\n"
 "Іншими словами, для всіх натуральних чисел $a$, $b$ і $c$ маємо\n"
 "$(a + b) \\times c = ac + bc$."
 
@@ -2569,7 +2569,7 @@ msgid ""
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences "
 "of\n"
-"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+"`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "Зробіть це ще раз!\n"
 "\n"
@@ -2841,7 +2841,7 @@ msgid ""
 "  the goal until it becomes our hypothesis! In other words, we\n"
 "  will \"argue backwards\". The `apply` tactic can do this too.\n"
 "  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+"  \"Typewriter mode\")."
 msgstr ""
 "На останньому рівні ми маніпулювали гіпотезою `x + 1 = 4`\n"
 "  поки вона не стало метою `x = 3`. На цьому рівні ми будемо маніпулювати\n"
@@ -2933,8 +2933,8 @@ msgid ""
 "We have seen how to `apply` theorems and assumptions\n"
 "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
 "To prove this goal, we need to know how to say \"let's assume `P` and deduce "
-"`Q`\"\n"
-"in Lean. We do this with the `intro` tactic."
+"`Q`\".\n"
+"In Lean, we do this with the `intro` tactic."
 msgstr ""
 "Ми побачили, як `apply`-іти теореми та припущення\n"
 "виду `P → Q`. Але що, якщо наша *мета* має форму `P → Q`?\n"
@@ -4064,12 +4064,12 @@ msgstr "$x + y = y\\implies x=0.$"
 msgid ""
 "Did you use induction on `y`?\n"
 "Here's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\n"
-"If you want to inspect it, you can go into editor mode by clicking `</>` in "
+"If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in "
 "the top right\n"
 "and then just cut and paste the proof and move your cursor around it\n"
 "to see the hypotheses and goal at any given point\n"
 "(although you'll lose your own proof this way). Click `>_` to get\n"
-"back to command line mode.\n"
+"back to \"Typewriter mode\".\n"
 "```\n"
 "nth_rewrite 2 [← zero_add y]\n"
 "exact add_right_cancel x 0 y\n"
@@ -5360,7 +5360,7 @@ msgstr ""
 msgid ""
 "One day this game will have a Prime Number World, with a final boss\n"
 "of proving that $2$ is prime.\n"
-"To do this, we will have to rule out things like $2 = 37 × 42.$\n"
+"To do this, we will have to rule out things like $2 = 37 × 42$.\n"
 "We will do this by proving that any factor of $2$ is at most $2$,\n"
 "which we will do using this lemma. The proof I have in mind manipulates the "
 "hypothesis\n"
@@ -5369,7 +5369,7 @@ msgid ""
 msgstr ""
 "Одного разу в цій грі з’явиться світ простих чисел із останнім босом\n"
 "доведення того, що $2$ є простим числом.\n"
-"Для цього нам доведеться виключити такі речі, як $2 = 37 × 42.$\n"
+"Для цього нам доведеться виключити такі речі, як $2 = 37 × 42$.\n"
 "Ми зробимо це, довівши, що будь-який множник $2$ не перевищує $2$,\n"
 "що ми зробимо, використовуючи цю лему. Доказ, який я маю на увазі, маніпулює "
 "гіпотезою\n"
diff --git a/.i18n/zh/Game.json b/.i18n/zh/Game.json
index dba45d72..28fd4ef7 100644
--- a/.i18n/zh/Game.json
+++ b/.i18n/zh/Game.json
@@ -207,10 +207,10 @@
  "`add_left_cancel a b n` 是定理 $n+a=n+b\\implies a=b$。你可以通过对 `n` 进行归纳来证明它，或者你可以从 `add_right_cancel` 推导出它。",
  "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$":
  "`add_left_cancel a b n` 是 $n+a=n+b \\implies a=b$ 的定理名字。",
- "`add_comm a b` is a proof of `a + b = b + a`.":
- "`add_comm a b` 是 `a + b = b + a` 的证明。",
  "`add_comm b c` is a proof that `b + c = c + b`. But if your goal\nis `a + b + c = a + c + b` then `rw [add_comm b c]` will not\nwork! Because the goal means `(a + b) + c = (a + c) + b` so there\nis no `b + c` term *directly* in the goal.\n\nUse associativity and commutativity to prove `add_right_comm`.\nYou don't need induction. `add_assoc` moves brackets around,\nand `add_comm` moves variables around.\n\nRemember that you can do more targeted rewrites by\nadding explicit variables as inputs to theorems. For example `rw [add_comm b]`\nwill only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\nwill only do rewrites of the form `b + c = c + b`.":
  "`add_comm b c` 是一个 `b + c = c + b` 的证明。但如果您的目标是 `a + b + c = a + c + b`，那么 `rw [add_comm b c]` 将不起作用！因为目标是 `(a + b) + c = (a + c) + b`，所以目标中*直接*没有 `b + c` 项。\n\n使用结合律和交换律来证明 `add_right_comm`。您不需要使用归纳法。`add_assoc` 移动括号，`add_comm` 移动变量。\n\n请记住，您可以通过将显式变量添加为定理的输入来进行更有针对性的重写。\n例如，`rw [add_comm b]` 只会重写形如 `b + ? = ? + b` 的形式，而 `rw [add_comm b c]` 只会重写形如 `b + c = c + b` 的形式。",
+ "`add_comm a b` is a proof of `a + b = b + a`.":
+ "`add_comm a b` 是 `a + b = b + a` 的证明。",
  "`add_assoc a b c` is a proof\nthat `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\nas `a + b + c`, because the notation for addition is defined to be left\nassociative.":
  "`add_assoc a b c` 是一个 `(a + b) + c = a + (b + c)` 的证明。\n请注意，在 Lean `(a + b) + c` 中显示\n为 `a + b + c`，因为加法符号被定义为左\n结合的。",
  "`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\nmeans \"there exists\". So `a ≤ b` means that there exists\na number `c` such that `b = a + c`. This definition works\nbecause there are no negative numbers in this game.\n\nTo *prove* an \"exists\" statement, use the `use` tactic.\nLet's see an example.":
@@ -264,8 +264,8 @@
  "为什么我们不直接将 `succ n` 定义为 `n + 1`？因为我们还没有\n *定义* 加法！我们将在下一关做到这一点。",
  "What do you think of this two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` doesn't just take hypotheses, it will eat any proof which exists\nin the system.":
  "你对这两行代码有什么看法？\n\n```\nsymm\nexact zero_ne_one\n```\n\n请注意，`exact` 不仅限于使用假设，它可以接受系统中存在的任何证明。",
- "Well done! You now have enough tools to tackle the main boss of this level.":
- "做得好！现在你有足够的工具来对付这个关卡的大Boss了。",
+ "Well done! You now have enough tools to tackle the main boss of this world.":
+ "做得好！现在你有足够的工具来对付这个世界的大Boss了。",
  "Well done!": "做得好！",
  "Welcome to tutorial world! In this world we learn the basics\nof proving theorems. The boss level of this world\nis the theorem `2 + 2 = 4`.\n\nYou prove theorems by solving puzzles using tools called *tactics*.\nThe aim is to prove the theorem by applying tactics\nin the right order.\n\nLet's learn some basic tactics. Click on \"Start\" below\nto begin your quest.":
  "欢迎进入教程世界！在这里，我们将掌握证明定理的初步技能。这个世界中的终极挑战是证明 `2 + 2 = 4` 这一定理。\n\n解决这些谜题并证明定理的过程中，你将使用一种名为*策略*的强大工具。证明定理的关键在于准确地应用这些策略。\n\n现在，让我们开始学习一些基本策略吧。请点击下面的“开始”按钮，开启你的证明之旅。",
@@ -301,7 +301,7 @@
  "我们现在有足够的工具去证明乘法服从结合律，\n乘法世界的boss关。祝你好运！",
  "We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\nif we have a hypothesis `succ n = 0`? It's the wrong way around!\n\nThe `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\nto `y ≠ x`. And `symm at h`\ndoes the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\nthe proof `zero_ne_one`; now try proving $1 \\neq 0$.":
  "我们知道 `zero_ne_succ n` 是证明 `0 = succ n → False` 的证明。但是如果我们有一个假设 `succ n = 0` 呢？这恰好是反过来的！\n\n`symm` 策略可以将目标 `x = y` 改为 `y = x`，并将目标 `x ≠ y` 改为 `y ≠ x`。而 `symm at h` 对假设 `h` 也做同样的操作。\n我们已经证明了 $0 \\neq 1$，并将证明命名为 `zero_ne_one`；现在请尝试证明 $1 \\neq 0$。",
- "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\nin Lean. We do this with the `intro` tactic.":
+ "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".\nIn Lean, we do this with the `intro` tactic.":
  "我们已经看到了如何 `apply` 形式为 `P → Q` 的定理和假设。\n但如果我们的 *目标* 是形式为 `P → Q` 的呢？\n要证明这个目标，我们需要知道如何在 Lean 中表示 “假设 `P` 并推导出 `Q`”。我们用 `intro` 策略来做这件事。",
  "We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.":
  "我们前面给出的 `2 + 2 ≠ 5` 证明并不令人满意，现在给出一个更好的证明。",
@@ -428,7 +428,7 @@
  "我们的第一个挑战是`mul_comm x y : x * y = y * x`，\n我们想通过归纳法来证明这一点。在证明0的目标下我们需要 `mul_zero` （我们有）和 `zero_mul` （我们没有），所以让我们从这里开始。",
  "One of the best named levels in the game, a savage `pow_pow`\nsub-boss appears as the music reaches a frenzy. What\nelse could there be to prove about powers after this?":
  "游戏中最名副其实的关卡之一。\n随着音乐达到狂热，一个凶猛的 `pow_pow` 小boss出现了。\n在这之后，还有什么关于幂的性质需要证明呢？",
- "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42.$\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
+ "One day this game will have a Prime Number World, with a final boss\nof proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 = 37 × 42$.\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n`mul_le_mul_right`.":
  "在质数世界中，我们将证明 $2$ 是质数。为此，我们必须排除像 $2 ≠ 37 × 42$ 这样的情况。\n我们将通过证明 $2$ 的任何因数最多是 $2$ 来做到这一点，我们将使用这个引理来实现。\n我脑海中的证明会操作假设，直到它变成目标，几乎使用我们到目前为止在这个世界中已经证明的所有内容。",
  "On the set of natural numbers, addition is commutative.\nIn other words, if `a` and `b` are arbitrary natural numbers, then\n$a + b = b + a$.":
  "在自然数集上，加法是可交换的。\n换句话说，如果 `a` 和 `b` 是任意自然数，那么\n$a + b = b + a$。",
@@ -505,6 +505,8 @@
  "我的证明：\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```",
  "Multiplication usually makes a number bigger, but multiplication by zero can make\nit smaller. Thus many lemmas about inequalities and multiplication need the\nhypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.\nTo help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\non the right to see what it does.":
  "乘法通常会使一个数字变大，但是乘以零可以使它变小。因此，关于不等式和乘法的许多引理需要假设 `a ≠ 0`。\n这里有一个关键的引理使我们能够使用这个假设。我们可以使用 `tauto` 策略帮助我们进行证明。点击右侧的策略名称查看它的作用。",
+ "Multiplication is distributive over addition.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
+ "乘法对加法有分配律。换句话说，对于所有自然数 $a$、$b$ 和 $c$，\n我们有 $(a + b) \\times c = ac + bc$。",
  "Multiplication is distributive over addition on the left.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$a(b + c) = ab + ac$.":
  "乘法对左边的加法具有分配性。\n换句话说，对于所有自然数 $a$、$b$ 和 $c$，我们有\n$a(b + c) = ab + ac$。",
  "Multiplication is commutative.": "乘法是可交换的。",
@@ -562,7 +564,7 @@
  "在这个游戏中，你将根据皮亚诺公理重新构建自然数集 $\\mathbb{N}$，学习在 Lean 中证明定理的基础知识。\n\n这是对 Lean 的一个很好的初步介绍！",
  "In the next level, we'll do the same proof but backwards.":
  "在下一级别中，我们将进行相同的证明，但要从后往前证。",
- "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  command line mode).":
+ "In the last level, we manipulated the hypothesis `x + 1 = 4`\n  until it became the goal `x = 3`. In this level we'll manipulate\n  the goal until it becomes our hypothesis! In other words, we\n  will \"argue backwards\". The `apply` tactic can do this too.\n  Again I will walk you through this one (assuming you're in\n  \"Typewriter mode\").":
  "在最后一关，我们操纵了假设 `x + 1 = 4`\n  直到成为目标 `x = 3` 。在这一关我们将改写\n  目标，直到它成为我们的假设！换句话说，我们\n  会“从后向前”证明。 `apply` 策略也可以做到这一点。\n  我将再次引导您完成这一过程（假设您在\n  命令行模式）。",
  "In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\nfrom a false statement. The `tauto` tactic will close this goal.":
  "在“基础情形”中，我们有一个假设 `ha : 0 ≠ 0`，你可以从一个假命题中推导出任何东西。`tauto` 策略将证明这个目标。",
@@ -710,9 +712,9 @@
  "Fermat's Last Theorem": "费马大定理",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Lean 中的每个数字要么是 $0$ 要么是后继数。我们已经知道如何加 $0$，\n我们还需要弄清楚如何添加后继数。假设我们已经知道\n`37 + d = q`。 `37 + succ d` 的答案应该是什么？\n`succ d` 比 `d` 大1，因此 `37 + succ d` 应该是 `succ q`，\n也就是比 `q` 大1。更一般地说，`x + succ d` 应该\n为 `succ (x + d)`。让我们将其添加为定理。\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\n如果您在证明目标中看到 `... + succ ...`，那么用 `rw [add_succ]` 改写\n通常是个好主意。\n\n现在让我们证明 `succ n = n + 1`。弄清楚如何引入 `+ succ` \n，然后再 `rw [add_succ]`。在右侧“定理”下的 `+`（加法）和\n `012`（数字）选项卡里\n看看你可以用哪些证明重写目标。\n\n在 Lean 中，每个数字要么是 $0$，要么是某个数字的后继数。我们已经掌握了如何加上 $0$，下一步需要明白如何加上后继数。设想我们已经知道 `37 + d = q`。那么 `37 + succ d` 应该是什么呢？由于 `succ d` 比 `d` 多 $1$，所以 `37 + succ d` 应该等于 `succ q`，也就是 `q` 加 $1$。更一般地，`x + succ d` 应等于 `succ (x + d)`。我们把这个规则加为一个引理：\n\n- `add_succ x d : x + succ d = succ (x + d)`\n\n当你在证明目标中遇到 `... + succ ...` 形式时，使用 `rw [add_succ]` 来重写通常是一个好策略。\n\n现在，让我们来证明 `succ n = n + 1`。思考如何先引入 `+ succ` 形式，然后再应用 `rw [add_succ]` 策略。请在右侧“定理”部分的 `+`（代表加法）和 `012`（代表数字）标签页中查找可以用来重写目标的定理。",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet.":
  "再做一次！\n\n`rw [zero_add] at «{h}»` 试图填充 `zero_add` 的参数（找到 `«{x}»`），然后替换它找到的所有 `0 + «{x}»` 出现的地方。因此，`0 + «{y}»`还没有被重写 。",
- "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
+ "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to \"Typewriter mode\".\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "你是否对 `y` 使用了归纳法？\n这里有一个使用 `add_right_cancel` 证明 `add_left_eq_self`的两行证明。如果你想查看它，你可以通过点击右上角的 `</>` 进入编辑器模式，然后只需剪切和粘贴证明，并在其周围移动你的光标，以查看在任何给定点的假设和目标（尽管这样做你会失去自己的证明）。点击 `>_` 返回命令行模式。\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
  "Dealing with `or`": "处理 `or`",
  "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World (when someone gets around to\nimplementing it).":
@@ -751,8 +753,6 @@
  "Advanced Addition World": "高级加法世界",
  "Advanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts about multiplication, such as `x * y = 1 → x = 1`, and\n`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.":
  "高级 *加法* 世界证明了涉及加法的各种引理，例如 `x + y = 0 → x = 0` 和 `x + y = x → y = 0`。这些引理被用来证明 ≤ 世界中关于 ≤ 的基本事实。\n\n在高级乘法世界中，我们证明了关于乘法的类似事实，例如 `x * y = 1 → x = 1`，以及 `x * y = x → y = 1`（在后一个结果中假设 `x ≠ 0`）。这将为我们进入可除性世界做准备。\n\n乘法世界比加法世界更为复杂。同样，高级乘法世界比高级加法世界更为复杂。其中一个原因是某些中间结果只在额外假设下为真，即变量之一非零。这导致了一些意想不到的转折。",
- "Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.":
- "加法和乘法有分配律。换句话说，对于所有自然数 $a$、$b$ 和 $c$，\n我们有 $(a + b) \\times c = ac + bc$。",
  "Addition World": "加法世界",
  "Adding zero": "加零",
  "A two-line proof is\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nWe now have all the tools necessary to set up the basic theory of divisibility of naturals.":
@@ -771,8 +771,8 @@
  "2 + 2 ≠ 5": "2 + 2 ≠ 5",
  "1 ≠ 0": "1 ≠ 0",
  "0 ≤ x": "0 ≤ x",
- "*Game version: 4.3*\n\n*Recent additions: bug fixes*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://github.com/ImperialCollegeLondon/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
- "*游戏版本：4.2*\n\n*最近新增：不等式世界，算法世界*\n\n## 进度保存\n\n游戏会将你的进度存储在本地浏览器存储中。\n如果你删除它，你的进度将会丢失！\n\n警告：在大多数浏览器中，删除 cookie 也会清除本地存储（或“本地网站数据”）。确保首先下载你的游戏进度！\n\n## 致谢\n\n* **创建者：** Kevin Buzzard, Jon Eugster\n* **原始 Lean3 版本：** Kevin Buzzard, Mohammad Pedramfar\n* **游戏引擎：** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **额外关卡：** Sian Carey, Ivan Farabella, Archie Browne.\n* **特别感谢：** 所有学生测试者，所有邀请 Kevin 发表演讲的学校，以及向他提出关于材料问题的所有学生。\n\n## 资源\n\n* [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛\n* [原始 Lean3 版本](https://github.com/ImperialCollegeLondon/natural_number_game/)（不再维护）\n\n## 有问题吗？\n\n请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新成员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使用您的全名，保持话题相关，且友好。如果你正在寻找一个不那么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean Discord](https://discord.gg/WZ9bs9UCvx)。\n\n另外，如果你遇到问题/漏洞，你也可以在 github 上提出问题：\n\n* 对于游戏引擎的问题，请在 [lean4game](https://github.com/leanprover-community/lean4game/issues) 仓库提出问题。\n* 对于游戏内容的问题，请在 [NNG](https://github.com/hhu-adam/NNG4/issues) 仓库提出问题。",
+ "*Game version: 4.3*\n\n*Recent additions: bug fixes*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.":
+ "*游戏版本：4.2*\n\n*最近新增：不等式世界，算法世界*\n\n## 进度保存\n\n游戏会将你的进度存储在本地浏览器存储中。\n如果你删除它，你的进度将会丢失！\n\n警告：在大多数浏览器中，删除 cookie 也会清除本地存储（或“本地网站数据”）。确保首先下载你的游戏进度！\n\n## 致谢\n\n* **创建者：** Kevin Buzzard, Jon Eugster\n* **原始 Lean3 版本：** Kevin Buzzard, Mohammad Pedramfar\n* **游戏引擎：** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **额外关卡：** Sian Carey, Ivan Farabella, Archie Browne.\n* **特别感谢：** 所有学生测试者，所有邀请 Kevin 发表演讲的学校，以及向他提出关于材料问题的所有学生。\n\n## 资源\n\n* [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛\n* [原始 Lean3 版本](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)（不再维护）\n\n## 有问题吗？\n\n请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新成员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使用您的全名，保持话题相关，且友好。如果你正在寻找一个不那么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean Discord](https://discord.gg/WZ9bs9UCvx)。\n\n另外，如果你遇到问题/漏洞，你也可以在 github 上提出问题：\n\n* 对于游戏引擎的问题，请在 [lean4game](https://github.com/leanprover-community/lean4game/issues) 仓库提出问题。\n* 对于游戏内容的问题，请在 [NNG](https://github.com/hhu-adam/NNG4/issues) 仓库提出问题。",
  "$x=37\\implies x=37$.": "$x=37\\implies x=37$ 。",
  "$x+y=x\\implies y=0$.": "$x+y=x\\implies y=0$.",
  "$x+1=y+1 \\implies x=y$.": "$x+1=y+1\\implies x=y$。",
@@ -840,4 +840,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "## 概述\n\n我们自制的策略 `simp_add` 将解决以下形式的任意目标：\n `a + (b + c) + (d + e) = e + (d + (c + b)) + a`。",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "## 概述\n\nLean 的简化器 `simp` 将它将用每个用户提供给它的引理\n以及所有标记为 `simp` 的引理重写目标。\n此外，如果提供了如`add_comm`这样的引理，它将尝试将对变量排序，以避免陷入无限循环。"}
+ "## 概述\n\nLean 的简化器 `simp` 将它将用每个用户提供给它的引理\n以及所有标记为 `simp` 的引理重写目标。\n此外，如果提供了如`add_comm`这样的引理，它将尝试将对变量排序，以避免陷入无限循环。"}
\ No newline at end of file
diff --git a/.i18n/zh/Game.po b/.i18n/zh/Game.po
index 7e81b4e2..ea0adea3 100644
--- a/.i18n/zh/Game.po
+++ b/.i18n/zh/Game.po
@@ -501,7 +501,7 @@ msgstr ""
 msgid ""
 "One day this game will have a Prime Number World, with a final boss\n"
 "of proving that $2$ is prime.\n"
-"To do this, we will have to rule out things like $2 = 37 × 42.$\n"
+"To do this, we will have to rule out things like $2 = 37 × 42$.\n"
 "We will do this by proving that any factor of $2$ is at most $2$,\n"
 "which we will do using this lemma. The proof I have in mind manipulates the "
 "hypothesis\n"
@@ -747,7 +747,7 @@ msgid ""
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all "
 "occurrences of\n"
-"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+"`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "再做一次！\n"
 "\n"
@@ -1023,11 +1023,11 @@ msgstr "`mul_zero m` 是 `m * 0 = 0` 的证明。"
 
 #: Game.Levels.Multiplication.L08add_mul
 msgid ""
-"Addition is distributive over multiplication.\n"
+"Multiplication is distributive over addition.\n"
 "In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
 "$(a + b) \\times c = ac + bc$."
 msgstr ""
-"加法和乘法有分配律。换句话说，对于所有自然数 $a$、$b$ 和 $c$，\n"
+"乘法对加法有分配律。换句话说，对于所有自然数 $a$、$b$ 和 $c$，\n"
 "我们有 $(a + b) \\times c = ac + bc$。"
 
 #: Game.Levels.Implication.L09zero_ne_succ
@@ -3968,7 +3968,7 @@ msgid ""
 "  the goal until it becomes our hypothesis! In other words, we\n"
 "  will \"argue backwards\". The `apply` tactic can do this too.\n"
 "  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+"  \"Typewriter mode\")."
 msgstr ""
 "在最后一关，我们操纵了假设 `x + 1 = 4`\n"
 "  直到成为目标 `x = 3` 。在这一关我们将改写\n"
@@ -4432,8 +4432,8 @@ msgid ""
 "We have seen how to `apply` theorems and assumptions\n"
 "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
 "To prove this goal, we need to know how to say \"let's assume `P` and deduce "
-"`Q`\"\n"
-"in Lean. We do this with the `intro` tactic."
+"`Q`\".\n"
+"In Lean, we do this with the `intro` tactic."
 msgstr ""
 "我们已经看到了如何 `apply` 形式为 `P → Q` 的定理和假设。\n"
 "但如果我们的 *目标* 是形式为 `P → Q` 的呢？\n"
@@ -4560,8 +4560,8 @@ msgstr "如果 $x$ 是自然数，则 $x \\le \\operatorname{succ}(x)$。"
 
 #: Game.Levels.Addition.L02succ_add
 msgid ""
-"Well done! You now have enough tools to tackle the main boss of this level."
-msgstr "做得好！现在你有足够的工具来对付这个关卡的大Boss了。"
+"Well done! You now have enough tools to tackle the main boss of this world."
+msgstr "做得好！现在你有足够的工具来对付这个世界的大Boss了。"
 
 #: Game.Levels.Multiplication.L04mul_comm
 msgid "Multiplication is commutative."
@@ -5000,12 +5000,12 @@ msgid ""
 "Did you use induction on `y`?\n"
 "Here's a two-line proof of `add_left_eq_self` which uses "
 "`add_right_cancel`.\n"
-"If you want to inspect it, you can go into editor mode by clicking `</>` in "
+"If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in "
 "the top right\n"
 "and then just cut and paste the proof and move your cursor around it\n"
 "to see the hypotheses and goal at any given point\n"
 "(although you'll lose your own proof this way). Click `>_` to get\n"
-"back to command line mode.\n"
+"back to \"Typewriter mode\".\n"
 "```\n"
 "nth_rewrite 2 [← zero_add y]\n"
 "exact add_right_cancel x 0 y\n"