Update translation files

.i18n/fr/Game.po

@@ -1263,10 +1263,10 @@ msgstr ""
 "sur n'importe quel `succ` dans le but ou les hypothèses pour voir exactement ce qu'il prend."
 
 #: Game.Levels.Addition.L02succ_add
-msgid "Well done! You now have enough tools to tackle the main boss of this level."
+msgid "Well done! You now have enough tools to tackle the main boss of this world."
 msgstr ""
 "Bien joué ! Vous avez maintenant suffisamment d'outils pour affronter le boss principal de ce "
-"niveau."
+"monde."
 
 #: Game.Levels.Addition.L03add_comm
 msgid "add_comm (level boss)"
@@ -1822,11 +1822,11 @@ msgstr "`add_mul a b c` est une preuve que $(a+b)c=ac+bc$."
 
 #: Game.Levels.Multiplication.L08add_mul
 msgid ""
-"Addition is distributive over multiplication.\n"
+"Multiplication is distributive over addition.\n"
 "In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
 "$(a + b) \\times c = ac + bc$."
 msgstr ""
-"L'addition est distributive sur la multiplication.\n"
+"La multiplication est distributive sur l'addition.\n"
 "Autrement dit, pour tous les nombres naturels $a$, $b$ et $c$, nous avons\n"
 "$(a + b) \\times c = ac + bc$."
 
@@ -2448,7 +2448,7 @@ msgid ""
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n"
-"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+"`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "Faites-le encore !\n"
 "\n"
@@ -2703,7 +2703,7 @@ msgid ""
 "  the goal until it becomes our hypothesis! In other words, we\n"
 "  will \"argue backwards\". The `apply` tactic can do this too.\n"
 "  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+"  \"Typewriter mode\")."
 msgstr ""
 "Dans le dernier niveau, nous avons manipulé l'hypothèse `x + 1 = 4`\n"
 "  jusqu'à ce qu'elle devienne le but `x = 3`. Dans ce niveau, nous manipulerons\n"
@@ -2784,8 +2784,8 @@ msgstr ""
 msgid ""
 "We have seen how to `apply` theorems and assumptions\n"
 "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
-"To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\n"
-"in Lean. We do this with the `intro` tactic."
+"To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".\n"
+"In Lean, we do this with the `intro` tactic."
 msgstr ""
 "Nous avons vu comment utiliser `apply` sur des théorèmes et des hypothèses\n"
 "de la forme `P → Q`. Mais que faire si notre *but* est de la forme `P → Q` ?\n"
@@ -3841,11 +3841,11 @@ msgstr "$x + y = y\\implies x=0.$"
 msgid ""
 "Did you use induction on `y`?\n"
 "Here's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\n"
-"If you want to inspect it, you can go into editor mode by clicking `</>` in the top right\n"
+"If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in the top right\n"
 "and then just cut and paste the proof and move your cursor around it\n"
 "to see the hypotheses and goal at any given point\n"
 "(although you'll lose your own proof this way). Click `>_` to get\n"
-"back to command line mode.\n"
+"back to \"Typewriter mode\".\n"
 "```\n"
 "nth_rewrite 2 [← zero_add y]\n"
 "exact add_right_cancel x 0 y\n"
@@ -5042,7 +5042,7 @@ msgstr ""
 msgid ""
 "One day this game will have a Prime Number World, with a final boss\n"
 "of proving that $2$ is prime.\n"
-"To do this, we will have to rule out things like $2 = 37 × 42.$\n"
+"To do this, we will have to rule out things like $2 = 37 × 42$.\n"
 "We will do this by proving that any factor of $2$ is at most $2$,\n"
 "which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n"
 "until it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n"

.i18n/it/Game.po

@@ -548,7 +548,7 @@ msgstr ""
 msgid ""
 "One day this game will have a Prime Number World, with a final boss\n"
 "of proving that $2$ is prime.\n"
-"To do this, we will have to rule out things like $2 = 37 × 42.$\n"
+"To do this, we will have to rule out things like $2 = 37 × 42$.\n"
 "We will do this by proving that any factor of $2$ is at most $2$,\n"
 "which we will do using this lemma. The proof I have in mind manipulates the "
 "hypothesis\n"
