Merge pull request #116 from bearomorphism/typo-occur

Fix typo in Game

.i18n/en/Game.pot

@@ -450,7 +450,7 @@ msgstr ""
 msgid "Do that again!\n"
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
-"the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n"
+"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."
 msgstr ""
 

.i18n/fr/Game.json

@@ -744,7 +744,7 @@
  "Fermat's Last Theorem": "Grand théorème de Fermat",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Chaque nombre dans Lean est soit $0$, soit un successeur. Nous savons comment ajouter $0$,\nmais nous devons comprendre comment ajouter des successeurs. Disons que nous savons déjà\nque `37 + d = q`. Que devrait être la réponse à `37 + succ d` ? Eh bien,\n`succ d` est un de plus que `d`, donc `37 + succ d` devrait être `succ q`,\nle nombre un de plus que `q`. Plus généralement, `x + succ d` devrait\nêtre `succ (x + d)`. Ajoutons cela comme lemme.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nSi vous voyez `... + succ ...` dans votre but, `rw [add_succ]` est\ngénéralement une bonne idée.\n\nProuvons maintenant que `succ n = n + 1`. Trouvez comment introduire `+ succ`\ndans notre situation, puis `rw [add_succ]`. Alternez entre les onglets `+` (addition) et\n`012` (numéraux) sous \"Théorèmes\" à droite pour\nvoir quelles preuves vous pouvez réécrire.",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
  "Faites-le encore !\n\n`rw [zero_add] at «{h}»` essaie de remplir\nles arguments de `zero_add` (trouvant `«{x}»`) puis remplace toutes les occurrences de\n`0 + «{x}»` qu'il trouve. Par conséquent, il n'a pas réécrit `0 + «{y}»` pour l'instant.",
  "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "Avez-vous utilisé l'induction sur `y` ?\nVoici une preuve en deux lignes de `add_left_eq_self` qui utilise `add_right_cancel`.\nSi vous voulez l'inspecter, vous pouvez passer en mode éditeur en cliquant sur `</>` en haut à droite\npuis copier et coller la preuve et déplacer votre curseur autour\npour voir les hypothèses et le but à n'importe quel point\n(bien que vous perdiez ainsi votre propre preuve). Cliquez sur `>_` pour\nrevenir en mode ligne de commande.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
@@ -877,4 +877,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "# Aperçu\n\nNotre tactique maison `simp_add` résoudra tout but de\nla forme `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "# Aperçu\n\nLe simplificateur de Lean, `simp`, réécrira chaque lemme\nmarqué `simp` et chaque lemme fourni par l'utilisateur, autant que possible.\nDe plus, il tentera d'ordonner les variables dans un ordre interne si on lui donne\ndes lemmes comme `add_comm`, afin de ne pas tomber dans une boucle infinie."}
+ "# Aperçu\n\nLe simplificateur de Lean, `simp`, réécrira chaque lemme\nmarqué `simp` et chaque lemme fourni par l'utilisateur, autant que possible.\nDe plus, il tentera d'ordonner les variables dans un ordre interne si on lui donne\ndes lemmes comme `add_comm`, afin de ne pas tomber dans une boucle infinie."}

.i18n/fr/Game.po

@@ -2447,7 +2447,7 @@ msgid ""
 "Do that again!\n"
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
-"the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n"
+"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."
 msgstr ""
 "Faites-le encore !\n"

.i18n/it/Game.json

@@ -738,7 +738,7 @@
  "Fermat's Last Theorem": "L'ultimo teorema di Fermat",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Ogni numero in Lean è $0$ oppure il successore di un altro numero. Abbiamo già visto come aggiungere $0$,\ne ci rimane da capire come aggiungere un successore. Ipotizziamo di sapere\nche vale l'uguaglianza `37 + d = q`. A cosa dovrebbe essere uguale `37 + succ d`? Beh,\n`succ d` è un'unità più grande di `d`, quindi `37 + succ d` dovrebbe essere `succ q`,\nossia un'unità più grande di `q`. In generale `x + succ d` dovrebbe\ndare `succ (x + d)`. Formalizziamo questo ragionamento in un lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nQuando vedi `... + succ ...` nel goal, eseguire `rw [add_succ]` è una\nbuona idea.\n\nDimostriamo ora che `succ n = n + 1`. Cerca di introdurre un `+ succ` nel\ngoal, poi esegui `rw [add_succ]`. Controlla entrambi i tab `+` (addizione) e\n`012` (numeri) nella sezione \"Teoremi\" a destra\nper vedere quali teoremi da riscrivere hai a disposizione.",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
  "Ripeti lo stesso comando!\n\n`rw [zero_add] at «{h}»` ha completato automaticamente\nla chiamata a `zero_add` (trovando l'argomento `«{x}»`) e poi ha sostituito tutte le occorrenze di\n`0 + «{x}»` in un solo colpo. Dunque non ha toccato `0 + «{y}»` ancora, perciò dovresti ripetere il comando.",
  "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "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```",
@@ -873,4 +873,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "# Overview\n\nLa nostra tattica casalinga `simp_add` risolverà qualsiasi goal\ndel tipo `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "# Overview\n\nIl semplificatore di Lean, `simp`, riscriverà ogni\nlemma con il tag `simp` e ogni lemma dato dall'utente, finché può.\nNon solo, cercherà di ordinare le variabili secondo la sua logica interna affinché non entri\nin un loop infinito quando utilizza lemmi come `add_comm`"}
+ "# Overview\n\nIl semplificatore di Lean, `simp`, riscriverà ogni\nlemma con il tag `simp` e ogni lemma dato dall'utente, finché può.\nNon solo, cercherà di ordinare le variabili secondo la sua logica interna affinché non entri\nin un loop infinito quando utilizza lemmi come `add_comm`"}

