merge it/Game.po and zh/Game.po with Game.pot, regenerate jsons

.i18n/it/Game.json

@@ -229,7 +229,7 @@
  "`a ≤ b` è *notazione* per `∃ c, b = a + c`. La \"E rovesciata\"\nsi legge \"esiste\". Quindi `a ≤ b` vuol dire che esiste\nun numero `c` tale che `b = a + c`. Questa definizione è valida\nperché non abbiamo i numeri negativi in questo gioco.\n\nPer *dimostrare* un \"esiste\", puoi usare la tattica `use`.\nVediamo un esempio.",
  "`a ≤ b` is *notation* for `∃ c, b = a + c`.\n\nBecause this game doesn't have negative numbers, this definition\nis mathematically valid.\n\nThis means that if you have a goal of the form `a ≤ b` you can\nmake progress with the `use` tactic, and if you have a hypothesis\n`h : a ≤ b`, you can make progress with `cases h with c hc`.":
  "`a ≤ b` è *notazione* per `∃ c, b = a + c`.\n\nDato che in questo gioco non abbiamo i numeri negativi, questa definizione\nè matematicamente valida.\n\nUna conseguenza pratica di tale definizione è che se hai un goal della forma `a ≤ b` puoi\nscomporlo con la tattica `use`, e se hai un'ipotesi\n`h : a ≤ b`, puoi scomporla tramite `cases h with c hc`.",
- "`a ≠ b` is *notation* for `(a = b) → False`.\n\nThe reason this is mathematically\nvalid is that if `P` is a true-false statement then `P → False`\nis the logical opposite of `P`. Indeed `True → False` is false,\nand `False → False` is true!\n\nThe upshot of this is that use can treat `a ≠ b` in exactly\nthe same way as you treat any implication `P → Q`. For example,\nif your *goal* is of the form `a ≠ b` then you can make progress\nwith `intro h`, and if you have a hypothesis `h` of the\nform `a ≠ b` then you can `apply h at h1` if `h1` is a proof\nof `a = b`.":
+ "`a ≠ b` is *notation* for `(a = b) → False`.\n\nThe reason this is mathematically\nvalid is that if `P` is a true-false statement then `P → False`\nis the logical opposite of `P`. Indeed `True → False` is false,\nand `False → False` is true!\n\nThe upshot of this is that you can treat `a ≠ b` in exactly\nthe same way as you treat any implication `P → Q`. For example,\nif your *goal* is of the form `a ≠ b` then you can make progress\nwith `intro h`, and if you have a hypothesis `h` of the\nform `a ≠ b` then you can `apply h at h1` if `h1` is a proof\nof `a = b`.":
  "`a ≠ b` è *notazione* per `(a = b) → False`.\n\nQuesta interpretazione è valida in matematica\nperché se `P` è una proposizione vero-falso allora `P → False`\nè la negazione logica di `P`. Infatti `True → False` è falso,\ne `False → False` è vero!\n\nIl vantaggio di questa notazione è che possiamo trattare una disuguaglianza `a ≠ b`\ncome se fosse un implicazione `P → Q`, che sappiamo già come manipolare. Ad esempio,\nse il tuo *goal* è una disuguaglianza `a ≠ b`, puoi fare progresso\ncon `intro h`, e se un'ipotesi `h` è una disuguaglianza\n`a ≠ b` allora puoi fare `apply h at h1` se `h1` è la prova di\ndi `a = b`.",
  "`Pow a b`, with notation `a ^ b`, is the usual\n  exponentiation of natural numbers. Internally it is\n  defined via two axioms:\n\n  * `pow_zero a : a ^ 0 = 1`\n\n  * `pow_succ a b : a ^ succ b = a ^ b * a`\n\nNote in particular that `0 ^ 0 = 1`.":
  "`Pow a b`, con notazione `a ^ b`, è\n  l'elevamento a potenza sui numeri naturali. Dentro Lean è\n  definita tramite due assiomi:\n\n  * `pow_zero a : a ^ 0 = 1`\n\n  * `pow_succ a b : a ^ succ b = a ^ b * a`\n\nIn particolare, dal primo segue che `0 ^ 0 = 1`.",
@@ -369,9 +369,9 @@
  "Il lemma precedente può essere usato per dimostrare questo.",
  "The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\nLet's prove one of these facts in this level, and the other in the next.\n\n## A new tactic: `cases`\n\nThe `cases` tactic will split an object or hypothesis up into the possible ways\nthat it could have been created.\n\nFor example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\nbut don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\nIn this situation you can use `cases b with d` instead. There are two ways to make\na number: it's either zero or a successor. So you will end up with two goals, one\nwith `b = 0` and one with `b = succ d`.\n\nAnother example: if you have a hypothesis `h : False` then you are done, because a false statement implies\nany statement. Here `cases h` will close the goal, because there are *no* ways to\nmake a proof of `False`! So you will end up with no goals, meaning you have proved everything.":
  "Il prossimo risultato di cui abbiamo bisogno per il Mondo `≤` è: se `a + b = 0` allora `a = 0` e `b = 0`.\nIn questo livello dimostriamo solo la prima parte della conclusione, la seconda nel livello successivo.\n\n## Nuova tattica: `cases`\n\nLa tattica `cases` scompone un oggetto o un'ipotesi in tutti i modi possibili\nin cui può essere stato creato.\n\nAd esempio, su un numero naturale a volte è sufficiente ragionare con i due casi `b = 0` e `b = succ d` separatamente,\ntralasciando l'ipotesi induttiva `hd` prodotta da `induction b with d hd`.\nIn questa situazione puoi usare `cases b with d`. Ci sono due modi per creare un numero:\ncome zero o come successore di qualcosa. `case` riprodurrà proprio queste due alternative, spezzando la dimostrazione in due sotto-goal, uno\ncon l'ipotesi `b = 0` e un'altro con l'ipotesi `b = succ d`.\n\nChiariamo con un altro esempio: se hai l'ipotesi `h : False` allora hai finito, perché un'affermazione falsa implica\nqualsiasi cosa. Qua `cases h` chiuderà la dimostrazione, perché *non* vi è alcun modo\ndi costruire una dimostrazione di `False`! Quindi rimarrai con zero sotto-goal da dimostrare, ossia hai dimostrato tutto.",
- "The music gets ever more dramatic, as we explore\nthe interplay between exponentiation and multiplication.\n\nIf you're having trouble exchanging the right `x * y`\nbecause `rw [mul_comm]` swaps the wrong multiplication,\nthen read the documentation of `rw` for tips on how to fix this.":
+ "The music gets ever more dramatic, as we explore\nthe interplay between exponentiation and multiplication.\n\nIf you're having trouble exchanging the right `a * b`\nbecause `rw [mul_comm]` swaps the wrong multiplication,\nthen read the documentation of `rw` for tips on how to fix this.":
  "La musica si fa sempre più drammatica nel mentre che ci addentriamo\nnella relazione tra elevamento a potenza e prodotto.\n\nSe stai avendo difficoltà a scambiare il giusto `x * y`\nperché `rw [mul_comm]` sta operando su un prodotto diverso,\nleggi la documentazione di `rw` per ripassare come fare sostituzioni mirate.",
- "The music dies down. Is that it?\n\nCourse it isn't, you can\nclearly see that there are two worlds left.\n\nA passing mathematician says that mathematicians don't have a name\nfor the structure you just constructed. You feel cheated.\n\nSuddenly the music starts up again. This really is the final boss.":
+ "The music dies down. Is that it?\n\nCourse it isn't, you can\nclearly see that there are two levels left.\n\nA passing mathematician says that mathematicians don't have a name\nfor the structure you just constructed. You feel cheated.\n\nSuddenly the music starts up again. This really is the final boss.":
  "La musica cessa di suonare. È finita?\n\nOvvio che no, come vedi\nci sono ancora due livelli da battere.\n\nIntanto, un matematico di passaggio ti svela che i matematici non hanno dato un nome\nalla struttura che hai appena costruito. Questa notizia ti lascia l'amaro in bocca.\n\nLa musica riparte improvvisamente. Ti lasci alle spalle il passato: lo scontro con il boss finale è vicino.",
  "The lemma proved in the final level of this world will be helpful\nin Divisibility World.":
  "Il lemma dimostrato nel livello finale di questo mondo ci sarà d'aiuto\nnel Mondo Divisibilità.",
@@ -405,7 +405,7 @@
  "Inizia con `induction «{y}» with d hd`.",
  "Start with `have h2 := mul_ne_zero a b`.":
  "Inizia con `have h2 := mul_ne_zero a b`.",
- "Start with `contrapose! h`, to change the goal into its\ncontrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`.":
+ "Start with `contrapose! h`, to change the goal into its\ncontrapositive, namely a hypothesis of `succ m = succ n` and a goal of `m = n`.":
  "Inizia con `contrapose! h`, che ti fa dimostrare la\ncontronominale del goal, cioè avrai tra le ipotesi la negazione del goal, `succ m = succ m`, e come nuovo goal avrai la negazione dell'ipotesi `h`, `m = n`.",
  "Start with `cases «{hxy}» with a ha`.":
  "Inizia con `cases «{hxy}» with a ha`.",
@@ -450,6 +450,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 degno di premio Oscar, 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`.":
+ "Nel Mondo Numeri Primi dimostreremo che $2$ è primo.\nMa per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42.$\nLo faremo mostrando 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 diventa il goal, usando praticamente tutto ciò che abbiamo dimostrato in questo mondo finora.",
  "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). $":
@@ -493,14 +495,14 @@
  "Ora `«{ha}»` è una dimostrazione di `«{y}» = «{x}» + «{a}»`, mentre `hxy` è scomparso. In modo simile, puoi scomporre\n`«{hyz}»` nelle sue varie parti tramite `cases «{hyz}» with b hb`.",
  "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`.":
  "Ora con `rw [← two_eq_succ_one]` `succ 1` diventa `2`.",
+ "Now `rw [«{h}»] at «{h2}»` so you can `apply le_one at «{h2}»`.":
+ "Adesso `rw [h] at h2` così puoi fare `apply le_one at hx`.",
  "Now `rw [h]` then `rfl` works, but `exact h` is quicker.":
  "Ora potresti usare `rw [h]` e `rfl` in successione, ma `exact h` è più elegante.",
- "Now `rw [h] at h2` so you can `apply le_one at hx`.":
- "Adesso `rw [h] at h2` così puoi fare `apply le_one at hx`.",
  "Now `rw [add_zero]` will change `c + 0` into `c`.":
  "Ora `rw [add_zero]` trasformerà `c + 0` in `c`.",
  "Now `rfl` will work.": "Adesso `rfl` funzionerà.",
- "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\nchange `succ x = succ y`.":
+ "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\nchange `h` to `succ x = succ y`.":
  "Adesso puoi fare `repeat rw [← succ_eq_add_one] at h` per fare due sostituzioni in un colpo\ne avrai `succ x = succ y`.",
  "Now `exact h` finishes the job.": "Ora concludi con `exact h`.",
  "Now `cases «{h2}» with e he`.": "Ora `cases «{h2}» with e he`.",