@@ -558,7 +558,7 @@ msgid ""
 msgstr ""
 "Un giorno questo gioco avrà il Mondo Numeri Primi, il cui boss finale\n"
 "sarà dimostrare che $2$ è un numero primo.\n"
-"Ma per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42.$\n"
+"Ma per arrivarci, dobbiamo escludere falsità del tipo $2 ≠ 37 × 42$.\n"
 "Lo faremo dimostrando che ogni fattore di $2$ è al più $2$,\n"
 "che avremo gratis grazie a questo lemma. La dimostrazione che ho in mente io "
 "manipola l'ipotesi finché\n"
@@ -815,7 +815,7 @@ msgid ""
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all "
 "occurrences of\n"
-"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
+"`0 + «{x}»` it finds. Therefore, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "Ripeti lo stesso comando!\n"
 "\n"
@@ -1122,11 +1122,11 @@ msgstr "`mul_zero m` è la dimostrazione di `m * 0 = 0`."
 
 #: Game.Levels.Multiplication.L08add_mul
 msgid ""
-"Addition is distributive over multiplication.\n"
+"Multiplication is distributive over addition.\n"
 "In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
 "$(a + b) \\times c = ac + bc$."
 msgstr ""
-"L'addizione gode della proprietà distributiva sulla moltiplicazione.\n"
+"La moltiplicazione gode della proprietà distributiva sull'addizione.\n"
 "Equivalentemente, per tutti i numeri naturali $a$, $b$ e $c$, si ha che\n"
 "$(a + b) \\times c = ac + bc$."
 
@@ -4400,7 +4400,7 @@ msgid ""
 "  the goal until it becomes our hypothesis! In other words, we\n"
 "  will \"argue backwards\". The `apply` tactic can do this too.\n"
 "  Again I will walk you through this one (assuming you're in\n"
-"  command line mode)."
+"  \"Typewriter mode\")."
 msgstr ""
 "Nell'ultimo livello abbiamo manipolato l'ipotesi `x + 1 = 4`\n"
 "  per farla coincidere con il goal `x = 3`. In questo livello manipoleremo\n"
@@ -4893,8 +4893,8 @@ msgid ""
 "We have seen how to `apply` theorems and assumptions\n"
 "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n"
 "To prove this goal, we need to know how to say \"let's assume `P` and deduce "
-"`Q`\"\n"
-"in Lean. We do this with the `intro` tactic."
+"`Q`\".\n"
+"In Lean, we do this with the `intro` tactic."
 msgstr ""
 "Abbiamo visto come fare `apply` di teoremi e ipotesi\n"
 "della forma `P → Q`. Ma come ci comportiamo se è il *goal* ad avere la forma "
@@ -5039,7 +5039,7 @@ msgstr "Sia $x$ un numero, allora $x \\le \\operatorname{succ}(x)$."
 
 #: Game.Levels.Addition.L02succ_add
 msgid ""
-"Well done! You now have enough tools to tackle the main boss of this level."
+"Well done! You now have enough tools to tackle the main boss of this world."
 msgstr ""
 "Ottimo lavoro! Ora sei abbastanza pratico per affrontare il boss principale "
 "di questo mondo."
@@ -5526,12 +5526,12 @@ msgid ""
 "Did you use induction on `y`?\n"
 "Here's a two-line proof of `add_left_eq_self` which uses "
 "`add_right_cancel`.\n"
-"If you want to inspect it, you can go into editor mode by clicking `</>` in "
+"If you want to inspect it, you can go into \"Editor mode\" by clicking `</>` in "
 "the top right\n"
 "and then just cut and paste the proof and move your cursor around it\n"
 "to see the hypotheses and goal at any given point\n"
 "(although you'll lose your own proof this way). Click `>_` to get\n"
-"back to command line mode.\n"
+"back to \"Typewriter mode\".\n"
 "```\n"
 "nth_rewrite 2 [← zero_add y]\n"
 "exact add_right_cancel x 0 y\n"