.i18n/it/Game.po

@@ -814,7 +814,7 @@ msgid ""
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all "
-"occurences of\n"
+"occurrences of\n"
 "`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "Ripeti lo stesso comando!\n"

.i18n/uk/Game.json

@@ -736,7 +736,7 @@
  "Fermat's Last Theorem": "Остання теорема Ферма",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Кожне число в Lean є або $0$, або наступним значенням (наступником). Ми знаємо, як додати $0$,\nале нам потрібно зрозуміти, як додати наступників. Скажімо, ми вже знаємо\nщо `37 + d = q`. Якою має бути відповідь на `37 + succ d`? Гаразд,\n`succ d` на одиницю більший за `d`, тому `37 + succ d` має бути `succ q`,\nчисло на один більше за `q`. Більш загально `x + succ d` повинен\nбути `succ (x + d)`. Додамо це як лему.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nЯкщо ви побачите `... + succ ...` у своїй меті, `rw [add_succ]`\nзазвичай хороша ідея.\n\nДавайте тепер доведемо, що `succ n = n + 1`. З’ясуйте, як додати `+ succ`\nу фокус, а потім зробіть `rw [add_succ]`. Перемикайте між вкладками `+` (додавання) і\n`012` (цифри) у розділі \"Теореми\" праворуч\nі подивіться, які докази ви можете переписати.",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
  "Зробіть це ще раз!\n\n`rw [zero_add] в «{h}»` намагається заповнити\nаргументи `zero_add` (знаходження `«{x}»`), потім вона замінює всі знайдені входження\n`0 + «{x}»`. Таким чином тактика не переписує `0 + «{y}»`.",
  "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "Ви використовували індукцію на `y`?\nОсь дворядковий доказ `add_left_eq_self`, який використовує `add_right_cancel`.\nЯкщо ви хочете перевірити його, ви можете перейти в режим редактора, натиснувши `</>` у верхньому правому куті\nа потім просто виріжте та вставте доказ і перемістіть курсор навколо нього\nщоб побачити гіпотези та мету в будь-якій точці\n(хоча таким чином ви втратите свій власний доказ). Натисніть `>_`, щоб\nповернутися назад до режиму командного рядка.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
@@ -869,4 +869,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "# Огляд\n\nНаша саморобна тактика `simp_add` вирішить довільні цілі\nу формі `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "# Огляд\n\nСпрощувач Lean, `simp`, перепише кожну лему\nз тегом `simp` і кожну лему, надану користувачем, настількі, наскільки це можливо.\nКрім того, він намагатиметься впорядкувати змінні у внутрішньому порядку, якщо йому буде скормлено\nлеми, такі як `add_comm`, щоб він не перейшов в нескінченний цикл."}
+ "# Огляд\n\nСпрощувач Lean, `simp`, перепише кожну лему\nз тегом `simp` і кожну лему, надану користувачем, настількі, наскільки це можливо.\nКрім того, він намагатиметься впорядкувати змінні у внутрішньому порядку, якщо йому буде скормлено\nлеми, такі як `add_comm`, щоб він не перейшов в нескінченний цикл."}

.i18n/uk/Game.po

@@ -2567,7 +2567,7 @@ msgid ""
 "Do that again!\n"
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
-"the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences "
+"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."
 msgstr ""

.i18n/zh/Game.json