@@ -526,7 +528,7 @@
  "Natural Number Game": "Il Gioco dei Numeri Naturali",
  "My proof:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```":
  "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 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.":
+ "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 di norma 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 hanno\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 su cosa fa.",
  "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$.",
@@ -576,14 +578,14 @@
  "In questo mondo non parlerò troppo.\n\n`add_right_cancel a b n` è il teorema che afferma $a+n=b+n\\implies a=b$.",
  "In this level, we see inequalities as *hypotheses*. We have not seen this before.\nThe `cases` tactic can be used to take `hxy` apart.":
  "In questo livello, abbiamo delle disuguaglianze tra le *ipotesi*. Non abbiamo ancora visto questo caso.\nLa tattica `cases` può essere usata per scomporre l'ipotesi `hxy`.",
+ "In this level, the hypotheses `h2` is an *implication*. It says\nthat *if* `x = 37` *then* `y = 42`. We can use this\nhypothesis with the `apply` tactic. Remember you can click on\n`apply` or any other tactic on the right to see a detailed explanation\nof what it does, with examples.":
+ "",
  "In this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n\nWait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\nThis is `zero_add`, which is different.\n\nThe difficulty with proving `0 + n = n` is that we do not have a *formula* for\n`0 + n` in general, we can only use `add_zero` and `add_succ` once\nwe know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n\nThe base case will require us to prove `0 + 0 = 0`, and the inductive step\nwill ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because\n`0` and successor are the only way to make numbers, this will cover all the cases.\n\nSee if you can do your first induction proof in Lean.\n\n(By the way, if you are still in the \"Editor mode\" from the last world, you can swap\nback to \"Typewriter mode\" by clicking the `>_` button in the top right.)":
  "In questo livello dimostreremo l'enunciato $0+n=n$, dove $n$ è un numero naturale incognito.\n\nMa come, non l'abbiamo già dimostrato? No! Abbiamo dimostrato $n+0=n$, che abbiamo chiamato `add_zero`.\nQuesto è `zero_add`, un teorema diverso.\n\nCiò che complica le cose nel dimostrare `0 + n = n` è che non abbiamo una *formula* per riscrivere\n`0 + n` in generale, possiamo solo applicare `add_zero` o `add_succ` una volta che sappiamo che\n`n` è `0` oppure un successore. La tattica `induction` spezza la dimostrazione in questi due casi.\n\nNel caso base dovremo dimostrare `0 + 0 = 0`, e nel caso induttivo dovremo dimostrare\nche se `0 + d = d` allora `0 + succ d = succ d`. Dato che\n`0` e il successore sono i due soli modi per costruire i numeri naturali, la dimostrazione coprirà tutti i casi possibili.\n\nOra prova a svolgere la tua prima dimostrazione per induzione su Lean.\n\n(Se sei ancora nella \"Modalità editor\" dallo scorso mondo, puoi rientrare nella\n\"Modalità interattiva\" cliccando sul pulsante `>_` in alto a destra.)",
- "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\nseveral reasons. One of these is that\nwe need to introduce a new idea: we will need to understand the concept of\nmathematical induction a little better.\n\nStarting with `induction b with d hd` is too naive, because in the inductive step\nthe hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\nso the induction hypothesis does not apply!\n\nAssume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,\nbecause we now have the flexibility to change `c`.\"":
+ "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\nseveral reasons. One of these is that\nwe need to introduce a new idea: we will need to understand the concept of\nmathematical induction a little better.\n\nStarting with `induction b with d hd` is too naive, because in the inductive step\nthe hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\nso the induction hypothesis does not apply!\n\nAssume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n\"for all `c`, if `a * b = a * c` then `b = c`\". This *can* be proved by induction,\nbecause we now have the flexibility to change `c`.":
  "In questo livello dimostriamo se `a * b = a * c` e `a ≠ 0` allora `b = c`. È un pò complicato, per\ndiverse ragioni. Una di queste è che\nabbiamo bisogno di introdurre una nuova idea, approfondendo la nozione di\ninduzione matematica.\n\nSarebbe ingenuo partire con `induction b with d hd`, perché nel passo induttivo\nl'ipotesi è `a * d = a * c → d = c` ma quello che sappiamo è solo che `a * succ d = a * c`,\ndunque non possiamo applicare l'ipotesi ipotesi induttiva!\n\nSupponiamo di fissare la variabile `a ≠ 0`. Il vero enunciato che vogliamo dimostrare per induzione su `b` è\n\"per tutte le `c`, se `a * b = a * c` allora `b = c`\". Questo *può* essere dimostrato per induzione,\nperché abbiamo permesso alla `c` di variare.",
  "In this level the *goal* is $2y=2(x+7)$ but to help us we\nhave an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\nyour list of assumptions. Lean thinks of `h` as being a secret proof of the\nassumption, rather like `x` is a secret number.\n\nBefore we can use `rfl`, we have to \"substitute in for $y$\".\nWe do this in Lean by *rewriting* the proof `h`,\nusing the `rw` tactic.":
  "In questo livello il *goal* è $2y=2(x+7)$ e l'unica informazione che\npuò aiutarci a dimostrarlo è l'*ipotesi* `h` che dice $y = x + 7$. Verifica di avere `h` sotto la voce \"Ipotesi\".\nLean vede `h` come una dimostrazione segreta dell'ipotesi,\nun po' come il valore della variabile `x` è un'incognita.\n\nPrima di poter usare la tattica `rfl`, dobbiamo \"sostituire per la variabile $y$\".\nIn Lean possiamo *riscrivere* la dimostrazione `h`\nattraverso la tattica `rw`.",
- "In this level one of our hypotheses is an *implication*. We can use this\nhypothesis with the `apply` tactic.":
- "In questo livello una delle nostre ipotesi è un'*implicazione*. Possiamo usare\nquesta ipotesi con la tattica `apply`.",
  "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\nlearning the basics about theorem proving in Lean.\n\nThis is a good first introduction to Lean!":
  "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.":
@@ -596,8 +598,6 @@
  "Nei mondi successivi ci sono livelli molto più brutti\ncome `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\nQui le parentesi vanno spostate, e le variabili vanno scambiate tra di loro.\n\nIn questo livello, `(a + b) + (c + d) = ((a + c) + d) + b`,\ndimentichiamoci delle parentesi e concentriamoci solamente\nsull'ordine delle variabili.\nPer portare `a+b+c+d` a `a+c+d+b` dobbiamo scambiare `b` con `c`,\ne poi scambiare `b` con `d`. Questo è più facile di quanto\npensi tramite `add_left_comm`.",
  "In order to use the tactic `rfl` you can enter it in the text box\nunder the goal and hit \"Execute\".":
  "Per utilizzare la tattica `rfl` digitala nella casella di testo\nsotto il goal e premi \"Esegui\".",
- "In Prime Number World we will be 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 pretty much everything which we've proved in this world so far.":
- "Nel Mondo Numeri Primi dimostreremo che $2$ è primo.\nMa per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42.$\nLo faremo mostrando 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 diventa il goal, usando praticamente tutto ciò che abbiamo dimostrato in questo mondo finora.",
  "In Advanced Addition World we will prove some basic\naddition facts such as $x+y=x\\implies y=0$. The theorems\nproved in this world will be used to build\na theory of inequalities in `≤` World.\n\nClick on \"Start\" to proceed.":
  "Nel Mondo Addizione Avanzata dimostreremo delle proprietà\nbasilari dell'addizione come $x+y=x\\implies y=0$. I teoremi\ndimostrati in questo mondo servono da mattoncini teorici con cui costruiremo\nla teoria delle disuguaglianze nel Mondo `≤`.\n\nPremi su \"Via\" per iniziare.",
  "Implication World": "Mondo Implicazione",
@@ -665,6 +665,8 @@
  "Come ti sembra questa dimostrazione:\n\n```\nrw [add_comm]\nexact add_right_eq_zero b a\n```\n\nQuesto è tutto per il Mondo Addizione Avanzata! I teoremi di questo mondo ti torneranno utili\nnel prossimo mondo, il Mondo `≤`. Clicca su \"Abbandona mondo\" per navigarci.",
  "Here's what I was thinking of:\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```":
  "Ecco quello che avevo in mente:\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```",
+ "Here's the short proof:\n```\nhave h2 := mul_ne_zero a b\ntauto\n```\nThis works because, given `mul_ne_zero a b`,\nthe argument is reduced to pure logic.":
+ "",
  "Here's my solution:\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```":
  "Ecco come l'ho fatta io:\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```",
  "Here's my solution:\n```\nrw [mul_comm, mul_one]\nrfl\n```":
@@ -685,7 +687,7 @@
  "Ecco una dimostrazione di due righe:\n```\nuse 1\nexact succ_eq_add_one x\n```\n\nQuesto funziona perché `succ_eq_add_one x` è la dimostrazione di `succ x = x + 1`.",
  "Here's a two-line proof:\n```\nrepeat rw [zero_add] at h\nexact h\n```":
  "Ecco una dimostrazione di due righe:\n```\nrepeat rw [zero_add] at h\nexact h\n```",
- "Here's a proof using `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\nand here's an even shorter one using the same idea:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nAlternatively you can just prove it by induction on `x`\n(the dots in the proof just indicate the two goals and\ncan be omitted):\n\n```\n  induction x with d hd\n  · intro h\n    rw [zero_add] at h\n    assumption\n  · intro h\n    rw [succ_add] at h\n    apply succ_inj at h\n    apply hd at h\n    assumption\n```":
+ "Here's a proof using `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\nand here's an even shorter one using the same idea:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nAlternatively you can just prove it by induction on `x`:\n\n```\ninduction x with d hd\nintro h\nrw [zero_add] at h\nexact h\nintro h\nrw [succ_add] at h\napply succ_inj at h\napply hd at h\nexact h\n```":
  "Ecco una dimostrazione che usa `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\ned eccone una più breve che condensa le ultime tre righe in una sola:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nVolendo puoi anche dimostrarlo per induzione su `x`\n(i pallini nel codice qui sotto hanno solo funzione decorativa,\nassieme all'indentazione servono per riconoscere più facilmente i due sottogoal, ma possono essere omessi):\n\n```\n  induction x with d hd\n  · intro h\n    rw [zero_add] at h\n    assumption\n  · intro h\n    rw [succ_add] at h\n    apply succ_inj at h\n    apply hd at h\n    assumption\n```",
  "Here's a completely backwards proof:\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```":
  "Ecco una dimostrazione che procede all'indietro:\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```",
@@ -745,7 +747,7 @@
  "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```":
  "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.":
+ "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World (when someone gets around to\nimplementing it).":
  "Congratulazioni! Hai finito il Mondo Algoritmi. Questi algoritmi\nti saranno sicuramente utili per il Mondo Pari-Dispari.",
  "Congratulations! You have proved Fermat's Last Theorem!\n\nEither that, or you used magic...":
  "Congratulazioni! Hai dimostrato l'ultimo teorema di Fermat!\n\nO forse no... ti ho visto usare la polvere magica...",
@@ -805,7 +807,7 @@
  "2 + 2 ≠ 5": "2 + 2 ≠ 5",
  "1 ≠ 0": "1 ≠ 0",
  "0 ≤ x": "0 ≤ x",
- "*Game version: 4.2*\n\n*Recent additions: Inequality world, algorithm world*\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.":
+ "*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: Mondo Disequazioni, Mondo Algoritmi*\n\n## Salvataggio del gioco\n\nIl gioco salva il tuo progresso nella memoria locale del browser.\nSe cancelli la memoria, perderai anche i dati del gioco! (le tue preziose dimostrazioni!)\n\nAttenzione: nella maggior parte dei browser, cancellare i cookies cancella 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$.",
@@ -832,7 +834,7 @@
  "## Descrizione\n\n`repeat t` applica la tattica `t`\nnel goal ripetitivamente. Non è necessario usare questa tattica\nper completare il gioco, ma a volte è utile nel rendere le dimostrazioni più succinte.\n\n## Esempio\n\n`repeat rw [add_zero]` trasformerà il goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\nnel nuovo goal\n`a = b`.\n\"\n\nTacticDoc nth_rewrite \"\n## Descrizione\n\nSe hai `h : X = Y` e ci sono diverse `X` nel goal, allora\n`nth_rewrite 3 [h]` sostituirà solo la terza `X` in `Y`.\n\n## Esempio\n\nSe nel goal hai `2 + 2 = 4` allora con `nth_rewrite 2 [two_eq_succ_one]`\nsostituisce la seconda occorrenza del lato sinistro di `two_eq_succ_one`, e il goal diventa `2 + succ 1 = 4`. Invece il normale `rw [two_eq_succ_one]`\nsostituira la prima occorrenza di `2` nel goal, che diventa `succ 1 + succ 1 = 4`.",
  "## Summary\n\n`repeat t` repeatedly applies the tactic `t`\nto the goal. You don't need to use this\ntactic, it just speeds things up sometimes.\n\n## Example\n\n`repeat rw [add_zero]` will turn the goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\ninto the goal\n`a = b`.":
  "## Descrizione\n\n`repeat t` applica la tattica `t`\nnel goal ripetitivamente. Non è strettamente necessaria al fine di\ncompletare il gioco, ma a volte è utile per velocizzare le dimostrazioni.\n\n## Esempio\n\n`repeat rw [add_zero]` trasformerà il goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\nnel nuovo goal\n`a = b`.",
- "## Summary\n\nThe `use` tactic makes progress with goals which claim something *exists*.\nIf the goal claims that some `x` exists with some property, and you know\nthat `x = 37` will work, then `use 37` will make progress.\n\nBecause `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\nyou can make progress on goals of the form `a ≤ b` by `use`ing the\nnumber which is morally `b - a`.":
+ "## Summary\n\nThe `use` tactic makes progress with goals which claim something *exists*.\nIf the goal claims that some `x` exists with some property, and you know\nthat `x = 37` will work, then `use 37` will make progress.\n\nBecause `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\nyou can make progress on goals of the form `a ≤ b` by `use`ing the\nnumber which is morally `b - a` (i.e. `use b - a`)\n\nAny of the following examples is possible assuming the type of the argument passed to the `use` function is accurate:\n\n- `use 37`\n- `use a`\n- `use a * a + 1`":
  "## Descrizione\n\nLa tattica `use` permette di avanzare su goal che postulano l'*esistenza* di qualcosa.\nSe il goal afferma che esiste una certa `x`con qualche proprietà, e sei sicuro\nche `x = 37` la soddisfi, allora con `use 37` farai progresso nella dimostrazione.\n\nDato che `a ≤ b` è notazione per \\\"there exists `c` such that `b = a + c`\\\",\npuoi fare progresso su goal della forma `a ≤ b` passando a `use`\nquel numero che corrisponde a `b - a`, la distanza tra `a` e `b`.",
  "## Summary\n\nThe `symm` tactic will change a goal or hypothesis of\nthe form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\nand on `X ↔ Y`.\n\n### Example\n\nIf the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n\n### Example\n\nIf `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`.":
  "## Descrizione\n\nLa tattica `symm` trasformerà un goal o un'ipotesi della forma di\nun'uguaglianza `X = Y` in `Y = X`. Funziona anche sulla disuguaglianza `X ≠ Y`\ne sull'equivalenza `X ↔ Y`.\n\n### Esempio\n\nSe il goal è `2 + 2 = 4`, `symm` lo trasformerà in `4 = 2 + 2`.\n\n### Esempio\n\nSe hai `h : 2 + 2 ≠ 5` allora `symm at h` trasformerà `h` in `5 ≠ 2 + 2`.",
@@ -846,13 +848,13 @@
  "## Descrizione\n\nSe `n` è un numero, allora `cases n with d` spezzerà il goal in due goal,\nuno dove `n = 0` e un altro dove `n = succ d`.\n\nSe `h` è una dimostrazione (per esempio tra le ipotesi), allora `cases h with...` spezzerà\nla dimostrazione in tante parti quante quanti i modi di derivare `h`.\n\n## Esempio\n\nSe `n : ℕ` è un numero, allora `cases n with d` spezzerà il goal in due subgoal,\nuno dove `n` è stato rimpiazzato da 0 e l'altro dove `n` è stato rimpiazzato da `succ d`. Questo\ncorrisponde all'intuizione matematica che ogni numero naturale è o `0`\noppure un successore.\n\n## Esempio\n\nSe `h : P ∨ Q` è un'ipotesi, allora `cases h with hp hq` trasformerà il goal\nin due goal, uno con l'ipotesi `hp : P` e l'altro con\nl'ipotesi `hq : Q`.\n\n## Esempio\n\nSe `h : False` è un'ipotesi, allora `cases h` trasformerà il goal in zero goal,\nperché non vi è alcun modo di dimostrare `False`! E se rimani con zero cose da dimostrare\nvuol dire che hai completato il livello.\n\n## Esempio\n\nSe `h : a ≤ b` è un'ipotesi, allora `cases h with c hc` istanzierà un nuovo numero `c`\ne una dimostrazione di `hc : b = a + c`. Questo deriva dalla *definizione* di `a ≤ b`, che è\n`∃ c, b = a + c`.",
  "## Summary\n\nIf `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\nattempts to prove the goal by induction on `n`, with the inductive\nvariable in the successor case being `d`, and the inductive hypothesis being `hd`.\n\n### Example:\nIf the goal is\n```\n0 + n = n\n```\n\nthen\n\n`induction n with d hd`\n\nwill turn it into two goals. The first is `0 + 0 = 0`;\nthe second has an assumption `hd : 0 + d = d` and goal\n`0 + succ d = succ d`.\n\nNote that you must prove the first\ngoal before you can access the second one.":
  "## Descrizione\n\nSe `n : ℕ` è un oggetto, e il goal fa il nome di `n`, allora `induction n with d hd`\navvia la dimostrazione per induzione attorno alla variabile `n`, con la variabile\ninduttiva nel caso del successore chiamata `d` e l'ipotesi induttiva chiamata`hd`.\n\n### Esempio:\nSe il goal è\n```\n0 + n = n\n```\n\nallora\n\n`induction n with d hd`\n\nlo spezzerà in sue sotto-goal. Il primo è `0 + 0 = 0`;\nil secondo porta ha con sé un ipotesi `hd : 0 + d = d` e il goal\n`0 + succ d = succ d`.\n\nTieni presente che devi dimostrare il primo\ngoal prima di avere accesso al secondo.",
- "## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`'s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.":
+ "## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.":
  "## Descrizione\n\nSe `h` è una prova dell'uguaglianza `X = Y`, allora `rw [h]` scriverà\n`Y` al posto di ogni `X` nel goal. `rw` svolge l'operazione di \\\"sostituzione\\\".\n\n## Varianti di `rw`\n\n* `rw [← h]` (riscrive le `Y` con `X`; per avere la freccetta all'indietro si digita `\\left ` oppure `\\l`.)\n\n* `rw [h1, h2]` (sostituzioni in sequenza)\n\n* `rw [h] at h2` (riscrive le `X` in `Y` nell'ipotesi `h2`)\n\n* `rw [h] at h1 h2 ⊢` (riscrive le `X` in `Y` in due ipotesi e nel goal;\nper avere il simbolo `⊢` digita `\\|-`.)\n\n* `repeat rw [add_zero]` riscriverà continuamente `? + 0` in `?`\nfinché non riesce più a trovare espressioni della forma `? + 0`.\n\n* `nth_rewrite 2 [h]` riscriverà solo la seconda `X` nel goal in `Y`.\n\n### Esempio:\n\nSe hai l'ipotesi `h : x = y + y` e il goal è\n```\nsucc (x + 0) = succ (y + y)\n```\n\nallora il comando\n\n`rw [add_zero]`\n\nriscriverà il goal in `succ x = succ (y + y)`, e poi il comando\n\n`rw [h]`\n\nriscriverà il goal in `succ (y + y) = succ (y + y)`, il quale\npuò essere risolto con `rfl`.\n\n### Esempio:\n\n`rw` può anche riscrivere nelle ipotesi.\nAd esempio, se hai le seguenti due ipotesi:\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\neseguendo `rw [h1] at h2` sostituirà la `x` dentro `h2`, che diventerà `h2 : 2 * y = y + 3`.\n\n## Errori comuni\n\n* `rw` accetta una lista di teoremi, dunque le parentesi quadre sono sempre da mettere. Scrivere `rw h` è un errore di sintassi.\n\n* Inoltre, gli argomenti che passi a `rw` devono essere *prove* di *uguaglianza*, dunque dei teoremi che hai dimostrato in precedenza e che hanno la forma`A = B`).\nScrivere `rw [P = Q]` è sbagliato: `P = Q` è solo l'*affermazione* dell'uguaglianza,\nnon la sua dimostrazione. Se invece hai `h : P = Q` nel contesto, `h` è una dimostrazione di `P = Q` e allora potrai scrivere `rw [h]`.\n\n## Dettagli\n\n`rw` è la tattica che svolge la \\\"sostituzione\\\". Ci sono due casi in cui può\nessere usata:\n\n1) Uso basilare: se `h : A = B` è un'ipotesi del contesto\noppure la dimostrazione di un teorema, e se il goal contiene una o più `A`, allora `rw [h]`\nle sostituirà tutte con `B`. La tattica darà un errore\nse non ci sono `A` nel goal.\n\n2) Uso avanzato: certi teoremi hanno delle incognite.\n Ad esempio, `add_zero`\npuò essere trattato come un funzione il cui corpo è `? + 0 = ?`\ndove `?` è l'input. Applicando `rw` a `add_zero`, `rw` cercherà all'interno del goal\nun termine della forma `x + 0`; appena lo trova\nfissa l'incognita `?` a `x` e cambierà tutte le occorrenze di `x + 0` a `x`.\n\nEsercizio: prova a spiegare perché `rw [add_zero]` trasforma il termine\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` in\n`0 + (x + 0) + 0 + (x + 0)`\n\nSe non ti ricordi il nome di una dimostrazione di un'uguaglianza, puoi cercarlo\nnell'elenco di lemma sulla destra.\n\n## Uso mirato\n\nSe nel goal hai `b + c + a = b + (a + c)` e vuoi riscrivere solo il termine `a + c`\na `c + a`, invocare semplicemente `rw [add_comm]` non darà il risultato che ti aspetti perché Lean\napplica il teorema sulla prima espressione che ha un match con un'addizione. Puoi usare `rw [add_comm a c]` per\nfar sì che Lean riscriva `a + c` a `c + a`. In questo modo stai fissando le incognite del teorema:\n`add_comm` è la prova di `?1 + ?2 = ?2 + ?1`, `add_comm a` è la prova\ndi `a + ? = ? + a`, e infine `add_comm a c` è la prova di `a + c = c + a`.\n\nData la dimostrazione `h : X = Y`, `rw [h]` riscriverà tutte le `X` a `Y` nel goal.\nPer cambiare solo la trentasettesima occorrenza di `X`\na `Y`, il metodo giusto è `nth_rewrite 37 [h]`.",
  "## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.":
  "## Descrizione\n\nSe hai `h : X = Y` e nel goal ci sono diverse `X`, con\n`nth_rewrite 3 [h]` puoi cambiare solo la terza `X` in `Y`.\n\n## Esempio\n\nSe il goal è `2 + 2 = 4` allora `nth_rewrite 2 [two_eq_succ_one]`\nsostituirà la seconda occorrenza di `2`, e il goal diventerà `2 + succ 1 = 4`. Invece, il semplice `rw [two_eq_succ_one]`\nsostituirà tutte le occorrenze di `2` e il goal diventerà `succ 1 + succ 1 = 4`.",
  "## Precision rewriting\n\nIn the last level, there was `b + 0` and `c + 0`,\nand `rw [add_zero]` changed the first one it saw,\nwhich was `b + 0`. Let's learn how to tell Lean\nto change `c + 0` first by giving `add_zero` an\nexplicit input.":
  "## Rewriting mirato\n\nNell'ultimo livello vi erano sia `b + 0` che `c + 0` da riscrivere,\ne `rw [add_zero]` ha scelto il primo che ha trovato,\nossia `b + 0`. Impariamo come dire a Lean\ndi riscrivere `c + 0` per primo dando ad `add_zero` un\ninput esplicito.",