@@ -710,7 +710,7 @@
  "Fermat's Last Theorem": "费马大定理",
  "Every number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.":
  "Lean 中的每个数字要么是 $0$ 要么是后继数。我们已经知道如何加 $0$，\n我们还需要弄清楚如何添加后继数。假设我们已经知道\n`37 + d = q`。 `37 + succ d` 的答案应该是什么？\n`succ d` 比 `d` 大1，因此 `37 + succ d` 应该是 `succ q`，\n也就是比 `q` 大1。更一般地说，`x + succ d` 应该\n为 `succ (x + d)`。让我们将其添加为定理。\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\n如果您在证明目标中看到 `... + succ ...`，那么用 `rw [add_succ]` 改写\n通常是个好主意。\n\n现在让我们证明 `succ n = n + 1`。弄清楚如何引入 `+ succ` \n，然后再 `rw [add_succ]`。在右侧“定理”下的 `+`（加法）和\n `012`（数字）选项卡里\n看看你可以用哪些证明重写目标。\n\n在 Lean 中，每个数字要么是 $0$，要么是某个数字的后继数。我们已经掌握了如何加上 $0$，下一步需要明白如何加上后继数。设想我们已经知道 `37 + d = q`。那么 `37 + succ d` 应该是什么呢？由于 `succ d` 比 `d` 多 $1$，所以 `37 + succ d` 应该等于 `succ q`，也就是 `q` 加 $1$。更一般地，`x + succ d` 应等于 `succ (x + d)`。我们把这个规则加为一个引理：\n\n- `add_succ x d : x + succ d = succ (x + d)`\n\n当你在证明目标中遇到 `... + succ ...` 形式时，使用 `rw [add_succ]` 来重写通常是一个好策略。\n\n现在，让我们来证明 `succ n = n + 1`。思考如何先引入 `+ succ` 形式，然后再应用 `rw [add_succ]` 策略。请在右侧“定理”部分的 `+`（代表加法）和 `012`（代表数字）标签页中查找可以用来重写目标的定理。",
- "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
+ "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurrences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.":
  "再做一次！\n\n`rw [zero_add] at «{h}»` 试图填充 `zero_add` 的参数（找到 `«{x}»`），然后替换它找到的所有 `0 + «{x}»` 出现的地方。因此，`0 + «{y}»`还没有被重写 。",
  "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `</>` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```":
  "你是否对 `y` 使用了归纳法？\n这里有一个使用 `add_right_cancel` 证明 `add_left_eq_self`的两行证明。如果你想查看它，你可以通过点击右上角的 `</>` 进入编辑器模式，然后只需剪切和粘贴证明，并在其周围移动你的光标，以查看在任何给定点的假设和目标（尽管这样做你会失去自己的证明）。点击 `>_` 返回命令行模式。\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```",
@@ -840,4 +840,4 @@
  "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.":
  "## 概述\n\n我们自制的策略 `simp_add` 将解决以下形式的任意目标：\n `a + (b + c) + (d + e) = e + (d + (c + b)) + a`。",
  "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.":
- "## 概述\n\nLean 的简化器 `simp` 将它将用每个用户提供给它的引理\n以及所有标记为 `simp` 的引理重写目标。\n此外，如果提供了如`add_comm`这样的引理，它将尝试将对变量排序，以避免陷入无限循环。"}
+ "## 概述\n\nLean 的简化器 `simp` 将它将用每个用户提供给它的引理\n以及所有标记为 `simp` 的引理重写目标。\n此外，如果提供了如`add_comm`这样的引理，它将尝试将对变量排序，以避免陷入无限循环。"}

.i18n/zh/Game.po

@@ -746,7 +746,7 @@ msgid ""
 "\n"
 "`rw [zero_add] at «{h}»` tries to fill in\n"
 "the arguments to `zero_add` (finding `«{x}»`) then it replaces all "
-"occurences of\n"
+"occurrences of\n"
 "`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
 msgstr ""
 "再做一次！\n"

Game/Levels/Implication/L02exact2.lean

@@ -17,7 +17,7 @@ Statement (x y : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
   Hint (hidden := true) "Do that again!
 
   `rw [zero_add] at {h}` tries to fill in
-  the arguments to `zero_add` (finding `{x}`) then it replaces all occurences of
+  the arguments to `zero_add` (finding `{x}`) then it replaces all occurrences of
   `0 + {x}` it finds. Therefor, it did not rewrite `0 + {y}`, yet."
   rw [zero_add] at h
   Hint "Now you could finish with `rw [{h}]` then `rfl`, but `exact {h}`

Game/Levels/OldProposition/Level_8.lean

@@ -28,7 +28,7 @@ Statement
   repeat rw [Not]
   ```
 
-  to get rid of the two occurences of `¬`. (`Not` is the name of `¬`)
+  to get rid of the two occurrences of `¬`. (`Not` is the name of `¬`)
 
   I'm sure you can take it from there."
   Branch