- "# Welcome to the Natural Number Game\n#### An introduction to mathematical proof.\n\nIn this game, we will build the basic theory of the natural\nnumbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\nthat `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\nAnd at the end we'll see if we can prove Fermat's Last Theorem.\nWe'll do this by solving levels of a computer puzzle game called Lean.\n\n# Read this.\n\nLearning how to use an interactive theorem prover takes time.\nTests show that the people who get the most out of this game are\nthose who read the help texts like this one.\n\nTo start, click on \"Tutorial World\".\n\nNote: this is a new Lean 4 version of the game containing several\nworlds which were not present in the old Lean 3 version. A new version\nof Advanced Multiplication World is in preparation, and worlds\nsuch as Prime Number World and more will be appearing during October and\nNovember 2023.\n\n## More\n\nClick on the three lines in the top right and select \"Game Info\" for resources,\nlinks, and ways to interact with the Lean community.":
+ "# Welcome to the Natural Number Game\n#### An introduction to mathematical proof.\n\nIn this game, we will build the basic theory of the natural\nnumbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\nthat `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\nAnd at the end we'll see if we can prove Fermat's Last Theorem.\nWe'll do this by solving levels of a computer puzzle game called Lean.\n\n# Read this.\n\nLearning how to use an interactive theorem prover takes time.\nTests show that the people who get the most out of this game are\nthose who read the help texts like this one.\n\nTo start, click on \"Tutorial World\".\n\nNote: this is a new Lean 4 version of the game containing several\nworlds which were not present in the old Lean 3 version. More new worlds\nsuch as Strong Induction World, Even/Odd World and Prime Number World\nare in development; if you want to see their state or even help out, checkout\nout the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues).\n\n## More\n\nClick on the three lines in the top right and select \"Game Info\" for resources,\nlinks, and ways to interact with the Lean community.":
  "# Benvenuto nel Gioco dei Numeri Naturali!\n#### Un'introduzione alla dimostrazione matematica.\n\nIn questo gioco costruiremo la teoria elementare dei numeri naturali\n`{0,1,2,3,4,...}` a partire da zero. Il nostro primo obiettivo è dimostrare\n`2 + 2 = 4`. Dopodiché dimostreremo `x + y = y + x`.\nInfine cercheremo di dimostrare l'Ultimo Teorema di Fermat.\nRisolveremo questi puzzle matematici in un ambiente interattivo chiamato Lean.\n\n# Leggi le istruzioni!\n\nImparare a usare un *interactive theorem prover* richiede tempo e impegno.\nLe statistiche mostrano che le persone che imparano di più da questo gioco sono\ncoloro che leggono attentamente il testo delle istruzioni, come questo.\n\nPer iniziare, clicca su \"Mondo Tutorial\".\n\nNota: questa è la versione del gioco per Lean 4 contenente diversi\nmondi che non erano presenti nella versione per Lean 3. Stiamo lavorando a una\nnuova versione del Mondo Moltiplicazione Avanzata e nuovi mondi\ntra cui Mondo Numeri Primi arriveranno durante Ottobre e\nNovembre 2023.\n\n## Altro\n\nClicca sulle tree lineette in alto a destra e seleziona \"Game Info\" per risorse,\nlink utili e vari modi per connetterti alla comunità di Lean.",
  "# Summary\nThe `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `Q` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $Q \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.":
  "# Descrizione\nLa tattica `right` trasforma un goal della forma `P ∨ Q` nel nuovo goal `Q`.\nUsala quando le tue ipotesi garantiscono che si può dedurre `P ∨ Q`\n\ndalla verità di `Q`.\n\nL'implementazione di Lean di questa tattica non fa altro che `apply` di un teorema\nche dice che $Q \\implies P \\lor Q.$\n\nNota bene che questa tattica può portare il tuo goal a uno stato irrisolvibile.",
@@ -862,9 +864,9 @@
  "# Descrizione\n\n`trivial` risolve il goal `True`.",
  "# Summary\n\n`decide` will attempt to solve a goal if it can find an algorithm which it\ncan run to solve it.\n\n## Example\n\nA term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\nare equal or different. Hence, once this term is made and made into an `instance`,\nthe `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.":
  "# Descrizione\n\nLa tattica `decide` cercherà di risolvere il goal se esiste un algoritmo\nche possiamo eseguire per risolverlo.\n\n## Esempio\n\nUn termine di tipo `DecidableEq ℕ` è un algoritmo che decide se due naturali\nsono uguali o diversi. Dunque, se abbiamo un'istanza di questo tipo,\nla tattica `decide` può usare la sua implementazione per risolvere i goal della forma `a = b` or `a ≠ b`.",
- "# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n\n## Example\n\nIf you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.":
+ "# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Details\n\n`tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication,\nit doesn't even know `add_zero`. The only things that `tauto` knows about numbers\nare firstly that `a = a` and secondly that `0 ≠ 1`, `0 ≠ 2`, `1 ≠ 2` and so on.\nWhat `tauto`'s strength is, is *logic*. If you have a hypothesis `x < 37`\nand another hypothesis `x < 37 → y + z = 42` and your goal is `y + z = 42` then `tauto` will\nsolve this goal, because to solve that goal you don't need to know any facts\nabout inequalities or addition, all you need to know is the rules of logic.\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n\n## Example\n\nIf you have a hypothesis `h : 0 = 1` then `tauto` will solve the goal, because\n`tauto` knows `0 ≠ 1` and this is enough to prove `False`, which implies any goal.\n\n## Example\n\nIf you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.":
  "# Descrizione\n\nLa tattica `tauto` risolverà qualsiasi goal che può essere tramite puro ragionamento logico (ossia, tramite le\ntavole di verità).\n\n## Esempio\n\nSe hai `False` come ipotesi, allora `tauto` risolverà\nil goal. Questo perché un'ipotesi false implica qualsiasi cosa.\n\n## Esempio\n\nSe hai il goal `True`, allora `tauto` risolverà il goal.\n\n## Esempio\n\nSe hai due ipotesi `h1 : a = 37` e `h2 : a ≠ 37` allora `tauto` risolverà\nsolve il goal perché può dedurre `False` dalle tue ipotesi, e quindi\ndimostrare il goal (dato che `False` implica qualsiasi cosa).\n\n## Esempio\n\nSe hai un'ipotesi `h : a ≠ a` allora `tauto` risolverà il goal perché\nè abbastanza intelligente da capire che `a = a` è vero, arrivando alla contraddizione che cerchiamo.\n\n## Esempio\n\nSe hai un'ipotesi della forma `a = 0 → a * b = 0` e hai il goal `a * b ≠ 0 → a ≠ 0`, allora\n`tauto` risolverà il goal, because esso è logicamente equivalente all'ipotesi.\nE se scambi il ruolo del goal e dell'ipotesi in questo esempio, `tauto` lo risolverebbe lo stesso.",
- "# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.":
+ "# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. For example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.":
  "# Descrizione\n\nLa tattica `have` può essere usata per aggiungere un'ipotesi a un livello, ma ovviamente ti chiede\ndi dimostrarla.\n\n\n## Esempio\n\nIl suo utilizzo più semplice e così. Se hai `a` nel contesto e vuoi eseguire\n\n`have ha : a = 0`\n\nallora otterrai un nuovo goal `a = 0` da dimostrare, e dopo che l'hai dimostrato\navrai l'ipotesi `ha : a = 0` nel contesto originale.\n\n## Esempio\n\nSe hai già pronta la dimostrazione di ciò che vuoi introdurre con `have`,\npuoi farlo in un unico comando. Ad esempio, se hai `a` e `b`\ncome numeri, allora\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\naggiungerà direttamente l'ipotesi `h2 : succ a = succ b → a = b`\nal contesto, dato che hai fornito assieme la sua dimostrazione (`succ_inj a b`).\n\n## Esempio\n\nSe hai in mano una dimostrazione, puoi omettere il lemma che vuoi introdurre (quello tra i simboli `:` e `:=`).\nAd esempio:\n\n`have h2 := succ_inj a b`\n\naggiungerà `h2 : succ a = succ b → a = b` come ipotesi.",
  "# Summary\n\nIf you have a hypothesis\n\n`h : a ≠ b`\n\nand goal\n\n`c ≠ d`\n\nthen `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\na hypothesis\n\n`h : c = d`\n\nand goal\n\n`a = b`.":
  "# Descrizione\n\nSe hai un'ipotesi\n\n`h : a ≠ b`\n\ne il goal\n\n`c ≠ d`\n\nallora `contrapose! h` cambierà l'impostazione con la cosiddetta \\\"contronominale\\\":\nun ipotesi\n\n`h : c = d`\n\ne il goal\n\n`a = b`.",

.i18n/zh/Game.json

@@ -217,7 +217,7 @@
  "`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。这个“倒 E”代表“存在”。所以 `a ≤ b` 意味着存在一个数字 `c` 使得 `b = a + c`。这个定义有效是因为在这个游戏中没有负数。\n\n要*证明*一个“存在性”定理，可以使用 `use` 策略。\n让我们看一个例子。",
  "`a ≤ b` is *notation* for `∃ c, b = a + c`.\n\nBecause this game doesn't have negative numbers, this definition\nis mathematically valid.\n\nThis means that if you have a goal of the form `a ≤ b` you can\nmake progress with the `use` tactic, and if you have a hypothesis\n`h : a ≤ b`, you can make progress with `cases h with c hc`.":
  "`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。\n\n因为这个游戏没有负数，这个定义在数学上是有效的。\n\n这意味着如果你有一个形式为 `a ≤ b` 的目标，你可以用 `use` 策略来取得进展，如果你有一个假设 `h : a ≤ b`，你可以用 `cases h with c hc` 来取得进展。",
- "`a ≠ b` is *notation* for `(a = b) → False`.\n\nThe reason this is mathematically\nvalid is that if `P` is a true-false statement then `P → False`\nis the logical opposite of `P`. Indeed `True → False` is false,\nand `False → False` is true!\n\nThe upshot of this is that use can treat `a ≠ b` in exactly\nthe same way as you treat any implication `P → Q`. For example,\nif your *goal* is of the form `a ≠ b` then you can make progress\nwith `intro h`, and if you have a hypothesis `h` of the\nform `a ≠ b` then you can `apply h at h1` if `h1` is a proof\nof `a = b`.":
+ "`a ≠ b` is *notation* for `(a = b) → False`.\n\nThe reason this is mathematically\nvalid is that if `P` is a true-false statement then `P → False`\nis the logical opposite of `P`. Indeed `True → False` is false,\nand `False → False` is true!\n\nThe upshot of this is that you can treat `a ≠ b` in exactly\nthe same way as you treat any implication `P → Q`. For example,\nif your *goal* is of the form `a ≠ b` then you can make progress\nwith `intro h`, and if you have a hypothesis `h` of the\nform `a ≠ b` then you can `apply h at h1` if `h1` is a proof\nof `a = b`.":
  "`a ≠ b` 是由 `(a = b) → False` 定义的 。\n\n  这在数学上合法的原因是，如果 `P` 是一个真假命题，那么 `P → False`\n  与 `P` 的逻辑相反。确实 `True → False` 是假的，\n  `False → False` 是真的！\n\n  这样做的结果是我们可以用处理任何 `P → Q` 的方式处理 `a ≠ b`。例如，\n  如果 *目标* 的形式为 `a ≠ b` 那么您可以用 `intro h`取得进展；\n  如果你有一个假设 `h : a ≠ b` 那么你可以 `apply h at h1` 如果 `h1` 是\n  `a = b`的假设。",
  "`Pow a b`, with notation `a ^ b`, is the usual\n  exponentiation of natural numbers. Internally it is\n  defined via two axioms:\n\n  * `pow_zero a : a ^ 0 = 1`\n\n  * `pow_succ a b : a ^ succ b = a ^ b * a`\n\nNote in particular that `0 ^ 0 = 1`.":
  "`Pow a b`，其符号表示为 `a ^ b`，是自然数的常规指数运算。在内部，它是通过两个公理定义的：\n\n* `pow_zero a : a ^ 0 = 1`\n\n* `pow_succ a b : a ^ succ b = a ^ b * a`\n\n特别要注意的是 `0 ^ 0 = 1`。",
@@ -330,6 +330,8 @@
  "This world introduces exponentiation. If you want to define `37 ^ n`\nthen, as always, you will need to know what `37 ^ 0` is, and\nwhat `37 ^ (succ d)` is, given only `37 ^ d`.\n\nYou can probably guess the names of the general theorems:\n\n  * `pow_zero (a : ℕ) : a ^ 0 = 1`\n  * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n\nUsing only these, can you get past the final boss level?\n\nThe levels in this world were designed by Sian Carey, a UROP student\nat Imperial College London, funded by a Mary Lister McCammon Fellowship\nin the summer of 2019. Thanks to Sian and also thanks to Imperial\nCollege for funding her.":
  "这个世界引入了幂运算。如果你想定义 `37 ^ n`，那么像往常一样，你需要知道 `37 ^ 0` 是什么，以及在仅知 `37 ^ d` 的情况下，`37 ^ (succ d)` 是什么。\n\n你可能已经猜到了这些一般定理的名称：\n\n  * `pow_zero (a : ℕ) : a ^ 0 = 1`\n  * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n\n仅用这些定理，你能通过最后的boss关卡吗？\n\n这个世界中的关卡由帝国理工学院的 UROP 学生 Sian Carey 在 2019 年夏天设计，她的项目得到了 Mary Lister McCammon 奖学金的资助。感谢 Sian，也感谢帝国理工学院对她的资助。",
  "This time, use the `left` tactic.": "这一次，使用 `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 complare the two in the inventory.":
+ "",
  "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`.":
  "这个关卡要证明如果 `a ≠ 0` 且 `b ≠ 0`，那么 `a * b ≠ 0`。\n一种策略是将 `a` 和 `b` 都写成某物的 `succ`（后继），推断出 `a * b` 也是某物的 `succ`，然后应用 `zero_ne_succ`。",
  "This level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is\nlogically equivalent to the last level, so there is a very short proof.":
@@ -352,9 +354,9 @@
  "The previous lemma can be used to prove this one.": "先前的引理可以用来证明这个引理。",
  "The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\nLet's prove one of these facts in this level, and the other in the next.\n\n## A new tactic: `cases`\n\nThe `cases` tactic will split an object or hypothesis up into the possible ways\nthat it could have been created.\n\nFor example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\nbut don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\nIn this situation you can use `cases b with d` instead. There are two ways to make\na number: it's either zero or a successor. So you will end up with two goals, one\nwith `b = 0` and one with `b = succ d`.\n\nAnother example: if you have a hypothesis `h : False` then you are done, because a false statement implies\nany statement. Here `cases h` will close the goal, because there are *no* ways to\nmake a proof of `False`! So you will end up with no goals, meaning you have proved everything.":
  "在这一关中，让我们证明其中一个事实，而在下一关证明另一个。\n\n## 一种新的策略：`cases`\n\n`cases` 策略会将一个对象或假设分解为可能的创建方式。\n\n例如，有时你想分别处理 `b = 0` 和 `b = succ d` 这两种情况，但不需要与 `induction b with d hd` 一起来的归纳假设 `hd`。在这种情况下，你可以使用 `cases b with d`。制造一个数字有两种方式：它要么是零，要么是后继者。所以你最终会得到两个目标，一个是 `b = 0`，另一个是 `b = succ d`。\n\n另一个例子：如果你有一个假设 `h : False`，那么你就完成证明了，因为从 `False` 可以推出任何证明。这里 `cases h` 将证明目标，因为没有 *任何* 方法可以证明 `False`！所以你最终会没有目标，意味着你已经证明了一切。",
- "The music gets ever more dramatic, as we explore\nthe interplay between exponentiation and multiplication.\n\nIf you're having trouble exchanging the right `x * y`\nbecause `rw [mul_comm]` swaps the wrong multiplication,\nthen read the documentation of `rw` for tips on how to fix this.":
+ "The music gets ever more dramatic, as we explore\nthe interplay between exponentiation and multiplication.\n\nIf you're having trouble exchanging the right `a * b`\nbecause `rw [mul_comm]` swaps the wrong multiplication,\nthen read the documentation of `rw` for tips on how to fix this.":
  "当我们探索时，音乐变得更加戏剧化\n求幂和乘法之间的相互作用。\n\n如果您在更换正确的 `x * y` 时遇到问题\n因为 `rw [mul_comm]` 交换了错误的乘法，\n然后阅读 `rw` 的文档以获取有关如何解决此问题的提示。",
- "The music dies down. Is that it?\n\nCourse it isn't, you can\nclearly see that there are two worlds left.\n\nA passing mathematician says that mathematicians don't have a name\nfor the structure you just constructed. You feel cheated.\n\nSuddenly the music starts up again. This really is the final boss.":
+ "The music dies down. Is that it?\n\nCourse it isn't, you can\nclearly see that there are two levels left.\n\nA passing mathematician says that mathematicians don't have a name\nfor the structure you just constructed. You feel cheated.\n\nSuddenly the music starts up again. This really is the final boss.":
  "音乐渐渐平息。这就结束了吗？\n\n当然不是，你可以清楚地看到还有两个世界没有探索。\n\n一位路过的数学家说，你刚刚构建的结构只是个无名小卒。你感到有些被愚弄了。\n\n突然，音乐再次响起。这真的是最终的Boss。",
  "The lemma proved in the final level of this world will be helpful\nin Divisibility World.":
  "在这个世界的最后一个关卡证明的引理将在可除性世界中很有帮助。",
@@ -385,7 +387,7 @@
  "Start with `induction «{y}» with d hd`.": "从`induction «{y}» with d hd`开始。",
  "Start with `have h2 := mul_ne_zero a b`.":
  "从 `have h2 := mul_ne_zero a b` 开始。",
- "Start with `contrapose! h`, to change the goal into its\ncontrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`.":
+ "Start with `contrapose! h`, to change the goal into its\ncontrapositive, namely a hypothesis of `succ m = succ n` and a goal of `m = n`.":
  "从 `contrapose! h` 开始，将目标转变为其逆否命题，即假设为 `succ m = succ m`，目标为 `m = n`。",
  "Start with `cases «{hxy}» with a ha`.": "从 `cases «{hxy}» with a ha` 开始。",
  "Start with `cases a with d` to do a case split on `a = 0` and `a = succ d`.":
@@ -428,6 +430,8 @@
  "我们的第一个挑战是`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`.":
+ "在质数世界中，我们将证明 $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$。",
  "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). $":
@@ -468,14 +472,14 @@
  "现在 `«{ha}»` 是 `«{y}» = «{x}» + «{a}»`, 的证明，而 `hxy` 已经消失了。同样，你可以通过 `cases «{hyz}» with b hb` 将 `«{hyz}»` 分解。",
  "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`.":
  "现在 `rw [← two_eq_succ_one]` 会把 `succ 1` 改为 `2`。",
+ "Now `rw [«{h}»] at «{h2}»` so you can `apply le_one at «{h2}»`.":
+ "现在`rw [h] at h2`，这样就可以`apply le_one at hx`。",
  "Now `rw [h]` then `rfl` works, but `exact h` is quicker.":
  "现在 `rw [h]` 和 `rfl` 可以完成证明，但 `exact h` 更快。",
- "Now `rw [h] at h2` so you can `apply le_one at hx`.":
- "现在`rw [h] at h2`，这样就可以`apply le_one at hx`。",
  "Now `rw [add_zero]` will change `c + 0` into `c`.":
  "现在，`rw [add_zero]` 会把 `c + 0` 改为 `c`。",
  "Now `rfl` will work.": "现在可以用 `rfl` 了。",
- "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\nchange `succ x = succ y`.":
+ "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\nchange `h` to `succ x = succ y`.":
  "现在 `repeat rw [← succ_eq_add_one] at h` 是改写 `succ x = succ y` 的最快方法。",
  "Now `exact h` finishes the job.": "现在，用 `exact h ` 完成证明。",
  "Now `cases «{h2}» with e he`.": "现在使用 `cases «{h2}» with e he`。",
@@ -501,7 +505,7 @@
  "Natural Number Game": "自然数游戏",
  "My proof:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```":
  "我的证明：\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 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.":
+ "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 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$。",
@@ -542,7 +546,7 @@
  "对 `a` 或 `b` 进行归纳证明 —— 它们都是相同的。",
  "Induction on `a` is the most troublesome, then `b`,\nand `c` is the easiest.":
  "对 `a` 的归纳最麻烦，然后是 `b`、\n而 `c` 是最简单的。",
- "In this world we'll learn how to prove theorems of the form $P\\implies Q$.\nIn other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\nTo do that we need to learn some more tactics.\n\nThe `exact` tactic can be used to close a goal which is exactly one of\nthe hypotheses.":
+ "In this world we'll learn how to prove theorems of the form $P\\implies Q$.\nIn other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\nTo do that we need to learn some more tactics.\n\nThe `exact` tactic can be used to close a goal which is exactly one of\nthe hypotheses. It takes the name of the hypothesis as argument: `exact h`.":
  "在这个世界中，我们将学习如何证明形式为 $P\\implies Q$ 的定理。\n换句话说，就是如何证明“如果 $P$ 为真，则 $Q$ 也为真”的形式的定理。\n为此，我们需要学习一些更多的策略。\n\n`exact` 策略可以用来解决一个存在于假设中的目标。",
  "In this world we define `a ≤ b` and prove standard facts\nabout it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"\n\nThe definition of `a ≤ b` is \"there exists a number `c`\nsuch that `b = a + c`. \" So we're going to have to learn\na tactic to prove \"exists\" theorems, and another one\nto use \"exists\" hypotheses.\n\nClick on \"Start\" to proceed.":
  "在这个世界中，我们定义 `a ≤ b` 并证明关于它的一些事实，例如“如果 `a ≤ b` 且 `b ≤ c` 那么 `a ≤ c`。”\n\n`a ≤ b` 的定义是“存在一个数字 `c` 使得 `b = a + c`。”所以我们将不得不学习一种策略来证明“存在”定理，以及另一种策略来使用“存在”假设。\n\n点击“开始”继续。",
@@ -550,14 +554,14 @@
  "在这个世界中，探险将主要由您独自完成。\n\n`add_right_cancel a b n` 是定理 $a+n=b+n\\implies a=b$。",
  "In this level, we see inequalities as *hypotheses*. We have not seen this before.\nThe `cases` tactic can be used to take `hxy` apart.":
  "在本关，我们将不等视为 *假设* 。我们以前没有见过这个。\n`cases` 策略可用于拆解 `hxy` 假设。",
+ "In this level, the hypotheses `h2` is an *implication*. It says\nthat *if* `x = 37` *then* `y = 42`. We can use this\nhypothesis with the `apply` tactic. Remember you can click on\n`apply` or any other tactic on the right to see a detailed explanation\nof what it does, with examples.":
+ "",
  "In this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n\nWait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\nThis is `zero_add`, which is different.\n\nThe difficulty with proving `0 + n = n` is that we do not have a *formula* for\n`0 + n` in general, we can only use `add_zero` and `add_succ` once\nwe know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n\nThe base case will require us to prove `0 + 0 = 0`, and the inductive step\nwill ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because\n`0` and successor are the only way to make numbers, this will cover all the cases.\n\nSee if you can do your first induction proof in Lean.\n\n(By the way, if you are still in the \"Editor mode\" from the last world, you can swap\nback to \"Typewriter mode\" by clicking the `>_` button in the top right.)":
  "在这个关卡中，我们将证明 $0+n=n$，其中 $n$ 是一个未知的自然数。\n\n等等，我们不是已经知道这个了吗？不！我们知道的是 $n+0=n$，但那是 `add_zero`。这里的 `zero_add` 是不同的。\n\n证明 `0 + n = n` 的难点在于我们没有一个一般的*公式*来表示 `0 + n`，我们只能在知道 `n` 是 `0` 还是后继数后，使用 `add_zero` 和 `add_succ`。`induction` （归纳）策略会把目标分解成这两种情况。\n\n基础情况将要求我们证明 `0 + 0 = 0`，归纳步骤将要求我们证明如果 `0 + d = d` 那么 `0 + succ d = succ d`。因为 `0` 和后继数是构造数字的唯一方式，这将涵盖所有情况。\n\n看看你是否能在 Lean 中完成你的第一个归纳证明。\n\n(顺便说一句，如果你还在上一个世界的 \"编辑器模式 \"下，你可以通过点击 \"编辑器模式 \"下的\n点击右上角的 `>_` 按钮换回 \"模式\"）。",
- "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\nseveral reasons. One of these is that\nwe need to introduce a new idea: we will need to understand the concept of\nmathematical induction a little better.\n\nStarting with `induction b with d hd` is too naive, because in the inductive step\nthe hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\nso the induction hypothesis does not apply!\n\nAssume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,\nbecause we now have the flexibility to change `c`.\"":
+ "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\nseveral reasons. One of these is that\nwe need to introduce a new idea: we will need to understand the concept of\nmathematical induction a little better.\n\nStarting with `induction b with d hd` is too naive, because in the inductive step\nthe hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\nso the induction hypothesis does not apply!\n\nAssume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n\"for all `c`, if `a * b = a * c` then `b = c`\". This *can* be proved by induction,\nbecause we now have the flexibility to change `c`.":
  "在这个关卡中，我们证明了如果 `a * b = a * c` 且 `a ≠ 0` 那么 `b = c`。这是有些难的，因为几个原因。其中之一是我们需要引入一个新的想法：我们需要更好地理解数学归纳法的概念。\n\n从 `induction b with d hd` 开始太天真了，因为在归纳步骤中，假设是 `a * d = a * c → d = c`，但我们所知的是 `a * succ d = a * c`，所以归纳假设不适用！\n\n现在假设 `a ≠ 0` 是固定的。我们想要通过对 `b` 进行归纳来证明“对于所有的 `c`，如果 `a * b = a * c` 那么 `b = c`。这*可以*通过归纳来证明，因为我们现在有了改变 `c` 的灵活性。”",
  "In this level the *goal* is $2y=2(x+7)$ but to help us we\nhave an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\nyour list of assumptions. Lean thinks of `h` as being a secret proof of the\nassumption, rather like `x` is a secret number.\n\nBefore we can use `rfl`, we have to \"substitute in for $y$\".\nWe do this in Lean by *rewriting* the proof `h`,\nusing the `rw` tactic.":
  "在这个关卡里，*目标*是证明 $2y=2(x+7)$。现在我们有一条*假设* `h`，它指出 $y = x + 7$。请检查假设列表中是否包含了 `h`。在 Lean 中，`h` 被视为一种假设存在的证据，这有点像 `x` 是一个未知的具体数值。\n\n要想使用 `rfl` 完成证明，我们首先需要对 $y$ 进行替换。在 Lean 中，我们可以通过*重写*证明 `h` 来实现这一点，即使用 `rw` 策略。",
- "In this level one of our hypotheses is an *implication*. We can use this\nhypothesis with the `apply` tactic.":
- "在这个关卡中，我们的一个假设是一个*蕴含式*。我们可以使用 `apply` 策略来利用这个假设。",
  "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\nlearning the basics about theorem proving in Lean.\n\nThis is a good first introduction to Lean!":
  "在这个游戏中，你将根据皮亚诺公理重新构建自然数集 $\\mathbb{N}$，学习在 Lean 中证明定理的基础知识。\n\n这是对 Lean 的一个很好的初步介绍！",
  "In the next level, we'll do the same proof but backwards.":
@@ -570,8 +574,6 @@
  "在一些后续的世界中，我们将看到一些更棘手的关卡，比如 `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`。需要移动括号，还需要交换变量。\n\n在这个关卡中，`(a + b) + (c + d) = ((a + c) + d) + b`，让我们忘掉括号，只考虑变量的顺序。\n要将 `a+b+c+d` 转换成 `a+c+d+b`，我们需要交换 `b` 和 `c`，然后交换 `b` 和 `d`。但是使用 `add_left_comm` 比你想象的要简单。",
  "In order to use the tactic `rfl` you can enter it in the text box\nunder the goal and hit \"Execute\".":
  "要使用策略 \"rfl\"，您可以在目标下的文本框中输入它，然后点击 \"执行\"。",
- "In Prime Number World we will be 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 pretty much everything which we've proved in this world so far.":
- "在质数世界中，我们将证明 $2$ 是质数。为此，我们必须排除像 $2 ≠ 37 × 42$ 这样的情况。\n我们将通过证明 $2$ 的任何因数最多是 $2$ 来做到这一点，我们将使用这个引理来实现。\n我脑海中的证明会操作假设，直到它变成目标，几乎使用我们到目前为止在这个世界中已经证明的所有内容。",
  "In Advanced Addition World we will prove some basic\naddition facts such as $x+y=x\\implies y=0$. The theorems\nproved in this world will be used to build\na theory of inequalities in `≤` World.\n\nClick on \"Start\" to proceed.":
  "在高级加法世界中，我们将证明一些基本的加法事实，如 $x+y=x\\implies y=0$。在这个世界中证明的定理将被用来在 `≤` 世界中构建不等式理论。\n\n点击“开始”继续。",
  "Implication World": "蕴含世界",
@@ -637,6 +639,8 @@
  "这个证明怎么样：\n\n```\nrw [add_comm]\nexact add_right_eq_zero b a\n```\n\n这里就是高级加法世界的结尾了！你将带着这些定理\n进入下一个世界，`≤` 世界。点击“离开世界”来访问它。",
  "Here's what I was thinking of:\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```":
  "我是这么想的：\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```",
+ "Here's the short proof:\n```\nhave h2 := mul_ne_zero a b\ntauto\n```\nThis works because, given `mul_ne_zero a b`,\nthe argument is reduced to pure logic.":
+ "",
  "Here's my solution:\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```":
  "这是我的解法：\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```",
  "Here's my solution:\n```\nrw [mul_comm, mul_one]\nrfl\n```":
@@ -657,7 +661,7 @@
  "这是两行的证明：\n```\nuse 1\nexact succ_eq_add_one x\n```\n\n这是有效的，因为 `succ_eq_add_one x` 是 `succ x = x + 1` 的证明。",
  "Here's a two-line proof:\n```\nrepeat rw [zero_add] at h\nexact h\n```":
  "这是一个两行证明：\n```\nrepeat rw [zero_add] at h\nexact h\n```",
- "Here's a proof using `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\nand here's an even shorter one using the same idea:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nAlternatively you can just prove it by induction on `x`\n(the dots in the proof just indicate the two goals and\ncan be omitted):\n\n```\n  induction x with d hd\n  · intro h\n    rw [zero_add] at h\n    assumption\n  · intro h\n    rw [succ_add] at h\n    apply succ_inj at h\n    apply hd at h\n    assumption\n```":
+ "Here's a proof using `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\nand here's an even shorter one using the same idea:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nAlternatively you can just prove it by induction on `x`:\n\n```\ninduction x with d hd\nintro h\nrw [zero_add] at h\nexact h\nintro h\nrw [succ_add] at h\napply succ_inj at h\napply hd at h\nexact h\n```":
  "这里是使用 `add_left_eq_self` 的一个证明：\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\n这里是一个使用相同思路的更短的证明：\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\n或者，你也可以通过对 `x` 进行归纳来证明它\n（证明中的 `.` 只是表示两个目标，\n可以省略）：\n\n```\n  induction x with d hd\n  · intro h\n    rw [zero_add] at h\n    assumption\n  · intro h\n    rw [succ_add] at h\n    apply succ_inj at h\n    apply hd at h\n    assumption\n```",
  "Here's a completely backwards proof:\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```":
  "这是一个完全逆向的证明过程：\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```",
@@ -715,7 +719,7 @@
  "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```":
  "你是否对 `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.":
+ "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World (when someone gets around to\nimplementing it).":
  "恭喜！您已经完成了《算法世界》。这些算法\n将对您在奇偶世界中有所帮助。",
  "Congratulations! You have proved Fermat's Last Theorem!\n\nEither that, or you used magic...":
  "恭喜！您已经证明了费马大定理！\n\n要么就是，要么你使用了魔法……",
@@ -771,7 +775,7 @@
  "2 + 2 ≠ 5": "2 + 2 ≠ 5",
  "1 ≠ 0": "1 ≠ 0",
  "0 ≤ x": "0 ≤ x",
- "*Game version: 4.2*\n\n*Recent additions: Inequality world, algorithm world*\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.":
+ "*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$.",
@@ -797,7 +801,7 @@
  "## 小结\n\n`repeat t` 反复应用策略 `t` 到目标上。这个是个可选策略，它只是有时可以节省步骤。\n\n## 示例\n\n`repeat rw [add_zero]` 会将目标\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\n变为\n`a = b`。",
  "## Summary\n\n`repeat t` repeatedly applies the tactic `t`\nto the goal. You don't need to use this\ntactic, it just speeds things up sometimes.\n\n## Example\n\n`repeat rw [add_zero]` will turn the goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\ninto the goal\n`a = b`.":
  "## 小结\n\n`repeat t` 会重复应用策略 `t` 到目标上。你不一定要使用这个策略，它有时只是加快了速度。\n\n## 示例\n\n`repeat rw [add_zero]` 会将目标 `a + 0 + (0 + (0 + 0)) = b + 0 + 0` 转变为目标 `a = b`。",
- "## Summary\n\nThe `use` tactic makes progress with goals which claim something *exists*.\nIf the goal claims that some `x` exists with some property, and you know\nthat `x = 37` will work, then `use 37` will make progress.\n\nBecause `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\nyou can make progress on goals of the form `a ≤ b` by `use`ing the\nnumber which is morally `b - a`.":
+ "## Summary\n\nThe `use` tactic makes progress with goals which claim something *exists*.\nIf the goal claims that some `x` exists with some property, and you know\nthat `x = 37` will work, then `use 37` will make progress.\n\nBecause `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\nyou can make progress on goals of the form `a ≤ b` by `use`ing the\nnumber which is morally `b - a` (i.e. `use b - a`)\n\nAny of the following examples is possible assuming the type of the argument passed to the `use` function is accurate:\n\n- `use 37`\n- `use a`\n- `use a * a + 1`":
  "## 概述\n\n`use` 策略能用在声称某些东西 *存在* 的目标上。\n如果目标声称某些 `x` 存在并具有某些属性，并且您知道\n`x = 37` 将起作用，那么使用 `use 37` 来改写目标。\n\n因为 `a ≤ b` 是用 “存在 `c` 使得 `b = a + c`” 定义的，\n所以可以通过`use (b - a)` 在 `a ≤ b` 形式的目标上取得进展。",
  "## Summary\n\nThe `symm` tactic will change a goal or hypothesis of\nthe form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\nand on `X ↔ Y`.\n\n### Example\n\nIf the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n\n### Example\n\nIf `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`.":
  "## 小结\n\n`symm` 策略会将形如 `X = Y` 的目标或假设转换为 `Y = X`。它也适用于 `X ≠ Y` 和 `X ↔ Y`。\n\n### 例子\n\n如果目标是 `2 + 2 = 4`，那么 `symm` 会将其转换为 `4 = 2 + 2`。\n\n### 例子\n\n如果 `h : 2 + 2 ≠ 5`，那么 `symm at h` 会将 `h` 转换为 `5 ≠ 2 + 2`。",
@@ -811,13 +815,13 @@
  "## 概述\n\n如果 `n` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n = 0`，另一个是 `n = succ d`。\n\n如果 `h` 是一个证明（例如一个假设），那么 `cases h with...` 会将证明分解成用来证明它的各个部分。\n\n## 示例\n\n如果 `n : ℕ` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n` 被替换为 0，另一个是 `n` 被替换为 `succ d`。这对应于数学上的观点，即每个自然数要么是 `0`，要么是一个后继数。\n\n## 示例\n\n如果 `h : P ∨ Q` 是一个假设，那么 `cases h with hp hq` 会将一个目标变成两个目标，一个有假设 `hp : P`，另一个有假设 `hq : Q`。\n\n## 示例\n\n如果 `h : False` 是一个假设，那么 `cases h` 会将一个目标变成没有目标，因为没有方法可以证明 `False`！如果你没有剩余的目标，你就完成了这个关卡。\n\n## 示例\n\n如果 `h : a ≤ b` 是一个假设，那么 `cases h with c hc` 会创建一个新的数字 `c` 和一个证明 `hc : b = a + c`。这是因为 `a ≤ b` 的*定义*是 `∃ c, b = a + c`。",
  "## Summary\n\nIf `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\nattempts to prove the goal by induction on `n`, with the inductive\nvariable in the successor case being `d`, and the inductive hypothesis being `hd`.\n\n### Example:\nIf the goal is\n```\n0 + n = n\n```\n\nthen\n\n`induction n with d hd`\n\nwill turn it into two goals. The first is `0 + 0 = 0`;\nthe second has an assumption `hd : 0 + d = d` and goal\n`0 + succ d = succ d`.\n\nNote that you must prove the first\ngoal before you can access the second one.":
  "## 概述\n\n如果 `n : ℕ` 是一个对象，并且目标提到了 `n`，那么 `induction n with d hd`\n尝试通过对 `n` 进行归纳来证明目标，其中后继数情况下的归纳变量是 `d`，归纳假设是 `hd`。\n\n### 例子:\n如果目标是\n```\n0 + n = n\n```\n\n那么\n\n`induction n with d hd`\n\n将把它变成两个目标。第一个是 `0 + 0 = 0`；\n第二个有一个假设 `hd : 0 + d = d` 和目标\n`0 + succ d = succ d` 。\n\n注意你必须先证明第一个然后才能证第二个。",
- "## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`'s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.":
+ "## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.":
  "## 概述\n\n如果 `h` 是一个等式 `X = Y` 的证明，那么 `rw [h]` 将会把目标中所有的 `X` 改为 `Y`。这是一种“代入”的方式。\n\n## 变体\n\n* `rw [← h]`（将 `Y` 改为 `X`；通过输入 `\\left ` 或 `\\l` 获取反向箭头。）\n\n* `rw [h1, h2]`（一系列重写）\n\n* `rw [h] at h2`（在假设 `h2` 中将 `X` 改为 `Y`）\n\n* `rw [h] at h1 h2 ⊢`（在两个假设和目标中将 `X` 改为 `Y`；通过输入 `\\|-` 获取 `⊢` 符号。）\n\n* `repeat rw [add_zero]` 将会不断地把 `? + 0` 改为 `?`，直到没有更多的 `? + 0` 匹配为止。\n\n* `nth_rewrite 2 [h]` 只会把目标中的第二个 `X` 改为 `Y`。\n\n### 示例：\n\n如果你有假设 `h : x = y + y` 并且你的目标是\n```\nsucc (x + 0) = succ (y + y)\n```\n\n那么\n\n`rw [add_zero]`\n\n将会把目标改为 `succ x = succ (y + y)`，然后\n\n`rw [h]`\n\n将会把目标改为 `succ (y + y) = succ (y + y)`，这个可以通过 `rfl` 解决。\n\n### 示例：\n\n你也可以使用 `rw` 来改变一个假设。例如，如果你有两个假设\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\n那么 `rw [h1] at h2` 将会把 `h2` 变为 `h2 : 2 * y = y + 3`。\n\n## 常见错误\n\n* 你需要方括号。`rw h` 是不正确的。\n\n* 如果 `h` 不是一个*等式*的*证明*（形式为 `A = B` 的声明），例如如果 `h` 是一个函数或蕴含，那么 `rw` 不是你想要使用的策略。例如，`rw [P = Q]` 永远不正确， 因为`P = Q` 是定理的*陈述*，而不是证明。但如果 `h : P = Q` 是证明，那么 `rw [h]` 将会起作用。\n\n## 详情\n\n`rw` 策略是一种进行“代入”的方式。有两种不同的情况你可以使用这个策略。\n\n1) 基本使用：如果 `h : A = B` 是一个假设或定理的证明，并且目标中包含一个或多个 `A`，那么 `rw [h]` 会把它们全部改为 `B`。如果目标中没有 `A`，策略会报错。\n\n2) 高级使用：来自定理证明的假设经常有缺失的部分。例如 `add_zero` 是一个证明，表示 `? + 0 = ?`，因为 `add_zero` 实际上是一个函数，而 `?` 是输入。在这种情况下，`rw` 会在目标中查找任何形式为 `x + 0` 的子项，一旦找到，它就将 `?` 定位为 `x`，然后把所有的 `x + 0` 改为 `x`。\n\n练习：思考为什么 `rw [add_zero]` 会把项 `(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为 `0 + (x + 0) + 0 + (x + 0)`\n\n如果你不能记住等式证明的名称，请在右侧的定理列表中查找。\n\n## 针对性使用\n\n如果你的目标是 `b + c + a = b + (a + c)` 并且你想把 `a + c` 重写为 `c + a`，那么 `rw [add_comm]` 将不起作用，因为 Lean 会先找到另一个加法并交换它。使用 `rw [add_comm a c]` 来保证 Lean 将 `a + c` 重写为 `c + a`。这是因为 `add_comm` 是一个证明，表示 `?1 + ?2 = ?2 + ?1`，`add_comm a` 是一个证明，表示 `a + ? = ? + a`，而 `add_comm a c` 是另一个证明，表示 `a + c = c + a`。\n\n如果 `h : X = Y`，那么 `rw [h]` 将会把所有的 `X` 变为 `Y`。如果你只想改变第37次出现的 `X` 为 `Y`，那么可以使用 `nth_rewrite 37 [h]`。",
  "## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.":
  "## 小结\n\n如果 `h : X = Y` 并且在目标中有多个 `X`，那么 `nth_rewrite 3 [h]` 将仅更改第三个 `X` 为 `Y`。\n\n## 示例\n\n如果目标是 `2 + 2 = 4`，那么 `nth_rewrite 2 [two_eq_succ_one]` 将目标更改为 `2 + succ 1 = 4`。相比之下，`rw [two_eq_succ_one]` 将目标更改为 `succ 1 + succ 1 = 4`。",
  "## Precision rewriting\n\nIn the last level, there was `b + 0` and `c + 0`,\nand `rw [add_zero]` changed the first one it saw,\nwhich was `b + 0`. Let's learn how to tell Lean\nto change `c + 0` first by giving `add_zero` an\nexplicit input.":
  "## 精准重写\n\n在上一个关卡中，有 `b + 0` 和 `c + 0`，\n而 `rw [add_zero]` 改变了它看到的第一个加0，\n也就是 `b + 0`。让我们学习如何告诉 Lean\n通过给 `add_zero` 一个明确的输入来首先改变 `c + 0`。",
- "# Welcome to the Natural Number Game\n#### An introduction to mathematical proof.\n\nIn this game, we will build the basic theory of the natural\nnumbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\nthat `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\nAnd at the end we'll see if we can prove Fermat's Last Theorem.\nWe'll do this by solving levels of a computer puzzle game called Lean.\n\n# Read this.\n\nLearning how to use an interactive theorem prover takes time.\nTests show that the people who get the most out of this game are\nthose who read the help texts like this one.\n\nTo start, click on \"Tutorial World\".\n\nNote: this is a new Lean 4 version of the game containing several\nworlds which were not present in the old Lean 3 version. A new version\nof Advanced Multiplication World is in preparation, and worlds\nsuch as Prime Number World and more will be appearing during October and\nNovember 2023.\n\n## More\n\nClick on the three lines in the top right and select \"Game Info\" for resources,\nlinks, and ways to interact with the Lean community.":
+ "# Welcome to the Natural Number Game\n#### An introduction to mathematical proof.\n\nIn this game, we will build the basic theory of the natural\nnumbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\nthat `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\nAnd at the end we'll see if we can prove Fermat's Last Theorem.\nWe'll do this by solving levels of a computer puzzle game called Lean.\n\n# Read this.\n\nLearning how to use an interactive theorem prover takes time.\nTests show that the people who get the most out of this game are\nthose who read the help texts like this one.\n\nTo start, click on \"Tutorial World\".\n\nNote: this is a new Lean 4 version of the game containing several\nworlds which were not present in the old Lean 3 version. More new worlds\nsuch as Strong Induction World, Even/Odd World and Prime Number World\nare in development; if you want to see their state or even help out, checkout\nout the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues).\n\n## More\n\nClick on the three lines in the top right and select \"Game Info\" for resources,\nlinks, and ways to interact with the Lean community.":
  "# 欢迎进入自然数游戏\n### 数学证明的启蒙。\n\n本游戏将带领我们从头开始构建自然数 `{0,1,2,3,4,...}` 的基础理论体系。我们首先要证明的是 `2 + 2 = 4`。紧接着，我们会证明 `x + y = y + x`。\n最终，我们将尝试证明费马大定理。\n请通过完成本游戏中的关卡来完成这些挑战。\n\n## 阅读提示\n\n掌握交互式定理证明工具需要花费时间。\n经过测试发现，那些阅读了本帮助指南的玩家能够更好地享受本游戏并从中受益。\n\n开始游戏，请点击“教程世界”。\n\n请注意：这是基于全新 Lean 4 开发的游戏版本，新增了许多旧版 Lean 3 中未包含的世界。高级乘法世界的新版本正在开发中，其他新世界如素数世界等将于2023年10月至11月陆续推出。\n\n## 更多信息\n\n请点击屏幕右上角的“☰”，选择“游戏信息”，这里提供了资源链接以及如何与 Lean 社区互动的方法。",
  "# Summary\nThe `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `Q` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $Q \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.":
  "## 概述\n`right` 策略将 `P ∨ Q` 的目标更改为 `Q` 的目标。\n当您的假设`Q` 为真是 `P ∨ Q`为真的原因时使用它。\n\n在策略内部，它只是 `apply` （应用） 了 $Q \\implies P \\lor Q$ 这个定理\n\n请注意，这种策略可以将可解决的目标变成无法解决的目标。",
@@ -827,9 +831,9 @@
  "## 概述\n\n`trivial` 将解决目标 `True`。",
  "# Summary\n\n`decide` will attempt to solve a goal if it can find an algorithm which it\ncan run to solve it.\n\n## Example\n\nA term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\nare equal or different. Hence, once this term is made and made into an `instance`,\nthe `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.":
  "## 概述\n\n如果 `decide` 可以找到一种算法来解决目标，它将尝试解决该目标。\n\n### 示例\n\n类型为 `DecidableEq ℕ` 的项是用于判断两个自然数是否相等或不同的算法（的实现函数）。\n因此，一旦这个项被创建并成为一个 `instance`，`decide` 策略就可以使用它来解决形式为 `a = b` 或 `a ≠ b` 的目标。",
- "# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n\n## Example\n\nIf you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.":
+ "# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Details\n\n`tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication,\nit doesn't even know `add_zero`. The only things that `tauto` knows about numbers\nare firstly that `a = a` and secondly that `0 ≠ 1`, `0 ≠ 2`, `1 ≠ 2` and so on.\nWhat `tauto`'s strength is, is *logic*. If you have a hypothesis `x < 37`\nand another hypothesis `x < 37 → y + z = 42` and your goal is `y + z = 42` then `tauto` will\nsolve this goal, because to solve that goal you don't need to know any facts\nabout inequalities or addition, all you need to know is the rules of logic.\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n\n## Example\n\nIf you have a hypothesis `h : 0 = 1` then `tauto` will solve the goal, because\n`tauto` knows `0 ≠ 1` and this is enough to prove `False`, which implies any goal.\n\n## Example\n\nIf you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.":
  "## 概述\n\n`tauto` 策略将解决任何只靠命题逻辑就可以解决的目标（即，通过真值表）。\n\n### 示例\n\n如果你有一个假设为 `False`，那么 `tauto` 将解决目标。这是因为一个假的假设意味着任何假设。\n\n### 示例\n\n如果你的目标是 `True`，那么 `tauto` 将解决目标。\n\n### 示例\n\n如果你有两个假设 `h1 : a = 37` 和 `h2 : a ≠ 37`，那么 `tauto` 将解决目标，因为它可以从你的假设中证明 `False`，从而证明目标（因为 `False` 意味着任何事情）。\n\n### 示例\n\n如果你有一个假设 `h : a ≠ a`，那么 `tauto` 将解决目标，因为 `tauto` 足够聪明以知道 `a = a` 是真的，这提供了我们寻求的矛盾。\n\n### 示例\n\n如果你有一个形式为 `a = 0 → a * b = 0` 的假设，而你的目标是 `a * b ≠ 0 → a ≠ 0`，那么 `tauto` 将解决目标，因为目标在逻辑上等同于假设。\n如果你在这个示例中交换目标和假设，`tauto` 也会解决它。\n如果你有两个假设 `h1 : a = 37` 和 `h2 : a ≠ 37` 那么 `tauto` 将解决目标\n就能解决这个目标，因为它能从你的假设中证明 `False`，从而\n证明目标（因为 `False` 意味着任何事情）。\n\n### 示例\n\n如果你有一个假设 `h : a ≠ a` 那么 `tauto` 就能证明这个目标，因为\n`tauto` 足够聪明，知道 `a = a` 为真，这就给出了我们所寻求的矛盾。\n\n### 示例\n\n如果你有一个形式为 `a = 0 → a * b = 0` 的假设，而你的目标是 `a * b ≠ 0 → a ≠ 0`，那么\n`tauto` 将证明目标，因为目标在逻辑上等同于假设。\n如果把这个例子中的目标和假设换一下，`tauto` 也会解决它。",
- "# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.":
+ "# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. For example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.":
  "# 小结\n\n`have` 策略可以用来向一个关卡添加新的假设，但当然，你必须证明它们。\n\n## 示例\n\n最简单的使用方式是这样的。如果你在你的上下文中有 `a` 并且你执行了\n\n`have ha : a = 0`\n\n那么你将得到一个新的目标 `a = 0` 来证明，一旦你证明了它，你将在你原始的目标中有一个新的假设 `ha : a = 0`。\n\n## 示例\n\n如果你已经有了你想要 `have` 的证明，你可以立即创建它。例如，如果你有 `a` 和 `b` 这两个数字对象，那么\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\n将直接向上下文中添加一个新的假设 `h2 : succ a = succ b → a = b`，因为你刚刚提供了它的证明（`succ_inj a b`）。\n\n## 示例\n\n如果你手头有证明，那么你甚至不需要声明你在证明什么。例如\n\n`have h2 := succ_inj a b`\n\n将会添加假设 `h2 : succ a = succ b → a = b`。",
  "# Summary\n\nIf you have a hypothesis\n\n`h : a ≠ b`\n\nand goal\n\n`c ≠ d`\n\nthen `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\na hypothesis\n\n`h : c = d`\n\nand goal\n\n`a = b`.":
  "## 概述\n\n如果你有一个假设\n\n`h : a ≠ b`\n\n和目标\n\n`c ≠ d`\n\n那么 `contrapose! h` 将这个命题替换为所谓的“逆否命题”：\n一个假设\n\n`h : c = d`\n\n和目标\n\n`a = b`。",