NNG/.i18n/en/Game.pot

msgid ""
msgstr "Project-Id-Version: Game v4.22.0\n"
"Report-Msgid-Bugs-To: \n"
"POT-Creation-Date: 2025-09-23\n"
"Last-Translator: \n"
"Language-Team: none\n"
"Language: en\n"
"Content-Type: text/plain; charset=UTF-8\n"
"Content-Transfer-Encoding: 8bit"

#: Game.Levels.LessOrEqual.L09succ_le_succ
msgid "We've proved that `x ≤ 0` implies `x = 0`. The last two levels\n"
"in this world will prove which numbers are `≤ 1` and `≤ 2`.\n"
"This lemma will be helpful for them."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "If $x$ and $y$ are numbers, then either $x \\leq y$ or $y \\leq x$."
msgstr ""

#: Game.Levels.AdvAddition.L01add_right_cancel
msgid "`add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$"
msgstr ""

#: Game.Levels.LessOrEqual.L10le_one
msgid "x ≤ 1"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "Now finish the job with `rfl`."
msgstr ""

#: Game.Levels.Algorithm.L08decide
msgid "Implementing the algorithm for equality of naturals, and the proof that it is correct,\n"
"looks like this:\n"
"\n"
"```\n"
"instance instDecidableEq : DecidableEq ℕ\n"
"| 0, 0 => isTrue <| by\n"
"  show 0 = 0\n"
"  rfl\n"
"| succ m, 0 => isFalse <| by\n"
"  show succ m ≠ 0\n"
"  exact succ_ne_zero m\n"
"| 0, succ n => isFalse <| by\n"
"  show 0 ≠ succ n\n"
"  exact zero_ne_succ n\n"
"| succ m, succ n =>\n"
"  match instDecidableEq m n with\n"
"  | isTrue (h : m = n) => isTrue <| by\n"
"    show succ m = succ n\n"
"    rw [h]\n"
"    rfl\n"
"  | isFalse (h : m ≠ n) => isFalse <| by\n"
"    show succ m ≠ succ n\n"
"    exact succ_ne_succ m n h\n"
"```\n"
"\n"
"This Lean code is a formally verified algorithm for deciding equality\n"
"between two naturals. I've typed it in already, behind the scenes.\n"
"Because the algorithm is formally verified to be correct, we can\n"
"use it in Lean proofs. You can run the algorithm with the `decide` tactic."
msgstr ""

#: Game.Levels.Multiplication.L04mul_comm
msgid "The first sub-boss of Multiplication World is `mul_comm x y : x * y = y * x`.\n"
"\n"
"When you've proved this theorem we will have \"spare\" proofs\n"
"such as `zero_mul`, which is now easily deducible from `mul_zero`.\n"
"But we'll keep hold of these proofs anyway, because it's convenient\n"
"to have exactly the right tool for a job."
msgstr ""

#: Game.Levels.Multiplication.L09mul_assoc
msgid "mul_assoc"
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "Now we can prove the `or` statement by proving the statement on the right,\n"
"so use the `right` tactic."
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "Every number in Lean is either $0$ or a successor. We know how to add $0$,\n"
"but we need to figure out how to add successors. Let's say we already know\n"
"that `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`,\n"
"the number one bigger than `q`. More generally `x + succ d` should\n"
"be `succ (x + d)`. Let's add this as a lemma.\n"
"\n"
"* `add_succ x d : x + succ d = succ (x + d)`\n"
"\n"
"If you ever see `... + succ ...` in your goal, `rw [add_succ]` is\n"
"normally a good idea.\n"
"\n"
"Let's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\n"
"the picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n"
"`012` (numerals) tabs under \"Theorems\" on the right to\n"
"see which proofs you can rewrite."
msgstr ""

#: Game.Levels.Algorithm.L03add_algo2
msgid "Lean's simplifier, `simp`, is \"`rw` on steroids\". It will rewrite every lemma\n"
"tagged with `simp` and every lemma fed to it by the user, as much as it can.\n"
"\n"
"This level is not a level which you want to solve by hand.\n"
"Get the simplifier to solve it for you."
msgstr ""

#: Game.Levels.Implication.L10one_ne_zero
msgid "We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\n"
"if we have a hypothesis `succ n = 0`? It's the wrong way around!\n"
"\n"
"The `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\n"
"to `y ≠ x`. And `symm at h`\n"
"does the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\n"
"the proof `zero_ne_one`; now try proving $1 \\neq 0$."
msgstr ""

#: Game.Levels.Implication.L11two_add_two_ne_five
msgid "Here's my proof:\n"
"```\n"
"intro h\n"
"rw [add_succ, add_succ, add_zero] at h\n"
"repeat apply succ_inj at h\n"
"apply zero_ne_succ at h\n"
"exact h\n"
"```\n"
"\n"
"Even though Lean is a theorem prover, right now it's pretty clear that we have not\n"
"developed enough material to make it an adequate calculator. In Algorithm\n"
"World, a more computer-sciency world, we will develop machinery which makes\n"
"questions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.\n"
"Alternatively you can do more mathematics in Advanced Addition World, where we prove\n"
"the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\n"
"decide your route."
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "This lemma would have been easy if we had known that `x + y = y + x`. That theorem\n"
"  is called `add_comm` and it is *true*, but unfortunately its proof *uses* both\n"
"  `add_zero` and `zero_add`!\n"
"\n"
"  Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`."
msgstr ""

#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
msgid "`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`."
msgstr ""

#: Game.Levels.Power.L01zero_pow_zero
msgid "$0 ^ 0 = 1$"
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "This level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition\n"
"World's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the\n"
"lemma `le_one` from `≤` world.\n"
"\n"
"We'll prove it using a new and very useful tactic called `have`."
msgstr ""

#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
msgid "mul_left_ne_zero"
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "the rw tactic"
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "## Summary\n"
"\n"
"The `use` tactic makes progress with goals which claim something *exists*.\n"
"If the goal claims that some `x` exists with some property, and you know\n"
"that `x = 37` will work, then `use 37` will make progress.\n"
"\n"
"Because `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\n"
"you can make progress on goals of the form `a ≤ b` by `use`ing the\n"
"number which is morally `b - a` (i.e. `use b - a`)\n"
"\n"
"Any 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`"
msgstr ""

#: Game.Levels.AdvMultiplication.L07mul_ne_zero
msgid "mul_ne_zero"
msgstr ""

#: Game.Levels.Algorithm.L08decide
msgid "You can read more about the `decide` tactic by clicking\n"
"on it in the top right."
msgstr ""

#: Game.Levels.LessOrEqual.L10le_one
msgid "`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`."
msgstr ""

#: Game.Levels.AdvAddition.L02add_left_cancel
msgid "add_left_cancel"
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "You can probably take it from here."
msgstr ""

#: Game.Levels.Tutorial.L08twoaddtwo
msgid "2+2=4"
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "Try `cases «{hd}» with h1 h2`."
msgstr ""

#: Game.Levels.AdvMultiplication
msgid "Advanced *Addition* World proved various implications\n"
"involving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\n"
"These lemmas were used to prove basic facts about ≤ in ≤ World.\n"
"\n"
"In Advanced Multiplication World we prove analogous\n"
"facts about multiplication, such as `x * y = 1 → x = 1`, and\n"
"`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\n"
"us for Divisibility World.\n"
"\n"
"Multiplication World is more complex than Addition World. In the same\n"
"way, Advanced Multiplication world is more complex than Advanced Addition\n"
"World. One reason for this is that certain intermediate results are only\n"
"true under the additional hypothesis that one of the variables is non-zero.\n"
"This causes some unexpected extra twists."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "Now `rw [«{h}»] at «{h2}»` so you can `apply le_one at «{h2}»`."
msgstr ""

#: Game.Levels.Power.L01zero_pow_zero
msgid "zero_pow_zero"
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
msgid "If $x \\leq 0$, then $x=0$."
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "Applying a proof of $P\\implies Q$ to the *goal* changes $Q$ to $P$.\n"
"Now try `rw [succ_eq_add_one]` to make the goal more like the hypothesis."
msgstr ""

#: Game.Levels.Power.L05pow_two
msgid "Note: this lemma will be useful for the final boss!"
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "Note that `succ a + «{d}»` means `(succ a) + «{d}»`. Put your cursor\n"
"on any `succ` in the goal or assumptions to see what exactly it's eating."
msgstr ""

#: Game.Levels.Implication.L06intro
msgid "intro"
msgstr ""

#: Game.Levels.Implication.L03apply
msgid "## Summary\n"
"\n"
"If `t : P → Q` is a proof that $P \\implies Q$, and `h : P` is a proof of `P`,\n"
"then `apply t at h` will change `h` to a proof of `Q`. The idea is that if\n"
"you know `P` is true, then you can deduce from `t` that `Q` is true.\n"
"\n"
"If the *goal* is `Q`, then `apply t` will \\\"argue backwards\\\" and change the\n"
"goal to `P`. The idea here is that if you want to prove `Q`, then by `t`\n"
"it suffices to prove `P`, so you can reduce the goal to proving `P`.\n"
"\n"
"### Example:\n"
"\n"
"`succ_inj x y` is a proof that `succ x = succ y → x = y`.\n"
"\n"
"So if you have a hypothesis `h : succ (a + 37) = succ (b + 42)`\n"
"then `apply succ_inj at h` will change `h` to `a + 37 = b + 42`.\n"
"You could write `apply succ_inj (a + 37) (b + 42) at h`\n"
"but Lean is smart enough to figure out the inputs to `succ_inj`.\n"
"\n"
"### Example\n"
"\n"
"If the goal is `a * b = 7`, then `apply succ_inj` will turn the\n"
"goal into `succ (a * b) = succ 7`."
msgstr ""

#: Game.Levels.Multiplication.L09mul_assoc
msgid "A passing mathematician notes that you've proved\n"
"that the natural numbers are a commutative semiring.\n"
"\n"
"If you want to begin your journey to the final boss, head for Power World."
msgstr ""

#: Game.Levels.AdvMultiplication.L05le_mul_right
msgid "One day this game will have a Prime Number World, with a final boss\n"
"of proving that $2$ is prime.\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"
"`mul_le_mul_right`."
msgstr ""

#: Game.Levels.Power.L01zero_pow_zero
msgid "`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"
"\n"
"Note in particular that `0 ^ 0 = 1`."
msgstr ""

#: Game.Levels.LessOrEqual.L03le_succ_self
msgid "If you `use` the wrong number, you get stuck with a goal you can't prove.\n"
"What number will you `use` here?"
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "Now `apply succ_inj at h` to cancel the `succ`s."
msgstr ""

#: Game.Levels.AdvAddition
msgid "In Advanced Addition World we will prove some basic\n"
"addition facts such as $x+y=x\\implies y=0$. The theorems\n"
"proved in this world will be used to build\n"
"a theory of inequalities in `≤` World.\n"
"\n"
"Click on \"Start\" to proceed."
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "`four_eq_succ_three` is a proof of `4 = succ 3`."
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "In this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n"
"\n"
"Wait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\n"
"This is `zero_add`, which is different.\n"
"\n"
"The 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\n"
"we know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n"
"\n"
"The base case will require us to prove `0 + 0 = 0`, and the inductive step\n"
"will 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"
"\n"
"See 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\n"
"back to \"Typewriter mode\" by clicking the `>_` button in the top right.)"
msgstr ""

#: Game.Levels.Algorithm.L08decide
msgid "decide"
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "Now `rfl` will work."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "Now let's `apply` our new theorem. Execute `apply succ_inj at h`\n"
"to change `h` to a proof of `x = 3`."
msgstr ""

#: Game.Levels.Multiplication.L03succ_mul
msgid "`succ_mul a b` is the proof that `succ a * b = a * b + b`.\n"
"\n"
"It could be deduced from `mul_succ` and `mul_comm`, however this argument\n"
"would be circular because the proof of `mul_comm` uses `mul_succ`."
msgstr ""

#: Game.Levels.Algorithm.L09decide2
msgid "We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one."
msgstr ""

#: Game.Levels.Addition
msgid "Addition World"
msgstr ""

#: Game.Levels.Algorithm.L05pred
msgid "If $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ then $a=b$."
msgstr ""

#: Game.Levels.Implication.L10one_ne_zero
msgid "What do you think of this two-liner:\n"
"```\n"
"symm\n"
"exact zero_ne_one\n"
"```\n"
"\n"
"`exact` doesn't just take hypotheses, it will eat any proof which exists\n"
"in the system."
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
msgid "You want to use `add_right_eq_zero`, which you already\n"
"proved, but you'll have to start with `symm at` your hypothesis."
msgstr ""

#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
msgid "In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\n"
"from a false statement. The `tauto` tactic will close this goal."
msgstr ""

#: Game.Levels.Algorithm.L01add_left_comm
msgid "add_left_comm"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "`one_eq_succ_zero` is a proof of `1 = succ 0`.\""
msgstr ""

#: Game.Levels.Power.L02zero_pow_succ
msgid "We've just seen that `0 ^ 0 = 1`, but if `n`\n"
"is a successor, then `0 ^ n = 0`. We prove that here."
msgstr ""

#: Game.Levels.Power.L10FLT
msgid "For all naturals $a$ $b$ $c$ and $n$, we have\n"
"$$(a+1)^{n+3}+(b+1)^{n+3}\\not=(c+1)^{n+3}.$$"
msgstr ""

#: Game.Levels.Algorithm.L09decide2
msgid "Congratulations! You've finished Algorithm World. These algorithms\n"
"will be helpful for you in Even-Odd World (when someone gets around to\n"
"implementing it)."
msgstr ""

#: Game.Levels.Implication.L11two_add_two_ne_five
msgid "2 + 2 ≠ 5 is boring to prove in full, given only the tools we have currently.\n"
"To make it a bit less painful, I have unfolded all of the numerals for you.\n"
"See if you can use `zero_ne_succ` and `succ_inj` to prove this."
msgstr ""

#: Game.Levels.Power.L06pow_add
msgid "`pow_add a m n` is a proof that $a^{m+n}=a^ma^n.$"
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "Do that again!\n"
"\n"
"`rw [zero_add] at «{h}»` tries to fill in\n"
"the arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n"
"`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet."
msgstr ""

#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
msgid "My proof:\n"
"```\n"
"cases h with d hd\n"
"use d * t\n"
"rw [hd, add_mul]\n"
"rfl\n"
"```"
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "Arguing backwards"
msgstr ""

#: Game.Levels.Multiplication.L09mul_assoc
msgid "Multiplication is associative.\n"
"In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
"$(ab)c = a(bc)$."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "Those of you interested in speedrunning the game may want to know\n"
"that `repeat rw [add_zero]` will do both rewrites at once."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "mul_right_eq_one"
msgstr ""

#: Game.Levels.Addition.L04add_assoc
msgid "A passing mathematician congratulates you on proving that naturals\n"
"are an additive commutative monoid.\n"
"\n"
"Let's practice using `add_assoc` and `add_comm` in one more level,\n"
"before we leave addition world."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "`is_zero_succ a` is a proof of `is_zero (succ a) = False`."
msgstr ""

#: Game.Levels.AdvAddition.L06add_left_eq_zero
msgid "A proof that $a+b=0 \\implies b=0$."
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "A proof that $a+b=0 \\implies a=0$."
msgstr ""

#: Game.Levels.LessOrEqual.L03le_succ_self
msgid "`le_succ_self x` is a proof that `x ≤ succ x`."
msgstr ""

#: Game.Levels.Algorithm.L05pred
msgid "`pred_succ n` is a proof of `pred (succ n) = n`."
msgstr ""

#: Game.Levels.Tutorial.L01rfl
msgid "In order to use the tactic `rfl` you can enter it in the text box\n"
"under the goal and hit \"Execute\"."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "`is_zero_zero` is a proof of `is_zero 0 = True`."
msgstr ""

#: Game.Levels.AdvAddition.L06add_left_eq_zero
msgid "If $a+b=0$ then $b=0$."
msgstr ""

#: Game.Levels.Power.L01zero_pow_zero
msgid "`pow_zero a : a ^ 0 = 1` is one of the two axioms\n"
"defining exponentiation in this game."
msgstr ""

#: Game.Levels.Implication.L11two_add_two_ne_five
msgid "$2+2≠5$."
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "If $x$ is a number, then $x \\le x$."
msgstr ""

#: Game.Levels.LessOrEqual.L02zero_le
msgid "If $x$ is a number, then $0 \\le x$."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "You can put a `←` in front of any theorem provided to `rw` to rewrite\n"
"the other way around. Look at the docs for `rw` for an explanation. Type `←` with `\\l`."
msgstr ""

#: Game.Levels.AdvAddition.L04add_right_eq_self
msgid "$x+y=x\\implies y=0$."
msgstr ""

#: Game.Levels.Power
msgid "This world introduces exponentiation. If you want to define `37 ^ n`\n"
"then, as always, you will need to know what `37 ^ 0` is, and\n"
"what `37 ^ (succ d)` is, given only `37 ^ d`.\n"
"\n"
"You 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"
"\n"
"Using only these, can you get past the final boss level?\n"
"\n"
"The levels in this world were designed by Sian Carey, a UROP student\n"
"at Imperial College London, funded by a Mary Lister McCammon Fellowship\n"
"in the summer of 2019. Thanks to Sian and also thanks to Imperial\n"
"College for funding her."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "$\\operatorname{succ}(a) \\neq 0$."
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "Split into cases `c = 0` and `c = succ e` with `cases c with e`."
msgstr ""

#: Game.Levels.Implication.L01exact
msgid "Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$."
msgstr ""

#: Game.Levels.Algorithm.L01add_left_comm
msgid "Having to rearrange variables manually using commutativity and\n"
"associativity is very tedious. We start by reminding you of this. `add_left_comm`\n"
"is a key component in the first algorithm which we'll explain, but we need\n"
"to prove it manually.\n"
"\n"
"Remember that you can do precision commutativity rewriting\n"
"with things like `rw [add_comm b c]`. And remember that\n"
"`a + b + c` means `(a + b) + c`."
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "`mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`."
msgstr ""

#: Game.Levels.Implication.L11two_add_two_ne_five
msgid "2 + 2 ≠ 5"
msgstr ""

#: Game.Levels.Implication.L03apply
msgid "Start with `apply h2 at h1`. This will change `h1` to `y = 42`."
msgstr ""

#: Game.Levels.Implication.L08ne
msgid "If $x=y$ and $x \\neq y$ then we can deduce a contradiction."
msgstr ""

#: Game.Levels.Multiplication.L04mul_comm
msgid "`mul_comm` is the proof that multiplication is commutative. More precisely,\n"
"`mul_comm a b` is the proof that `a * b = b * a`."
msgstr ""

#: Game.Levels.LessOrEqual.L11le_two
msgid "If $x \\leq 2$ then $x = 0$ or $1$ or $2$."
msgstr ""

#: Game.Levels.LessOrEqual.L06le_antisymm
msgid "x ≤ y and y ≤ x implies x = y"
msgstr ""

#: Game.Levels.Power.L08pow_pow
msgid "One of the best named levels in the game, a savage `pow_pow`\n"
"sub-boss appears as the music reaches a frenzy. What\n"
"else could there be to prove about powers after this?"
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "`mul_zero m` is the proof that `m * 0 = 0`."
msgstr ""

#: Game.Levels.Multiplication.L08add_mul
msgid "Addition is distributive over multiplication.\n"
"In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
"$(a + b) \\times c = ac + bc$."
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "`zero_ne_succ n` is the proof that `0 ≠ succ n`.\n"
"\n"
"In Lean, `a ≠ b` is *defined to mean* `a = b → False`. Hence\n"
"`zero_ne_succ n` is really a proof of `0 = succ n → False`.\n"
"Here `False` is a generic false statement. This means that\n"
"you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`."
msgstr ""

#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
msgid "Multiplication usually makes a number bigger, but multiplication by zero can make\n"
"it smaller. Thus many lemmas about inequalities and multiplication need the\n"
"hypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.\n"
"To help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\n"
"on the right to see what it does."
msgstr ""

#: Game.Levels.Multiplication
msgid "Multiplication World"
msgstr ""

#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
msgid "Reduce to the previous lemma with `nth_rewrite 2 [← mul_one a] at h`"
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "Very well done.\n"
"\n"
"A passing mathematician remarks that with you've just proved that `ℕ` is totally\n"
"ordered.\n"
"\n"
"The final few levels in this world are much easier."
msgstr ""

#: Game.Levels.Power.L02zero_pow_succ
msgid "Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if\n"
"$n$ is a successor."
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "Now you can `apply zero_ne_succ at h`."
msgstr ""

#: Game.Levels.AdvMultiplication.L05le_mul_right
msgid "Here's what I was thinking of:\n"
"```\n"
"apply mul_left_ne_zero at h\n"
"apply one_le_of_ne_zero at h\n"
"apply mul_le_mul_right 1 b a at h\n"
"rw [one_mul, mul_comm] at h\n"
"exact h\n"
"```"
msgstr ""

#: Game.Levels.LessOrEqual.L10le_one
msgid "We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.\n"
"Now we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`."
msgstr ""

#: Game.Levels.Power.L02zero_pow_succ
msgid "`pow_succ a b : a ^ (succ b) = a ^ b * a` is one of the\n"
"two axioms defining exponentiation in this game."
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "intro practice"
msgstr ""

#: Game.Levels.Implication.L10one_ne_zero
msgid "## Summary\n"
"\n"
"The `symm` tactic will change a goal or hypothesis of\n"
"the form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\n"
"and on `X ↔ Y`.\n"
"\n"
"### Example\n"
"\n"
"If the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n"
"\n"
"### Example\n"
"\n"
"If `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`."
msgstr ""

#: Game.Levels.Addition.L05add_right_comm
msgid ""
"`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n"
"\n"
"In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\n"
"as `a + b + c = a + c + b`."
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "zero_ne_succ"
msgstr ""

#: Game.Levels.LessOrEqual.L11le_two
msgid "Nice!\n"
"\n"
"The next step in the development of order theory is to develop\n"
"the theory of the interplay between `≤` and multiplication.\n"
"If you've already done Multiplication World, you're now ready for\n"
"Advanced Multiplication World. Click on \"Leave World\" to access it."
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "Now you need to figure out which number to `use`. See if you can take it from here."
msgstr ""

#: Game.Levels.Algorithm.L05pred
msgid "We now start work on an algorithm to do addition more efficiently. Recall that\n"
"we defined addition by recursion, saying what it did on `0` and successors.\n"
"It is an axiom of Lean that recursion is a valid\n"
"way to define functions from types such as the naturals.\n"
"\n"
"Let's define a new function `pred` from the naturals to the naturals, which\n"
"attempts to subtract 1 from the input. The definition is this:\n"
"\n"
"```\n"
"pred 0 := 37\n"
"pred (succ n) := n\n"
"```\n"
"\n"
"We cannot subtract one from 0, so we just return a junk value. As well as this\n"
"definition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\n"
"Let's use this lemma to prove `succ_inj`, the theorem which\n"
"Peano assumed as an axiom and which we have already used extensively without justification."
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "Start with `rw [two_eq_succ_one]` to begin to break `2` down into its definition."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "Now rewrite `succ_eq_add_one` backwards at `h`\n"
"to get the right hand side."
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "`succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`."
msgstr ""

#: Game.Levels.AdvAddition.L02add_left_cancel
msgid "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$"
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "Let's first get `h` into the form `succ x = succ 3` so we can\n"
"apply `succ_inj`. First execute `rw [four_eq_succ_three] at h`\n"
"to change the 4 on the right hand side."
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\n"
"several reasons. One of these is that\n"
"we need to introduce a new idea: we will need to understand the concept of\n"
"mathematical induction a little better.\n"
"\n"
"Starting with `induction b with d hd` is too naive, because in the inductive step\n"
"the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\n"
"so the induction hypothesis does not apply!\n"
"\n"
"Assume `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,\n"
"because we now have the flexibility to change `c`."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "In the next level, we'll do the same proof but backwards."
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "try rewriting `add_zero`."
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "`mul_succ a b` is the proof that `a * succ b = a * b + a`."
msgstr ""

#: Game.Levels.Tutorial.L04rw_backwards
msgid "Try `rw [← one_eq_succ_zero]` to change `succ 0` into `1`."
msgstr ""

#: Game.Levels.Power.L03pow_one
msgid "For all naturals $a$, $a ^ 1 = a$."
msgstr ""

#: Game.Levels.Algorithm.L03add_algo2
msgid "# Overview\n"
"\n"
"Lean's simplifier, `simp`, will rewrite every lemma\n"
"tagged with `simp` and every lemma fed to it by the user, as much as it can.\n"
"Furthermore, it will attempt to order variables into an internal order if fed\n"
"lemmas such as `add_comm`, so that it does not go into an infinite loop."
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
msgid "x ≤ 0 → x = 0"
msgstr ""

#: Game.Levels.AdvAddition
msgid "Advanced Addition World"
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey."
msgstr ""

#: Game.Levels.Algorithm.L08decide
msgid "# Summary\n"
"\n"
"`decide` will attempt to solve a goal if it can find an algorithm which it\n"
"can run to solve it.\n"
"\n"
"## Example\n"
"\n"
"A term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\n"
"are equal or different. Hence, once this term is made and made into an `instance`,\n"
"the `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`."
msgstr ""

#: Game.Levels.AdvAddition.L02add_left_cancel
msgid "$n+a=n+b\\implies a=b$."
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "For any natural number $m$, we have $ m \\times 1 = m$."
msgstr ""

#: Game.Levels.Algorithm.L03add_algo2
msgid "making life simple"
msgstr ""

#: Game.Levels.Addition.L04add_assoc
msgid "add_assoc (associativity of addition)"
msgstr ""

#: Game.Levels.Algorithm.L09decide2
msgid "$2+2 \\neq 5.$"
msgstr ""

#: Game.Levels.Multiplication.L04mul_comm
msgid "mul_comm"
msgstr ""

#: Game.Levels.Algorithm.L03add_algo2
#: Game.Levels.Algorithm.L04add_algo3
msgid "If $a, b,\\ldots h$ are arbitrary natural numbers, we have\n"
"$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$."
msgstr ""

#: Game.Levels.AdvAddition.L01add_right_cancel
msgid "Start with induction on `n`."
msgstr ""

#: Game.Levels.Tutorial.L04rw_backwards
msgid "If `h` is a proof of `X = Y` then `rw [h]` will\n"
"turn `X`s into `Y`s. But what if we want to\n"
"turn `Y`s into `X`s? To tell the `rw` tactic\n"
"we want this, we use a left arrow `←`. Type\n"
"`\\l` and then hit the space bar to get this arrow.\n"
"\n"
"Let's prove that $2$ is the number after the number\n"
"after $0$ again, this time by changing `succ (succ 0)`\n"
"into `2`."
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "Now you could finish with `rw [«{h}»]` then `rfl`, but `exact «{h}»`\n"
"does it in one line."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "`tauto` is good enough to solve this goal."
msgstr ""

#: Game.Levels.Power.L01zero_pow_zero
msgid "Mathematicians sometimes argue that `0 ^ 0 = 0` is also\n"
"a good convention. But it is not a good convention in this\n"
"game; all the later levels come out beautifully with the\n"
"convention that `0 ^ 0 = 1`."
msgstr ""

#: Game.Levels.AdvMultiplication.L07mul_ne_zero
msgid "`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`."
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid ""
"Multiplication distributes\n"
"over addition on the left.\n"
"\n"
"`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`."
msgstr ""

#: Game.Levels.AdvAddition.L01add_right_cancel
msgid "add_right_cancel"
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "Start with `intro h`."
msgstr ""

#: Game.Levels.Power.L01zero_pow_zero
msgid "Mathematicians sometimes debate what `0 ^ 0` is;\n"
"the answer depends, of course, on your definitions. In this\n"
"game, `0 ^ 0 = 1`. See if you can prove it.\n"
"\n"
"Check out the *Pow* tab in your list of theorems\n"
"to see the new proofs which are available."
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "`zero_add x` is the proof of `0 + x = x`.\n"
"\n"
"`zero_add` is a `simp` lemma, because replacing `0 + x` by `x`\n"
"is almost always what you want to do if you're simplifying an expression."
msgstr ""

#: Game.Levels.AdvAddition.L03add_left_eq_self
msgid "add_left_eq_self"
msgstr ""

#: Game.Levels.Multiplication
msgid ""
"How should we define `37 * x`? Just like addition, we need to give "
"definitions\n"
"when $x=0$ and when $x$ is a successor.\n"
"\n"
"The zero case is easy: we define `37 * 0` to be `0`. Now say we know\n"
"`37 * d`. What should `37 * succ d` be? Well, that's $(d+1)$ $37$s,\n"
"so it should be `37 * d + 37`.\n"
"\n"
"Here are the definitions in Lean.\n"
"\n"
"  * `mul_zero a : a * 0 = 0`\n"
"  * `mul_succ a d : a * succ d = a * d + a`\n"
"\n"
"In this world, we must not only prove facts about multiplication like `a * b "
"= b * a`,\n"
"we must also prove facts about how multiplication interacts with addition, "
"like `a * (b + c) = a * b + a * c`.\n"
"Let's get started."
msgstr ""

#: Game.Levels.LessOrEqual.L06le_antisymm
msgid "Here's my proof:\n"
"```\n"
"cases hxy with a ha\n"
"cases hyx with b hb\n"
"rw [ha]\n"
"rw [ha, add_assoc] at hb\n"
"symm at hb\n"
"apply add_right_eq_self at hb\n"
"apply add_right_eq_zero at hb\n"
"rw [hb, add_zero]\n"
"rfl\n"
"```\n"
"\n"
"A passing mathematician remarks that with antisymmetry as well,\n"
"you have proved that `≤` is a *partial order* on `ℕ`.\n"
"\n"
"The boss level of this world is to prove\n"
"that `≤` is a total order. Let's learn two more easy tactics\n"
"first."
msgstr ""

#: GameServer.RpcHandlers
msgid "level completed with warnings… 🎭"
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add a b`\n"
"is the proof that `(succ a) + b = succ (a + b)` for `a` and `b` numbers.\n"
"This result is what's standing in the way of `x + y = y + x`. Again\n"
"we have the problem that we are adding `b` to things, so we need\n"
"to use induction to split into the cases where `b = 0` and `b` is a successor."
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "Many people find `apply t at h` easy, but some find `apply t` confusing.\n"
"If you find it confusing, then just argue forwards.\n"
"\n"
"You can read more about the `apply` tactic in its documentation, which you can view by\n"
"clicking on the tactic in the list on the right."
msgstr ""

#: Game.Levels.Implication.L10one_ne_zero
msgid "`one_ne_zero` is a proof that `1 ≠ 0`."
msgstr ""

#: Game.Levels.Power.L06pow_add
msgid "pow_add"
msgstr ""

#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
msgid "Now take apart the existence statement with `cases ha with n hn`."
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,\n"
"so start with `cases b with d`."
msgstr ""

#: Game.Levels.Tutorial.L01rfl
msgid "The rfl tactic"
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "If $x=37$ or $y=42$, then $y=42$ or $x=37$."
msgstr ""

#: Game.Levels.Multiplication.L06two_mul
msgid "`two_mul m` is the proof that `2 * m = m + m`."
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "`mul_one m` is the proof that `m * 1 = m`."
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "## Summary\n"
"\n"
"If `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\n"
"attempts to prove the goal by induction on `n`, with the inductive\n"
"variable in the successor case being `d`, and the inductive hypothesis being `hd`.\n"
"\n"
"### Example:\n"
"If the goal is\n"
"```\n"
"0 + n = n\n"
"```\n"
"\n"
"then\n"
"\n"
"`induction n with d hd`\n"
"\n"
"will turn it into two goals. The first is `0 + 0 = 0`;\n"
"the second has an assumption `hd : 0 + d = d` and goal\n"
"`0 + succ d = succ d`.\n"
"\n"
"Note that you must prove the first\n"
"goal before you can access the second one."
msgstr ""

#: Game.Levels.Implication.L01exact
msgid "The `exact` tactic"
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "succ_add"
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid "Induction on `a` is the most troublesome, then `b`,\n"
"and `c` is the easiest."
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "Use `mul_eq_zero` and remember that `tauto` will solve a goal\n"
"if there are hypotheses `a = 0` and `a ≠ 0`."
msgstr ""

#: Game.Levels.Tutorial
msgid "Welcome to tutorial world! In this world we learn the basics\n"
"of proving theorems. The boss level of this world\n"
"is the theorem `2 + 2 = 4`.\n"
"\n"
"You prove theorems by solving puzzles using tools called *tactics*.\n"
"The aim is to prove the theorem by applying tactics\n"
"in the right order.\n"
"\n"
"Let's learn some basic tactics. Click on \"Start\" below\n"
"to begin your quest."
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "This time, use the `left` tactic."
msgstr ""

#: Game.Levels.Algorithm.L08decide
msgid "$20+20=40$."
msgstr ""

#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
msgid "If you have completed Algorithm World then you can use the `contrapose!` tactic\n"
"here. If not then I'll talk you through a manual approach."
msgstr ""

#: Game.Levels.Multiplication.L03succ_mul
msgid "Similarly we have `mul_succ`\n"
"but we're going to need `succ_mul` (guess what it says -- maybe you\n"
"are getting the hang of Lean's naming conventions).\n"
"\n"
"The last level from addition world might help you in this level.\n"
"If you can't remember what it is, you can go back to the\n"
"home screen by clicking the house icon and then taking a look.\n"
"You won't lose any progress."
msgstr ""

#: Game.Levels.Addition.L03add_comm
msgid "Induction on `a` or `b` -- it's all the same in this one."
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "Now rewrite `four_eq_succ_three` backwards to make the goal\n"
"equal to the hypothesis."
msgstr ""

#: Game.Levels.AdvAddition.L04add_right_eq_self
msgid "`add_right_eq_self x y` is the theorem that $x + y = x \\implies y=0.$"
msgstr ""

#: Game.Levels.AdvMultiplication.L07mul_ne_zero
msgid "Start with `apply eq_succ_of_ne_zero at ha` and `... at hb`"
msgstr ""

#: Game
msgid "*Game version: 4.3*\n"
"\n"
"*Recent additions: bug fixes*\n"
"\n"
"## Progress saving\n"
"\n"
"The game stores your progress in your local browser storage.\n"
"If you delete it, your progress will be lost!\n"
"\n"
"Warning: In most browsers, deleting cookies will also clear the local storage\n"
"(or \"local site data\"). Make sure to download your game progress first!\n"
"\n"
"## Credits\n"
"\n"
"* **Creators:** Kevin Buzzard, Jon Eugster\n"
"* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n"
"* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n"
"* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n"
"* **Additional thanks:** All the student beta testers, all the schools\n"
"who invited Kevin to speak, and all the schoolkids who asked him questions\n"
"about the material.\n"
"\n"
"## Resources\n"
"\n"
"* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n"
"* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n"
"\n"
"## Problems?\n"
"\n"
"Please ask any questions about this game in the\n"
"[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\n"
"the stream \"New Members\". The community will happily help. Note that\n"
"the Lean Zulip chat is a professional research forum.\n"
"Please use your full real name there, stay on topic, and be nice. If you're\n"
"looking for somewhere less formal (e.g. you want to post natural number\n"
"game memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n"
"\n"
"Alternatively, if you experience issues / bugs you can also open github issues:\n"
"\n"
"* For issues with the game engine, please open an\n"
"[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n"
"* For issues about the game's content, please open an\n"
"[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo."
msgstr ""

#: Game.Levels.Multiplication.L05one_mul
msgid "`one_mul m` is the proof `1 * m = m`."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "Concretely: `rw [← succ_eq_add_one] at h`."
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "`succ_eq_add_one n` is the proof that `succ n = n + 1`."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "If $a, b$, $c$ and $d$ are numbers, we have\n"
"$(a + b) + (c + d) = ((a + c) + d) + b.$"
msgstr ""

#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
msgid "You can now `apply mul_left_cancel at h`"
msgstr ""

#: Game.Levels.Implication
msgid "We've proved that $2+2=4$; in Implication World we'll learn\n"
"how to prove $2+2\\neq 5$.\n"
"\n"
"In Addition World we proved *equalities* like $x + y = y + x$.\n"
"In this second tutorial world we'll learn some new tactics,\n"
"enabling us to prove *implications*\n"
"like $x+1=4 \\implies x=3.$\n"
"\n"
"We'll also learn two new fundamental facts about\n"
"natural numbers, which Peano introduced as axioms.\n"
"\n"
"Click on \"Start\" to proceed."
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "mul_left_cancel"
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "Start with `intro h` (remembering that `X ≠ Y` is just notation\n"
"for `X = Y → False`)."
msgstr ""

#: Game.Levels.AdvAddition.L06add_left_eq_zero
msgid "You can just mimic the previous proof to do this one -- or you can figure out a way\n"
"of using it."
msgstr ""

#: Game.Levels.AdvAddition.L03add_left_eq_self
msgid "$x + y = y\\implies x=0.$"
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "For all natural numbers $n$, we have $0 + n = n$."
msgstr ""

#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
msgid "The lemma proved in the final level of this world will be helpful\n"
"in Divisibility World."
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "If the goal is not *exactly* a hypothesis, we can sometimes\n"
"use rewrites to fix things up."
msgstr ""

#: Game.Levels.AdvAddition.L03add_left_eq_self
msgid "`add_left_eq_self x y` is the theorem that $x + y = y \\implies x=0.$"
msgstr ""

#: Game.Levels.Implication.L08ne
msgid "We still can't prove `2 + 2 ≠ 5` because we have not talked about the\n"
"definition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.\n"
"Here `False` is a generic false proposition, and `→` is Lean's notation\n"
"for \"implies\". In logic we learn\n"
"that `True → False` is false, but `False → False` is true. Hence\n"
"`X → False` is the logical opposite of `X`.\n"
"\n"
"Even though `a ≠ b` does not look like an implication,\n"
"you should treat it as an implication. The next two levels will show you how.\n"
"\n"
"`False` is a goal which you cannot deduce from a consistent set of assumptions!\n"
"So if your goal is `False` then you had better hope that your hypotheses\n"
"are contradictory, which they are in this level."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "See if you can take it from here. Look at the new lemmas and tactic\n"
"available on the right."
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid "Here's my solution:\n"
"```\n"
"induction c with d hd\n"
"rw [add_zero, mul_zero, add_zero]\n"
"rfl\n"
"rw [add_succ, mul_succ, hd, mul_succ, add_assoc]\n"
"rfl\n"
"```\n"
"\n"
"Inducting on `a` or `b` also works, but might take longer."
msgstr ""

#: Game.Levels.Implication.L08ne
msgid "Remember that `h2` is a proof of `x = y → False`. Try\n"
"`apply`ing `h2` either `at h1` or directly to the goal."
msgstr ""

#: Game.Levels.Tutorial.L04rw_backwards
msgid "Can you now change the goal into `2 = 2`?"
msgstr ""

#: Game.Levels.Implication
msgid "Implication World"
msgstr ""

#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
msgid "Now `apply h` and you can probably take it from here."
msgstr ""

#: Game.Levels.Multiplication.L05one_mul
msgid "You can prove $1\\times m=m$ in at least three ways.\n"
"Either by induction, or by using `succ_mul`, or\n"
"by using commutativity. Which do you think is quickest?"
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "Use `add_succ`."
msgstr ""

#: Game.Levels.Power.L07mul_pow
msgid "`mul_pow a b n` is a proof that $(ab)^n=a^nb^n.$"
msgstr ""

#: Game.Levels.Addition.L04add_assoc
msgid "`add_assoc a b c` is a proof\n"
"that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\n"
"as `a + b + c`, because the notation for addition is defined to be left\n"
"associative."
msgstr ""

#: Game.Levels.Power.L08pow_pow
msgid "For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$."
msgstr ""

#: Game.Levels.Implication.L06intro
msgid "$x=37\\implies x=37$."
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "[dramatic music]. Now are you ready to face the first boss of the game?"
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "Can you take it from here? (note: if you try `contrapose! h` again, it will\n"
"take you back to where you started!)"
msgstr ""

#: Game.Levels.Tutorial.L01rfl
msgid "If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$"
msgstr ""

#: Game.Levels.Tutorial.L04rw_backwards
msgid "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid ""
"# Statement\n"
"\n"
"If $a$ and $b$ are numbers, then\n"
"`succ_inj a b` is the proof that\n"
"$ (\\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
"\n"
"## More technical details\n"
"\n"
"There are other ways to think about `succ_inj`.\n"
"\n"
"You can think about `succ_inj` itself as a function which takes two\n"
"numbers $$a$$ and $$b$$ as input, and outputs a proof of\n"
"$ ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
"\n"
"You can think of `succ_inj` itself as a proof; it is the proof\n"
"that `succ` is an injective function. In other words,\n"
"`succ_inj` is a proof of\n"
"$\\forall a, b \\in  \\mathbb{N}, ( \\operatorname{succ}(a) = "
"\\operatorname{succ}(b)) \\implies a=b$.\n"
"\n"
"`succ_inj` was postulated as an axiom by Peano, but\n"
"in Lean it can be proved using `pred`, a mathematically\n"
"pathological function."
msgstr ""

#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "`mul_eq_zero a b` is a proof that if `a * b = 0` then `a = 0` or `b = 0`."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "x ≤ y or y ≤ x"
msgstr ""

#: Game.Levels.Implication.L03apply
msgid "Now finish using the `exact` tactic."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "We define a function `is_zero` thus:\n"
"\n"
"```\n"
"is_zero 0 := True\n"
"is_zero (succ n) := False\n"
"```\n"
"\n"
"We also create two lemmas, `is_zero_zero` and `is_zero_succ n`, saying that `is_zero 0 = True`\n"
"and `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`, Peano's\n"
"Last Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have\n"
"this opposite version too, which can be proved in the same way. Note: you can\n"
"cheat here by using `zero_ne_succ` but the point of this world is to show\n"
"you how to *prove* results like that.\n"
"\n"
"If you can turn your goal into `True`, then the `trivial` tactic will solve it."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "You still don't know which way to go, so do `cases «{e}» with a`."
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "`two_eq_succ_one` is a proof of `2 = succ 1`."
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "Start with `cases «{hxy}» with a ha`."
msgstr ""

#: Game.Levels.Multiplication.L02zero_mul
msgid "For all natural numbers $m$, we have $ 0 \\times m = 0$."
msgstr ""

#: Game.Levels.Tutorial.L08twoaddtwo
msgid "$2+2=4$."
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "Now `rw [h]` then `rfl` works, but `exact h` is quicker."
msgstr ""

#: Game.Levels.Tutorial.L06add_zero2
msgid "## Precision rewriting\n"
"\n"
"In the last level, there was `b + 0` and `c + 0`,\n"
"and `rw [add_zero]` changed the first one it saw,\n"
"which was `b + 0`. Let's learn how to tell Lean\n"
"to change `c + 0` first by giving `add_zero` an\n"
"explicit input."
msgstr ""

#: Game.Levels.Implication.L01exact
msgid "The goal in this level is one of our hypotheses. Solve the goal by executing `exact h1`."
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid "You can do induction on any of the three variables. Some choices\n"
"are harder to push through than others. Can you do the inductive step in\n"
"5 rewrites only?"
msgstr ""

#: Game.Levels.Addition.L05add_right_comm
msgid "If $a, b$ and $c$ are arbitrary natural numbers, we have\n"
"$(a + b) + c = (a + c) + b$."
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "You can use `rw [zero_add] at «{h}»` to rewrite at `«{h}»` instead\n"
"of at the goal."
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "## Summary\n"
"\n"
"If `h` is a proof of an equality `X = Y`, then `rw [h]` will change\n"
"all `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;\n"
"get the `⊢` symbol with `\\|-`.)\n"
"\n"
"* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\n"
"until 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"
"\n"
"If you have the assumption `h : x = y + y` and your goal is\n"
"```\n"
"succ (x + 0) = succ (y + y)\n"
"```\n"
"\n"
"then\n"
"\n"
"`rw [add_zero]`\n"
"\n"
"will change the goal into `succ x = succ (y + y)`, and then\n"
"\n"
"`rw [h]`\n"
"\n"
"will change the goal into `succ (y + y) = succ (y + y)`, which\n"
"can be solved with `rfl`.\n"
"\n"
"### Example:\n"
"\n"
"You can use `rw` to change a hypothesis as well.\n"
"For example, if you have two hypotheses\n"
"```\n"
"h1 : x = y + 3\n"
"h2 : 2 * y = x\n"
"```\n"
"then `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`),\n"
"for example if `h` is a function or an implication,\n"
"then `rw` is not the tactic you want to use. For example,\n"
"`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\n"
"not the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n"
"\n"
"## Details\n"
"\n"
"The `rw` tactic is a way to do \\\"substituting in\\\". There\n"
"are two distinct situations where you can use this tactic.\n"
"\n"
"1) Basic usage: if `h : A = B` is an assumption or\n"
"the proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\n"
"will change them all to `B`s. The tactic will error\n"
"if there are no `A`s in the goal.\n"
"\n"
"2) Advanced usage: Assumptions coming from theorem proofs\n"
"often have missing pieces. For example `add_zero`\n"
"is a proof that `? + 0 = ?` because `add_zero` really is a function,\n"
"and `?` is the input. In this situation `rw` will look through the goal\n"
"for any subterm of the form `x + 0`, and the moment it\n"
"finds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n"
"\n"
"Exercise: 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"
"\n"
"If you can't remember the name of the proof of an equality, look it up in\n"
"the list of lemmas on the right.\n"
"\n"
"## Targetted usage\n"
"\n"
"If your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\n"
"to `c + a`, then `rw [add_comm]` will not work because Lean finds another\n"
"addition first and swaps those inputs instead. Use `rw [add_comm a c]` to\n"
"guarantee 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\n"
"that `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n"
"\n"
"If `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\n"
"If you only want to change the 37th occurrence of `X`\n"
"to `Y` then do `nth_rewrite 37 [h]`."
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "Start by unravelling the `1`."
msgstr ""

#: Game.Levels.Algorithm.L03add_algo2
msgid "Let's now make our own tactic to do this."
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "Dealing with `or`"
msgstr ""

#: Game.Levels.AdvAddition.L06add_left_eq_zero
msgid "add_left_eq_zero"
msgstr ""

#: Game
msgid "Natural Number Game"
msgstr ""

#: Game.Levels.Multiplication.L02zero_mul
msgid "Our first challenge is `mul_comm x y : x * y = y * x`,\n"
"and we want to prove it by induction. The zero\n"
"case will need `mul_zero` (which we have)\n"
"and `zero_mul` (which we don't), so let's\n"
"start with this."
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "Here we begin to\n"
"develop an algorithm which, given two naturals `a` and `b`, returns the answer\n"
"to \"does `a = b`?\"\n"
"\n"
"Here is the algorithm. First note that `a` and `b` are numbers, and hence\n"
"are either `0` or successors.\n"
"\n"
"*) If `a` and `b` are both `0`, return \"yes\".\n"
"\n"
"*) If one is `0` and the other is `succ n`, return \"no\".\n"
"\n"
"*) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"\n"
"\n"
"Our job now is to *prove* that this algorithm always gives the correct answer. The proof that\n"
"`0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof\n"
"that `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then\n"
"`succ m = succ n` is `rw [h]` and then `rfl`. This level is a proof of the one\n"
"remaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`."
msgstr ""

#: Game.Levels.Power.L09add_sq
msgid "It's all over! You have proved a theorem which has tripped up\n"
"schoolkids for generations (some of them think $(a+b)^2=a^2+b^2$:\n"
"this is \"the freshman's dream\").\n"
"\n"
"How many rewrites did you use? I can do it in 12.\n"
"\n"
"But wait! This boss is stirring...and mutating into a second more powerful form!"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "Note that you can do `rw [two_eq_succ_one, one_eq_succ_zero]`\n"
"and then `rfl` to solve this level in two lines."
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "The reason `«{x}» ≤ «{x}»` is because `«{x}» = «{x}» + 0`.\n"
"So you should start this proof with `use 0`."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "succ_inj : the successor function is injective"
msgstr ""

#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
msgid "# Summary\n"
"\n"
"The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\n"
"truth tables).\n"
"\n"
"## Details\n"
"\n"
"`tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication,\n"
"it doesn't even know `add_zero`. The only things that `tauto` knows about numbers\n"
"are firstly that `a = a` and secondly that `0 ≠ 1`, `0 ≠ 2`, `1 ≠ 2` and so on.\n"
"What `tauto`'s strength is, is *logic*. If you have a hypothesis `x < 37`\n"
"and another hypothesis `x < 37 → y + z = 42` and your goal is `y + z = 42` then `tauto` will\n"
"solve this goal, because to solve that goal you don't need to know any facts\n"
"about inequalities or addition, all you need to know is the rules of logic.\n"
"\n"
"## Example\n"
"\n"
"If you have `False` as a hypothesis, then `tauto` will solve\n"
"the goal. This is because a false hypothesis implies any hypothesis.\n"
"\n"
"## Example\n"
"\n"
"If your goal is `True`, then `tauto` will solve the goal.\n"
"\n"
"## Example\n"
"\n"
"If you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\n"
"solve the goal because it can prove `False` from your hypotheses, and thus\n"
"prove the goal (as `False` implies anything).\n"
"\n"
"## Example\n"
"\n"
"If 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"
"\n"
"If 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"
"\n"
"If 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.\n"
"If you switch the goal and hypothesis in this example, `tauto` would solve it too."
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "# Summary\n"
"The `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.\n"
"Use it when your hypotheses guarantee that the reason that `P ∨ Q`\n"
"is true is because in fact `P` is true.\n"
"\n"
"Internally this tactic is just `apply`ing a theorem\n"
"saying that $P \\implies P \\lor Q.$\n"
"\n"
"Note that this tactic can turn a solvable goal into an unsolvable\n"
"one."
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "If $x \\leq y$ and $y \\leq z$, then $x \\leq z$."
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "`le_refl x` is a proof of `x ≤ x`.\n"
"\n"
"The reason for the name is that this lemma is \"reflexivity of $\\le$\""
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
msgid "`le_zero x` is a proof of the implication `x ≤ 0 → x = 0`."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "If `a` and `b` are numbers, then `succ_inj a b` is a proof\n"
"that `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*\n"
"tab for more information.\n"
"\n"
"Peano had this theorem as an axiom, but in Algorithm World\n"
"we will show how to prove it in Lean. Right now let's just assume it,\n"
"and let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed\n"
"by manipulating our hypothesis until it becomes the goal. I will\n"
"walk you through this level."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid ""
"In some later worlds, we're going to see some much nastier levels,\n"
"like `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\n"
"Brackets need to be moved around, and variables need to be swapped.\n"
"\n"
"In this level, `(a + b) + (c + d) = ((a + c) + d) + b`,\n"
"let's forget about the brackets and just think about\n"
"the variable order.\n"
"To turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,\n"
"and then swap `b` and `d`. But this is easier than you\n"
"think with `add_left_comm`."
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "You might want to think about whether induction\n"
"on `a` or `b` is the best idea."
msgstr ""

#: Game.Levels.Power.L02zero_pow_succ
msgid "For all numbers $m$, $0 ^{\\operatorname{succ} (m)} = 0$."
msgstr ""

#: Game.Levels.Multiplication.L08add_mul
msgid "Here's my proof:\n"
"```\n"
"rw [mul_comm, mul_add]\n"
"repeat rw [mul_comm c]\n"
"rfl\n"
"```"
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "Start with `intro h` to assume the hypothesis."
msgstr ""

#: Game.Levels.Tutorial.L06add_zero2
msgid "`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.\n"
"You can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You\n"
"can usually stick to `rw [add_zero]` unless you need real precision."
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "Let's see if you can use the tactics we've learnt to prove $x+1=y+1\\implies x=y$.\n"
"Try this one by yourself; if you need help then click on \"Show more help!\"."
msgstr ""

#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
msgid "Start with `intro hb`."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "`le_total x y` is a proof that `x ≤ y` or `y ≤ x`."
msgstr ""

#: GameServer.RpcHandlers
msgid "intermediate goal solved! 🎉"
msgstr ""

#: Game.Levels.Tutorial.L01rfl
msgid "Congratulations! You completed your first verified proof!\n"
"\n"
"Remember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,\n"
"you can click on `rfl` in the list of tactics on the right.\n"
"\n"
"Now click on \"Next\" to learn about the `rw` tactic."
msgstr ""

#: Game.Levels.Power.L05pow_two
msgid "`pow_two a` says that `a ^ 2 = a * a`."
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "First execute `rw [h]` to replace the `y` with `x + 7`."
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "See the new \"*\" tab in your lemmas, containing `mul_zero` and `mul_succ`.\n"
"Right now these are the only facts we know about multiplication.\n"
"Let's prove nine more.\n"
"\n"
"Let's start with a warm-up: no induction needed for this one,\n"
"because we know `1` is a successor."
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "Now you have two goals. Once you proved the first, you will jump to the second one.\n"
"This first goal is the base case $n = 0$.\n"
"\n"
"Recall that you can rewrite the proof of any lemma which is visible\n"
"in your inventory, or of any assumption displayed above the goal,\n"
"as long as it is of the form `X = Y`."
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "In this level, we see inequalities as *hypotheses*. We have not seen this before.\n"
"The `cases` tactic can be used to take `hxy` apart."
msgstr ""

#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
msgid "We want to reduce this to a hypothesis `b = 0` and a goal `a * b = 0`,\n"
"which is logically equivalent but much easier to prove. Remember that `X ≠ 0`\n"
"is notation for `X = 0 → False`. Click on `Show more help!` if you need hints."
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "`ℕ` is the natural numbers, just called \\\"numbers\\\" in this game. It's\n"
"defined via two rules:\n"
"\n"
"* `0 : ℕ` (zero is a number)\n"
"* `succ (n : ℕ) : ℕ` (the successor of a number is a number)\n"
"\n"
"## Game Implementation\n"
"\n"
"*The game uses its own copy of the natural numbers, called `MyNat` with notation `ℕ`.\n"
"It is distinct from the Lean natural numbers `Nat`, which should hopefully\n"
"never leak into the natural number game.*"
msgstr ""

#: Game.Levels.Tutorial.L08twoaddtwo
msgid "Here is an example proof of 2+2=4 showing off various techniques.\n"
"\n"
"```lean\n"
"nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.\n"
"rw [add_succ]\n"
"rw [one_eq_succ_zero]\n"
"rw [add_succ, add_zero] -- two rewrites at once\n"
"rw [← three_eq_succ_two] -- change `succ 2` to `3`\n"
"rw [← four_eq_succ_three]\n"
"rfl\n"
"```\n"
"\n"
"Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\n"
"on the `</>` button in the top right. You can now see your proof\n"
"written as several lines of code. Move your cursor between lines to see\n"
"the goal state at any point. Now cut and paste your code elsewhere if you\n"
"want to save it, and paste the above proof in instead. Move your cursor\n"
"around to investigate. When you've finished, click the `>_` button in the top right to\n"
"move back into \"Typewriter mode\".\n"
"\n"
"You have finished tutorial world!\n"
"Click \"Leave World\" to go back to the\n"
"overworld, and select Addition World, where you will learn\n"
"about the `induction` tactic."
msgstr ""

#: Game.Levels.LessOrEqual.L10le_one
msgid "Here's my proof:\n"
"```\n"
"cases x with y\n"
"left\n"
"rfl\n"
"rw [one_eq_succ_zero] at hx ⊢\n"
"apply succ_le_succ at hx\n"
"apply le_zero at hx\n"
"rw [hx]\n"
"right\n"
"rfl\n"
"```\n"
"\n"
"If you solved this level then you should be fine with the next level!"
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "A passing mathematician remarks that with reflexivity and transitivity out of the way,\n"
"you have proved that `≤` is a *preorder* on `ℕ`."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "Now `cases «{h2}» with e he`."
msgstr ""

#: Game.Levels.Algorithm.L04add_algo3
msgid "Let's now move on to a more efficient approach to questions\n"
"involving numerals, such as `20 + 20 = 40`."
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "## Summary\n"
"\n"
"`repeat t` repeatedly applies the tactic `t`\n"
"to the goal. You don't need to use this\n"
"tactic, 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`\n"
"into the goal\n"
"`a = b`.\n"
"\"\n"
"\n"
"TacticDoc nth_rewrite \"\n"
"## Summary\n"
"\n"
"If `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"
"\n"
"If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\n"
"will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\n"
"will change the goal to `succ 1 + succ 1 = 4`."
msgstr ""

#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "Start with `have h2 := mul_ne_zero a b`."
msgstr ""

#: Game.Levels.Multiplication.L06two_mul
msgid "Here's my solution:\n"
"```\n"
"rw [two_eq_succ_one, succ_mul, one_mul]\n"
"rfl\n"
"```"
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "zero_add"
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
#: Game.Levels.Tutorial.L08twoaddtwo
msgid "Now you can `rw [add_succ]`"
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "## Summary\n"
"\n"
"If `n` is a number, then `cases n with d` will break the goal into two goals,\n"
"one with `n = 0` and the other with `n = succ d`.\n"
"\n"
"If `h` is a proof (for example a hypothesis), then `cases h with...` will break the\n"
"proof up into the pieces used to prove it.\n"
"\n"
"## Example\n"
"\n"
"If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,\n"
"one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This\n"
"corresponds to the mathematical idea that every natural number is either `0`\n"
"or a successor.\n"
"\n"
"## Example\n"
"\n"
"If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal\n"
"into two goals, one with a hypothesis `hp : P` and the other with a\n"
"hypothesis `hq : Q`.\n"
"\n"
"## Example\n"
"\n"
"If `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,\n"
"because there are no ways to make a proof of `False`! And if you have no goals left,\n"
"you have finished the level.\n"
"\n"
"## Example\n"
"\n"
"If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`\n"
"and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is\n"
"`∃ c, b = a + c`."
msgstr ""

#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
msgid "Start with `cases a with d` to do a case split on `a = 0` and `a = succ d`."
msgstr ""

#: Game.Levels.LessOrEqual.L11le_two
msgid "We'll need this lemma to prove that two is prime!\n"
"\n"
"You'll need to know that `∨` is right associative. This means that\n"
"`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`.\n"
"This affects how `left` and `right` work."
msgstr ""

#: Game.Levels.Implication.L08ne
msgid "Remember, `x ≠ y` is *notation* for `x = y → False`."
msgstr ""

#: Game.Levels.Addition
msgid "Welcome to Addition World! In this world we'll learn the `induction` tactic.\n"
"This will enable us to defeat the boss level of this world, namely `x + y = y + x`.\n"
"\n"
"The tactics `rw`, `rfl` and `induction` are the only tactics you'll need to\n"
"beat all the levels in Addition World, Multiplication World, and Power World.\n"
"Power World contains the final boss of the game.\n"
"\n"
"There are plenty more tactics in this game, but you'll only need to know them if you\n"
"want to explore the game further (for example if you decide to 100%\n"
"the game)."
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "mul_one"
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to\n"
"introduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.\n"
"To learn about this result, click on it in the list of lemmas on the right."
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "For all natural numbers $a, b$, we have\n"
"$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$."
msgstr ""

#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
msgid "`eq_succ_of_ne_zero a` is a proof that `a ≠ 0 → ∃ n, a = succ n`."
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "The `use` tactic"
msgstr ""

#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
msgid "Use the previous lemma with `apply eq_succ_of_ne_zero at ha`."
msgstr ""

#: Game.Levels.Implication.L06intro
msgid "## Summary\n"
"\n"
"If the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,\n"
"and change the goal to `Q`. Mathematically, it says that to prove $P \\implies Q$,\n"
"we can assume $P$ and then prove $Q$.\n"
"\n"
"### Example:\n"
"\n"
"If your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1 \\implies x=y$)\n"
"then `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal\n"
"will change to $x=y$."
msgstr ""

#: Game.Levels.Addition.L03add_comm
msgid "add_comm (level boss)"
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "Start with `repeat rw [add_assoc]` to push all the brackets to the right."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "Start with `induction «{y}» with d hd`."
msgstr ""

#: Game.Levels.Algorithm.L03add_algo2
msgid "Solve this level in one line with `simp only [add_left_comm, add_comm]`"
msgstr ""

#: Game.Levels.LessOrEqual.L09succ_le_succ
msgid "If $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ then $x \\leq y$."
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.\n"
"More precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,\n"
"If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.\n"
"\n"
"## A note on associativity\n"
"\n"
"In Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However\n"
"`→` is right associative. This means that `x ≤ y → y ≤ z → x ≤ z` in Lean means\n"
"exactly that `≤` is transitive. This is different to how mathematicians use\n"
"$P \\implies Q \\implies R$; for them, this usually means that $P \\implies Q$\n"
"and $Q \\implies R$."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
#: Game.Levels.Tutorial.L06add_zero2
msgid "$a+(b+0)+(c+0)=a+b+c.$"
msgstr ""

#: Game.Levels.Addition.L04add_assoc
msgid "We've been adding up two numbers; in this level we will add up three.\n"
"\n"
"  What does $x+y+z$ *mean*? It could either mean $(x+y)+z$, or it\n"
"  could mean $x+(y+z)$. In Lean, $x+y+z$ means $(x+y)+z$.\n"
"\n"
"  But why do we care which one it means; $(x+y)+z$ and $x+(y+z)$ are *equal*!\n"
"\n"
"  That's true, but we didn't prove it yet. Let's prove it now by induction."
msgstr ""

#: Game.Levels.Power.L10FLT
msgid "We now have enough to state a mathematically accurate, but slightly\n"
"clunky, version of Fermat's Last Theorem.\n"
"\n"
"Fermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\\not =z^m$.\n"
"If you didn't do inequality world yet then we can't talk about $m \\geq 3$,\n"
"so we have to resort to the hack of using `n + 3` for `m`,\n"
"which guarantees it's big enough. Similarly instead of `x > 0` we\n"
"use `a + 1`.\n"
"\n"
"This level looks superficially like other levels we have seen,\n"
"but the shortest solution known to humans would translate into\n"
"many millions of lines of Lean code. The author of this game,\n"
"Kevin Buzzard, is working on translating the proof by Wiles\n"
"and Taylor into Lean, although this task will take many years.\n"
"\n"
"## CONGRATULATIONS!\n"
"\n"
"You've finished the main quest of the natural number game!\n"
"If you would like to learn more about how to use Lean to\n"
"prove theorems in mathematics, then take a look\n"
"at [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\n"
"an interactive textbook which you can read in your browser,\n"
"and which explains how to work with many more mathematical concepts in Lean."
msgstr ""

#: Game.Levels.Multiplication.L09mul_assoc
msgid "We now have enough to prove that multiplication is associative,\n"
"the boss level of multiplication world. Good luck!"
msgstr ""

#: Game.Levels.AdvAddition.L04add_right_eq_self
msgid ""
"`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n"
"Two ways to do it spring to mind; I'll mention them when you've solved it."
msgstr ""

#: Game.Levels.Power.L08pow_pow
msgid "pow_pow"
msgstr ""

#: Game.Levels.Implication.L03apply
msgid "The `apply` tactic."
msgstr ""

#: Game.Levels.Power.L09add_sq
msgid "For all numbers $a$ and $b$, we have\n"
"$$(a+b)^2=a^2+b^2+2ab.$$"
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "Now finish in one line."
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid ""
"The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` "
"and `b = 0`.\n"
"Let's prove one of these facts in this level, and the other in the next.\n"
"\n"
"## A new tactic: `cases`\n"
"\n"
"The `cases` tactic will split an object or hypothesis up into the possible "
"ways\n"
"that it could have been created.\n"
"\n"
"For example, sometimes you want to deal with the two cases `b = 0` and `b = "
"succ d` separately,\n"
"but don't need the inductive hypothesis `hd` that comes with `induction b "
"with d hd`.\n"
"In this situation you can use `cases b with d` instead. There are two ways "
"to make\n"
"a number: it's either zero or a successor. So you will end up with two "
"goals, one\n"
"with `b = 0` and one with `b = succ d`.\n"
"\n"
"Another example: if you have a hypothesis `h : False` then you are done, "
"because a false statement implies\n"
"any statement. Here `cases h` will close the goal, because there are *no* "
"ways to\n"
"make a proof of `False`! So you will end up with no goals, meaning you have "
"proved everything."
msgstr ""

#: Game
msgid "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\n"
"learning the basics about theorem proving in Lean.\n"
"\n"
"This is a good first introduction to Lean!"
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "The way to start this proof is `induction b with d hd generalizing c`."
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid "Our next goal is \"left and right distributivity\",\n"
"meaning $a(b+c)=ab+ac$ and $(b+c)a=ba+ca$. Rather than\n"
"these slightly pompous names, the name of the proofs\n"
"in Lean are descriptive. Let's start with\n"
"`mul_add a b c`, the proof of `a * (b + c) = a * b + a * c`.\n"
"Note that the left hand side contains a multiplication\n"
"and then an addition."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "## Summary\n"
"\n"
"`repeat t` repeatedly applies the tactic `t`\n"
"to the goal. You don't need to use this\n"
"tactic, 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`\n"
"into the goal\n"
"`a = b`."
msgstr ""

#: Game.Levels.Algorithm.L04add_algo3
msgid "You can make your own tactics in Lean.\n"
"This code here\n"
"```\n"
"macro \"simp_add\" : tactic => `(tactic|(\n"
"  simp only [add_assoc, add_left_comm, add_comm]))\n"
"```\n"
"was used to create a new tactic `simp_add`, which runs\n"
"`simp only [add_assoc, add_left_comm, add_comm]`.\n"
"Try running `simp_add` to solve this level!"
msgstr ""

#: Game.Levels.Power.L06pow_add
msgid "Let's now begin our approach to the final boss,\n"
"by proving some more subtle facts about powers."
msgstr ""

#: Game.Levels.AdvAddition.L06add_left_eq_zero
msgid ""
"How about this for a proof:\n"
"\n"
"```\n"
"rw [add_comm]\n"
"exact add_right_eq_zero b a\n"
"```\n"
"\n"
"That's the end of Advanced Addition World! You'll need these theorems\n"
"for the next world, `≤` World. Click on \"Leave World\" to access it."
msgstr ""

#: Game.Levels.LessOrEqual.L06le_antisymm
msgid "`le_antisymm x y` is a proof that if `x ≤ y` and `y ≤ x` then `x = y`."
msgstr ""

#: Game.Levels.Tutorial.L06add_zero2
msgid "Try `rw [add_zero c]`."
msgstr ""

#: Game.Levels.Algorithm.L01add_left_comm
msgid "If $a, b, c$ are numbers, then $a+(b+c)=b+(a+c)$."
msgstr ""

#: Game.Levels.Implication.L08ne
msgid "≠"
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "You can start a proof by induction on `n` by typing:\n"
"`induction n with d hd`."
msgstr ""

#: Game.Levels.Power.L06pow_add
msgid "For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m  a ^ n$."
msgstr ""

#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
msgid "mul_right_eq_self"
msgstr ""

#: Game.Levels.Multiplication.L08add_mul
msgid "`add_mul` is just as fiddly to prove by induction; but there's a trick\n"
"which avoids it. Can you spot it?"
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "Now `«{ha}»` is a proof that `«{y}» = «{x}» + «{a}»`, and `hxy` has vanished. Similarly, you can destruct\n"
"`«{hyz}»` into its parts with `cases «{hyz}» with b hb`."
msgstr ""

#: Game.Levels.AdvAddition.L03add_left_eq_self
msgid "`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "## The birth of number.\n"
"\n"
"Numbers in Lean are defined by two rules.\n"
"\n"
"* `0` is a number.\n"
"* If `n` is a number, then the *successor* `succ n` of `n` is a number.\n"
"\n"
"The successor of `n` means the number after `n`. Let's learn to\n"
"count, and name a few small numbers.\n"
"\n"
"## Counting to four.\n"
"\n"
"`0` is a number, so `succ 0` is a number. Let's call this new number `1`.\n"
"Similarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.\n"
"This gives us plenty of numbers to be getting along with.\n"
"\n"
"The *proof* that `2 = succ 1` is called `two_eq_succ_one`.\n"
"Check out the \"012\" tab in the list of lemmas on the right\n"
"for this and other proofs.\n"
"\n"
"Let's prove that $2$ is the number after the number after zero."
msgstr ""

#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
msgid "`mul_le_mul_right a b t` is a proof that `a ≤ b → a * t ≤ b * t`."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "Now `rw [add_zero]` will change `c + 0` into `c`."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0`\n"
"which we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\\ne`).\n"
"You'll be asked to\n"
"prove it, and then you'll have a new hypothesis which you can apply\n"
"`le_mul_right` to."
msgstr ""

#: Game.Levels.Power.L08pow_pow
msgid "`pow_pow a m n` is a proof that $(a^m)^n=a^{mn}.$"
msgstr ""

#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
msgid "`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`."
msgstr ""

#: Game.Levels.Implication.L04succ_inj
msgid "And now we've deduced what we wanted to prove: the goal is one of our assumptions.\n"
"Finish the level with `exact h`."
msgstr ""

#: Game.Levels.AdvMultiplication.L10mul_right_eq_self
msgid "A two-line proof is\n"
"\n"
"```\n"
"nth_rewrite 2 [← mul_one a] at h\n"
"exact mul_left_cancel a b 1 ha h\n"
"```\n"
"\n"
"We now have all the tools necessary to set up the basic theory of divisibility of naturals."
msgstr ""

#: Game.Levels.Algorithm.L09decide2
msgid "decide again"
msgstr ""

#: Game.Levels.LessOrEqual.L03le_succ_self
msgid "x ≤ succ x"
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "Can you take it from here? Click on \"Show more help!\" if you need a hint."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "Finally use a targetted `add_comm` to switch `b` and `d`"
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid "mul_add"
msgstr ""

#: Game.Levels.Implication.L04succ_inj
#: Game.Levels.Implication.L05succ_inj2
msgid "If $x+1=4$ then $x=3$."
msgstr ""

#: Game.Levels.LessOrEqual.L06le_antisymm
msgid "If $x \\leq y$ and $y \\leq x$, then $x = y$."
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "In this level the *goal* is $2y=2(x+7)$ but to help us we\n"
"have an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\n"
"your list of assumptions. Lean thinks of `h` as being a secret proof of the\n"
"assumption, rather like `x` is a secret number.\n"
"\n"
"Before we can use `rfl`, we have to \"substitute in for $y$\".\n"
"We do this in Lean by *rewriting* the proof `h`,\n"
"using the `rw` tactic."
msgstr ""

#: Game.Levels.Power.L03pow_one
msgid "`pow_one a` says that `a ^ 1 = a`.\n"
"\n"
"Note that this is not quite true by definition: `a ^ 1` is\n"
"defined to be `a ^ 0 * a` so it's `1 * a`, and to prove\n"
"that this is equal to `a` you need to use induction somewhere."
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "`rw [one_eq_succ_zero]` will do this."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "making life easier"
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "Now for to the second goal. Here you have the induction hypothesis\n"
"`«{hd}» : 0 + «{d}» = «{d}»`, and you need to prove that `0 + succ «{d}» = succ «{d}»`."
msgstr ""

#: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero
msgid "eq_succ_of_ne_zero"
msgstr ""

#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
msgid "Let's warm up with an easy one, which works even if `t = 0`."
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "# Summary\n"
"The `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\n"
"Use it when your hypotheses guarantee that the reason that `P ∨ Q`\n"
"is true is because in fact `Q` is true.\n"
"\n"
"Internally this tactic is just `apply`ing a theorem\n"
"saying that $Q \\implies P \\lor Q.$\n"
"\n"
"Note that this tactic can turn a solvable goal into an unsolvable\n"
"one."
msgstr ""

#: Game.Levels.Multiplication.L02zero_mul
msgid "zero_mul"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "Can you take it from here?"
msgstr ""

#: Game.Levels.Power.L07mul_pow
msgid "mul_pow"
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "If $a \\neq b$ then $\\operatorname{succ}(a) \\neq\\operatorname{succ}(b)$."
msgstr ""

#: Game.Levels.Multiplication.L05one_mul
msgid "one_mul"
msgstr ""

#: Game.Levels.Implication.L06intro
msgid "Start with `intro h` to assume the hypothesis and call its proof `h`."
msgstr ""

#: Game.Levels.Algorithm.L05pred
msgid "pred"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
#: Game.Levels.Tutorial.L04rw_backwards
msgid "$2$ is the number after the number after $0$."
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "In the last level, we manipulated the hypothesis `x + 1 = 4`\n"
"  until it became the goal `x = 3`. In this level we'll manipulate\n"
"  the goal until it becomes our hypothesis! In other words, we\n"
"  will \"argue backwards\". The `apply` tactic can do this too.\n"
"  Again I will walk you through this one (assuming you're in\n"
"  command line mode)."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "`rw [add_zero]` will change `b + 0` into `b`."
msgstr ""

#: Game.Levels.Multiplication.L06two_mul
msgid "For any natural number $m$, we have $ 2 \\times m = m+m$."
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$."
msgstr ""

#: Game.Levels.Tutorial.L02rw
msgid "## Summary\n"
"\n"
"If `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"
"\n"
"If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\n"
"will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\n"
"will change the goal to `succ 1 + succ 1 = 4`."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "# Summary\n"
"\n"
"`trivial` will solve the goal `True`."
msgstr ""

#: Game.Levels.Power.L09add_sq
msgid "[final boss music]"
msgstr ""

#: Game.Levels.Addition.L05add_right_comm
msgid "add_right_comm"
msgstr ""

#: Game.Levels.LessOrEqual
msgid "In this world we define `a ≤ b` and prove standard facts\n"
"about it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"\n"
"\n"
"The definition of `a ≤ b` is \"there exists a number `c`\n"
"such that `b = a + c`. \" So we're going to have to learn\n"
"a tactic to prove \"exists\" theorems, and another one\n"
"to use \"exists\" hypotheses.\n"
"\n"
"Click on \"Start\" to proceed."
msgstr ""

#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
msgid "one_le_of_ne_zero"
msgstr ""

#: Game.Levels.Power.L04one_pow
msgid "one_pow"
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "`succ_ne_zero a` is a proof of `succ a ≠ 0`."
msgstr ""

#: Game.Levels.AdvAddition.L02add_left_cancel
msgid "How about this for a proof:\n"
"```\n"
"repeat rw [add_comm n]\n"
"exact add_right_cancel a b n\n"
"```"
msgstr ""

#: Game.Levels.LessOrEqual.L02zero_le
msgid "0 ≤ x"
msgstr ""

#: Game.Levels.AdvAddition.L04add_right_eq_self
msgid "Here's a proof using `add_left_eq_self`:\n"
"```\n"
"rw [add_comm]\n"
"intro h\n"
"apply add_left_eq_self at h\n"
"exact h\n"
"```\n"
"\n"
"and here's an even shorter one using the same idea:\n"
"```\n"
"rw [add_comm]\n"
"exact add_left_eq_self y x\n"
"```\n"
"\n"
"Alternatively you can just prove it by induction on `x`:\n"
"\n"
"```\n"
"induction x with d hd\n"
"intro h\n"
"rw [zero_add] at h\n"
"exact h\n"
"intro h\n"
"rw [succ_add] at h\n"
"apply succ_inj at h\n"
"apply hd at h\n"
"exact h\n"
"```"
msgstr ""

#: Game.Levels.Multiplication.L01mul_one
msgid "`Mul a b`, with notation `a * b`, is the usual\n"
"  product of natural numbers. Internally it is\n"
"  via two axioms:\n"
"\n"
"  * `mul_zero a : a * 0 = 0`\n"
"\n"
"  * `mul_succ a b : a * succ b = a * b + a`\n"
"\n"
"Other theorems about naturals, such as `zero_mul`,\n"
"are proved by induction from these two basic theorems."
msgstr ""

#: Game.Levels.Addition.L05add_right_comm
msgid "You've now seen all the tactics you need to beat the final boss of the game.\n"
"You can begin the journey towards this boss by entering Multiplication World.\n"
"\n"
"Or you can go off the beaten track and learn some new tactics in Implication\n"
"World. These tactics let you prove more facts about addition, such as\n"
"how to deduce `a = 0` from `x + a = x`.\n"
"\n"
"Click \"Leave World\" and make your choice."
msgstr ""

#: Game.Levels.Multiplication.L08add_mul
msgid "add_mul"
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "Now `cases h2 with h0 h1` and deal with the two\n"
"cases separately."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "`mul_right_eq_one a b` is a proof that `a * b = 1 → a = 1`."
msgstr ""

#: Game.Levels.Addition.L03add_comm
msgid "On the set of natural numbers, addition is commutative.\n"
"In other words, if `a` and `b` are arbitrary natural numbers, then\n"
"$a + b = b + a$."
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
#: Game.Levels.AdvAddition.L01add_right_cancel
msgid "Nice!"
msgstr ""

#: Game.Levels.Tutorial.L06add_zero2
msgid "Let's now learn about Peano's second axiom for addition, `add_succ`."
msgstr ""

#: Game.Levels.LessOrEqual.L09succ_le_succ
msgid ""
"Here's my proof:\n"
"```\n"
"cases hx with d hd\n"
"use d\n"
"rw [succ_add] at hd\n"
"apply succ_inj at hd\n"
"exact hd\n"
"```"
msgstr ""

#: Game.Levels.Multiplication.L09mul_assoc
msgid "`mul_assoc a b c` is a proof that `(a * b) * c = a * (b * c)`.\n"
"\n"
"Note that when Lean says `a * b * c` it means `(a * b) * c`.\n"
"\n"
"Note that `(a * b) * c = a * (b * c)` cannot be proved by \\\"pure thought\\\":\n"
"for example subtraction is not associative, as `(6 - 2) - 1` is not\n"
"equal to `6 - (2 - 1)`."
msgstr ""

#: Game.Levels.Tutorial.L01rfl
msgid "## Summary\n"
"\n"
"`rfl` proves goals of the form `X = X`.\n"
"\n"
"In other words, the `rfl` tactic will close any goal of the\n"
"form `A = B` if `A` and `B` are *identical*.\n"
"\n"
"`rfl` is short for \\\"reflexivity (of equality)\\\".\n"
"\n"
"## Example:\n"
"\n"
"If the goal looks like this:\n"
"\n"
"```\n"
"x + 37 = x + 37\n"
"```\n"
"\n"
"then `rfl` will close it. But if it looks like `0 + x = x` then `rfl` won't work, because even\n"
"though $0+x$ and $x$ are always equal as *numbers*, they are not equal as *terms*.\n"
"The only term which is identical to `0 + x` is `0 + x`.\n"
"\n"
"## Details\n"
"\n"
"`rfl` is short for \\\"reflexivity of equality\\\".\n"
"\n"
"## Game Implementation\n"
"\n"
"*Note that our `rfl` is weaker than the version used in core Lean and `mathlib`,\n"
"for pedagogical purposes; mathematicians do not distinguish between propositional\n"
"and definitional equality because they think about definitions in a different way\n"
"to type theorists (`zero_add` and `add_zero` are both \\\"facts\\\" as far\n"
"as mathematicians are concerned, and who cares what the definition of addition is).*"
msgstr ""

#: Game.Levels.LessOrEqual.L11le_two
msgid "le_two"
msgstr ""

#: Game.Levels.Power.L05pow_two
msgid "pow_two"
msgstr ""

#: Game.Levels.Algorithm.L05pred
msgid "Nice! You've proved `succ_inj`!\n"
"Let's now prove Peano's other axiom, that successors can't be $0$."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "We'd like to prove `2 + 2 = 4` but right now\n"
"we can't even *state* it\n"
"because we haven't yet defined addition.\n"
"\n"
"## Defining addition.\n"
"\n"
"How are we going to add $37$ to an arbitrary number $x$? Well,\n"
"there are only two ways to make numbers in this game: $0$\n"
"and successors. So to define `37 + x` we will need\n"
"to know what `37 + 0` is and what `37 + succ x` is.\n"
"Let's start with adding `0`.\n"
"\n"
"### Adding 0\n"
"\n"
"To make addition agree with our intuition, we should *define* `37 + 0`\n"
"to be `37`. More generally, we should define `a + 0` to be `a` for\n"
"any number `a`. The name of this proof in Lean is `add_zero a`.\n"
"For example `add_zero 37` is a proof of `37 + 0 = 37`,\n"
"`add_zero x` is a proof of `x + 0 = x`, and `add_zero` is a proof\n"
"of `? + 0 = ?`.\n"
"\n"
"We write `add_zero x : x + 0 = x`, so `proof : statement`."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "is_zero"
msgstr ""

#: Game.Levels.Power.L07mul_pow
msgid "The music gets ever more dramatic, as we explore\n"
"the interplay between exponentiation and multiplication.\n"
"\n"
"If you're having trouble exchanging the right `a * b`\n"
"because `rw [mul_comm]` swaps the wrong multiplication,\n"
"then read the documentation of `rw` for tips on how to fix this."
msgstr ""

#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "Now the goal can be deduced from `h2` by pure logic, so use the `tauto`\n"
"tactic."
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "Next turn `1` into `succ 0` with `rw [one_eq_succ_zero]`."
msgstr ""

#: Game.Levels.Implication.L06intro
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."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "`rw [add_comm b d]`."
msgstr ""

#: Game.Levels.Power.L10FLT
msgid "`xyzzy` is an ancient magic spell, believed to be the origin of the\n"
"modern word `sorry`. The game won't complain - or notice - if you\n"
"prove anything with `xyzzy`."
msgstr ""

#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
msgid "The previous lemma can be used to prove this one."
msgstr ""

#: Game.Levels.Tutorial.L01rfl
msgid "# Read this first\n"
"\n"
"Each level in this game involves proving a mathematical theorem (the \"Goal\").\n"
"The goal will be a statement about *numbers*. Some numbers in this game have known values.\n"
"Those numbers have names like $37$. Other numbers will be secret. They're called things\n"
"like $x$ and $q$. We know $x$ is a number, we just don't know which one.\n"
"\n"
"In this first level we're going to prove the theorem that $37x + q = 37x + q$.\n"
"You can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`\n"
"are numbers.\n"
"\n"
"We solve goals in Lean using *Tactics*, and the first tactic we're\n"
"going to learn is called `rfl`, which proves all theorems of the form $X = X$.\n"
"\n"
"Prove that $37x+q=37x+q$ by executing the `rfl` tactic."
msgstr ""

#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "mul_eq_zero"
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "Now change `1` to `succ 0` in `h`."
msgstr ""

#: Game.Levels.AdvMultiplication.L01mul_le_mul_right
msgid "mul_le_mul_right"
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "`Add a b`, with notation `a + b`, is\n"
"the usual sum of natural numbers. Internally it is defined\n"
"via the following two hypotheses:\n"
"\n"
"* `add_zero a : a + 0 = a`\n"
"\n"
"* `add_succ a b : a + succ b = succ (a + b)`\n"
"\n"
"Other theorems about naturals, such as `zero_add a : 0 + a = a`, are proved\n"
"by induction using these two basic theorems.\""
msgstr ""

#: Game.Levels.Implication.L10one_ne_zero
msgid "1 ≠ 0"
msgstr ""

#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "Here's the short proof:\n"
"```\n"
"have h2 := mul_ne_zero a b\n"
"tauto\n"
"```\n"
"This works because, given `mul_ne_zero a b`,\n"
"the argument is reduced to pure logic."
msgstr ""

#: Game.Levels.AdvAddition.L04add_right_eq_self
msgid "add_right_eq_self"
msgstr ""

#: Game.Levels.LessOrEqual.L04le_trans
msgid "x ≤ y and y ≤ z implies x ≤ z"
msgstr ""

#: Game.Levels.LessOrEqual.L03le_succ_self
msgid "If $x$ is a number, then $x \\le \\operatorname{succ}(x)$."
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "Well done! You now have enough tools to tackle the main boss of this level."
msgstr ""

#: Game.Levels.Multiplication.L04mul_comm
msgid "Multiplication is commutative."
msgstr ""

#: Game.Levels.Addition.L03add_comm
msgid "`add_comm x y` is a proof of `x + y = y + x`."
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "Here's a two-line proof:\n"
"```\n"
"repeat rw [zero_add] at h\n"
"exact h\n"
"```"
msgstr ""

#: Game.Levels.AdvAddition.L02add_left_cancel
msgid "`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.\n"
"You can prove it by induction on `n` or you can deduce it from `add_right_cancel`."
msgstr ""

#: Game.Levels.Implication.L08ne
msgid "`a ≠ b` is *notation* for `(a = b) → False`.\n"
"\n"
"The reason this is mathematically\n"
"valid is that if `P` is a true-false statement then `P → False`\n"
"is the logical opposite of `P`. Indeed `True → False` is false,\n"
"and `False → False` is true!\n"
"\n"
"The upshot of this is that you can treat `a ≠ b` in exactly\n"
"the same way as you treat any implication `P → Q`. For example,\n"
"if your *goal* is of the form `a ≠ b` then you can make progress\n"
"with `intro h`, and if you have a hypothesis `h` of the\n"
"form `a ≠ b` then you can `apply h at h1` if `h1` is a proof\n"
"of `a = b`."
msgstr ""

#: Game.Levels.Algorithm.L04add_algo3
msgid "# Overview\n"
"\n"
"Our home-made tactic `simp_add` will solve arbitrary goals of\n"
"the form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`."
msgstr ""

#: Game.Levels.Multiplication.L03succ_mul
msgid "succ_mul"
msgstr ""

#: Game.Levels.Implication.L10one_ne_zero
msgid "$1\\neq0$."
msgstr ""

#: Game.Levels.Implication.L01exact
msgid "In this world we'll learn how to prove theorems of the form $P\\implies Q$.\n"
"In other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\n"
"To do that we need to learn some more tactics.\n"
"\n"
"The `exact` tactic can be used to close a goal which is exactly one of\n"
"the hypotheses. It takes the name of the hypothesis as argument: `exact h`."
msgstr ""

#: Game.Levels.Power.L09add_sq
msgid "`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$"
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "Numbers"
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "Start with `apply succ_inj` to apply `succ_inj` to the *goal*."
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "$x+1=y+1 \\implies x=y$."
msgstr ""

#: Game.Levels.Implication.L03apply
msgid "In this level, the hypotheses `h2` is an *implication*. It says\n"
"that *if* `x = 37` *then* `y = 42`. We can use this\n"
"hypothesis with the `apply` tactic. Remember you can click on\n"
"`apply` or any other tactic on the right to see a detailed explanation\n"
"of what it does, with examples."
msgstr ""

#: Game.Levels.Algorithm.L06is_zero
msgid "We're going to change that `False` into `True`. Start by changing it into\n"
"`is_zero (succ a)` by executing `rw [← is_zero_succ a]`."
msgstr ""

#: Game.Levels.LessOrEqual.L06le_antisymm
msgid "This level asks you to prove *antisymmetry* of $\\leq$.\n"
"In other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.\n"
"It's the trickiest one so far. Good luck!"
msgstr ""

#: Game.Levels.LessOrEqual.L09succ_le_succ
msgid "succ x ≤ succ y → x ≤ y"
msgstr ""

#: Game.Levels.Tutorial.L04rw_backwards
msgid "Why did we not just define `succ n` to be `n + 1`? Because we have not\n"
"even *defined* addition yet! We'll do that in the next level."
msgstr ""

#: Game.Levels.LessOrEqual.L10le_one
msgid "If $x \\leq 1$ then either $x = 0$ or $x = 1$."
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
msgid "`le_zero x` is a proof of `x ≤ 0 → x = 0`."
msgstr ""

#: Game
msgid "The classical introduction game for Lean."
msgstr ""

#: Game.Levels.Power.L10FLT
msgid "Fermat's Last Theorem"
msgstr ""

#: Game.Levels.Implication.L03apply
msgid "If $x=37$ and we know that $x=37\\implies y=42$ then we can deduce $y=42$."
msgstr ""

#: Game.Levels.Multiplication.L03succ_mul
msgid "For all natural numbers $a$ and $b$, we have\n"
"$(\\operatorname{succ}\\ a) \\times b = a\\times b + b$."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid ""
"# Summary\n"
"\n"
"The `have` tactic can be used to add new hypotheses to a level, but of "
"course\n"
"you have to prove them.\n"
"\n"
"\n"
"## Example\n"
"\n"
"The simplest usage is like this. If you have `a` in your context and you "
"execute\n"
"\n"
"`have ha : a = 0`\n"
"\n"
"then you will get a new goal `a = 0` to prove, and after you've proved\n"
"it you will have a new hypothesis `ha : a = 0` in your original goal.\n"
"\n"
"## Example\n"
"\n"
"If you already have a proof of what you want to `have`, you\n"
"can just create it immediately. For example, if you have `a` and `b`\n"
"number objects, then\n"
"\n"
"`have h2 : succ a = succ b → a = b := succ_inj a b`\n"
"\n"
"will directly add a new hypothesis `h2 : succ a = succ b → a = b`\n"
"to the context, because you just supplied the proof of it (`succ_inj a b`).\n"
"\n"
"## Example\n"
"\n"
"If you have a proof to hand, then you don't even need to state what you\n"
"are proving. For example\n"
"\n"
"`have h2 := succ_inj a b`\n"
"\n"
"will add `h2 : succ a = succ b → a = b` as a hypothesis."
msgstr ""

#: Game.Levels.Algorithm
msgid "Proofs like $2+2=4$ and $a+b+c+d+e=e+d+c+b+a$ are very tedious to do by hand.\n"
"In Algorithm World we learn how to get the computer to do them for us.\n"
"\n"
"Click on \"Start\" to proceed."
msgstr ""

#: Game.Levels.Power.L09add_sq
msgid "add_sq"
msgstr ""

#: Game.Levels.Power.L04one_pow
msgid "`one_pow n` is a proof that $1^n=1$."
msgstr ""

#: Game.Levels.LessOrEqual.L05le_zero
msgid "It's \"intuitively obvious\" that there are no numbers less than zero,\n"
"but to prove it you will need a result which you showed in advanced\n"
"addition world."
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "Here's a completely backwards proof:\n"
"```\n"
"intro h\n"
"apply succ_inj\n"
"repeat rw [succ_eq_add_one]\n"
"exact h\n"
"```"
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "`add_zero a` is a proof that `a + 0 = a`.\n"
"\n"
"## Summary\n"
"\n"
"`add_zero` is really a function, which\n"
"eats a number, and returns a proof of a theorem\n"
"about that number. For example `add_zero 37` is\n"
"a proof that `37 + 0 = 37`.\n"
"\n"
"The `rw` tactic will accept `rw [add_zero]`\n"
"and will try to figure out which number you omitted\n"
"to input.\n"
"\n"
"## Details\n"
"\n"
"A mathematician sometimes thinks of `add_zero`\n"
"as \\\"one thing\\\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.\n"
"This is just another way of saying that it's a function which\n"
"can eat any number n and will return a proof that `n + 0 = n`."
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\n"
"means \"there exists\". So `a ≤ b` means that there exists\n"
"a number `c` such that `b = a + c`. This definition works\n"
"because there are no negative numbers in this game.\n"
"\n"
"To *prove* an \"exists\" statement, use the `use` tactic.\n"
"Let's see an example."
msgstr ""

#: Game.Levels.LessOrEqual
msgid "≤ World"
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "And now `rw [add_zero]`"
msgstr ""

#: Game.Levels.Tutorial.L08twoaddtwo
msgid "Good luck!\n"
"\n"
"  One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.\n"
"  If you only want to change one of them, say the 3rd one, then use\n"
"  `nth_rewrite 3 [h]`."
msgstr ""

#: Game.Levels.AdvMultiplication.L05le_mul_right
msgid "`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.\n"
"\n"
"It's one way of saying that a divisor of a positive number\n"
"has to be at most that number."
msgstr ""

#: Game.Levels.Addition.L04add_assoc
msgid "Remember that when Lean writes `a + b + c`, it means `(a + b) + c`.\n"
"If you are not sure where the brackets are in an expression, just hover\n"
"your cursor over it and look at what gets highlighted. For example,\n"
"hover over both `+` symbols on the left hand side of the goal and\n"
"you'll see where the invisible brackets are."
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "`exact` practice."
msgstr ""

#: Game.Levels.Algorithm.L01add_left_comm
msgid "`add_left_comm a b c` is a proof that `a + (b + c) = b + (a + c)`."
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "An algorithm for equality"
msgstr ""

#: Game.Levels.LessOrEqual.L11le_two
msgid "`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`."
msgstr ""

#: Game.Levels.Addition.L02succ_add
msgid "`succ_add a b` is a proof that `succ a + b = succ (a + b)`."
msgstr ""

#: Game.Levels.AdvMultiplication.L05le_mul_right
msgid "le_mul_right"
msgstr ""

#: Game.Levels.Power
msgid "Power World"
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "$0\\neq1$."
msgstr ""

#: Game.Levels.AdvAddition.L03add_left_eq_self
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"
"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"
"```\n"
"nth_rewrite 2 [← zero_add y]\n"
"exact add_right_cancel x 0 y\n"
"```"
msgstr ""

#: Game.Levels.Multiplication.L06two_mul
msgid "two_mul"
msgstr ""

#: Game.Levels.Algorithm.L04add_algo3
msgid "the simplest approach"
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "If $a+b=0$ then $a=0$."
msgstr ""

#: Game.Levels.LessOrEqual.L08le_total
msgid "This is I think the toughest level yet. Tips: if `a` is a number\n"
"then `cases a with b` will split into cases `a = 0` and `a = succ b`.\n"
"And don't go left or right until your hypotheses guarantee that\n"
"you can prove the resulting goal!\n"
"\n"
"I've left hidden hints; if you need them, retry from the beginning\n"
"and click on \"Show more help!\""
msgstr ""

#: Game.Levels.AdvMultiplication.L02mul_left_ne_zero
msgid "`mul_left_ne_zero a b` is a proof that `a * b ≠ 0 → b ≠ 0`."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "So that's the algorithm: now let's use automation to perform it\n"
"automatically."
msgstr ""

#: Game.Levels.LessOrEqual.L09succ_le_succ
msgid "`succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`."
msgstr ""

#: Game.Levels.Implication.L09zero_ne_succ
msgid "`zero_ne_one` is a proof of `0 ≠ 1`."
msgstr ""

#: Game.Levels.AdvMultiplication.L09mul_left_cancel
msgid "The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\".\n"
"You can `apply` it `at` any hypothesis of the form `a * d = a * ?`. "
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$."
msgstr ""

#: Game.Levels.LessOrEqual.L02zero_le
msgid "`zero_le x` is a proof that `0 ≤ x`."
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "Well done!"
msgstr ""

#: Game.Levels.Tutorial.L06add_zero2
msgid "Precision rewriting"
msgstr ""

#: Game.Levels.Implication.L02exact2
msgid "Assuming $0+x=(0+y)+2$, we have $x=y+2$."
msgstr ""

#: Game.Levels.Multiplication.L06two_mul
msgid "This level is more important than you think; it plays\n"
"a useful role when battling a big boss later on."
msgstr ""

#: Game.Levels.Multiplication.L05one_mul
msgid "For any natural number $m$, we have $ 1 \\times m = m$."
msgstr ""

#: Game.Levels.Power.L08pow_pow
msgid "The music dies down. Is that it?\n"
"\n"
"Course it isn't, you can\n"
"clearly see that there are two levels left.\n"
"\n"
"A passing mathematician says that mathematicians don't have a name\n"
"for the structure you just constructed. You feel cheated.\n"
"\n"
"Suddenly the music starts up again. This really is the final boss."
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "We don't know whether to go left or right yet. So start with `cases «{h}» with hx hy`."
msgstr ""

#: Game.Levels.AdvAddition.L01add_right_cancel
msgid "In this world I will mostly leave you on your own.\n"
"\n"
"`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$."
msgstr ""

#: Game.Levels.Tutorial
msgid "Tutorial World"
msgstr ""

#: Game.Levels.AdvAddition.L01add_right_cancel
msgid "$a+n=b+n\\implies a=b$."
msgstr ""

#: Game.Levels.Addition.L04add_assoc
msgid "On the set of natural numbers, addition is associative.\n"
"In other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n"
"$ (a + b) + c = a + (b + c). $"
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "Totality of `≤` is the boss level of this world, and it's coming up next. It says that\n"
"if `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.\n"
"But we haven't talked about `or` at all. Here's a run-through.\n"
"\n"
"1) The notation for \"or\" is `∨`. You won't need to type it, but you can\n"
"type it with `\\or`.\n"
"\n"
"2) If you have an \"or\" statement in the *goal*, then two tactics made\n"
"progress: `left` and `right`. But don't choose a direction unless your\n"
"hypotheses guarantee that it's the correct one.\n"
"\n"
"3) If you have an \"or\" statement as a *hypothesis* `h`, then\n"
"`cases h with h1 h2` will create two goals, one where you went left,\n"
"and the other where you went right."
msgstr ""

#: Game.Levels.AdvMultiplication
msgid "Advanced Multiplication World"
msgstr ""

#: Game.Levels.AdvMultiplication.L08mul_eq_zero
msgid "This level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is\n"
"logically equivalent to the last level, so there is a very short proof."
msgstr ""

#: GameServer.RpcHandlers
msgid "level completed! 🎉"
msgstr ""

#: Game.Levels.Multiplication.L02zero_mul
msgid "`zero_mul x` is the proof that `0 * x = 0`.\n"
"\n"
"Note: `zero_mul` is a `simp` lemma."
msgstr ""

#: Game
msgid ""
"# Welcome to the Natural Number Game\n"
"#### An introduction to mathematical proof.\n"
"\n"
"In this game, we will build the basic theory of the natural\n"
"numbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\n"
"that `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\n"
"And at the end we'll see if we can prove Fermat's Last Theorem.\n"
"We'll do this by solving levels of a computer puzzle game called Lean.\n"
"\n"
"# Read this.\n"
"\n"
"Learning how to use an interactive theorem prover takes time.\n"
"Tests show that the people who get the most out of this game are\n"
"those who read the help texts like this one.\n"
"\n"
"To start, click on \"Tutorial World\".\n"
"\n"
"Note: this is a new Lean 4 version of the game containing several\n"
"worlds which were not present in the old Lean 3 version. More new worlds\n"
"such as Strong Induction World, Even/Odd World and Prime Number World\n"
"are in development; if you want to see their state or even help out, "
"checkout\n"
"out the [issues in the github repo](https://github.com/leanprover-community/"
"NNG4/issues).\n"
"\n"
"## More\n"
"\n"
"Click on the three lines in the top right and select \"Game Info\" for "
"resources,\n"
"links, and ways to interact with the Lean community."
msgstr ""

#: Game.Levels.Power.L05pow_two
msgid "For all naturals $a$, $a ^ 2 = a \\times a$."
msgstr ""

#: Game.Levels.Tutorial.L08twoaddtwo
msgid "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`."
msgstr ""

#: Game.Levels.Implication.L07intro2
msgid "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\n"
"change `h` to `succ x = succ y`."
msgstr ""

#: Game.Levels.LessOrEqual.L02zero_le
msgid "To solve this level, you need to `use` a number `c` such that `x = 0 + c`."
msgstr ""

#: Game.Levels.LessOrEqual.L01le_refl
msgid "`a ≤ b` is *notation* for `∃ c, b = a + c`.\n"
"\n"
"Because this game doesn't have negative numbers, this definition\n"
"is mathematically valid.\n"
"\n"
"This means that if you have a goal of the form `a ≤ b` you can\n"
"make 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`."
msgstr ""

#: Game.Levels.Tutorial.L03two_eq_ss0
msgid "`three_eq_succ_two` is a proof of `3 = succ 2`."
msgstr ""

#: Game.Levels.Algorithm.L02add_algo1
msgid "Now use `rw [add_left_comm b c]` to switch `b` and `c` on the left\n"
"hand side."
msgstr ""

#: Game.Levels.Power.L07mul_pow
msgid "For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$."
msgstr ""

#: Game.Levels.Multiplication.L05one_mul
msgid "Here's my solution:\n"
"```\n"
"rw [mul_comm, mul_one]\n"
"rfl\n"
"```"
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "add_succ"
msgstr ""

#: Game.Levels.Addition.L01zero_add
msgid "At this point you see the term `0 + «{d}»`, so you can use the\n"
"induction hypothesis with `rw [«{hd}»]`."
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "# Summary\n"
"\n"
"If you have a hypothesis\n"
"\n"
"`h : a ≠ b`\n"
"\n"
"and goal\n"
"\n"
"`c ≠ d`\n"
"\n"
"then `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\n"
"a hypothesis\n"
"\n"
"`h : c = d`\n"
"\n"
"and goal\n"
"\n"
"`a = b`."
msgstr ""

#: Game.Levels.Power.L03pow_one
msgid "pow_one"
msgstr ""

#: Game.Levels.AdvMultiplication.L07mul_ne_zero
msgid "This level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy\n"
"is to write both `a` and `b` as `succ` of something, deduce that `a * b` is\n"
"also `succ` of something, and then `apply zero_ne_succ`."
msgstr ""

#: Game.Levels.Implication.L01exact
msgid "## Summary\n"
"\n"
"If the goal is a statement `P`, then `exact h` will close the goal if `h` is a proof of `P`.\n"
"\n"
"### Example\n"
"\n"
"If the goal is `x = 37` and you have a hypothesis `h : x = 37`\n"
"then `exact h` will solve the goal.\n"
"\n"
"### Example\n"
"\n"
"If the goal is `x + 0 = x` then `exact add_zero x` will close the goal.\n"
"\n"
"### Exact needs to be exactly right\n"
"\n"
"Note that `exact add_zero` will *not work* in the previous example;\n"
"for `exact h` to work, `h` has to be *exactly* a proof of the goal.\n"
"`add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,\n"
"a proof of `? + 0 = ?` where `?` needs to be supplied by the user.\n"
"This is in contrast to `rw` and `apply`, which will \\\"guess the inputs\\\"\n"
"if necessary. If the goal is `x + 0 = x` then `rw [add_zero]`\n"
"and `rw [add_zero x]` will both change the goal to `x = x`,\n"
"because `rw` guesses the input to the function `add_zero`."
msgstr ""

#: Game.Levels.Implication.L06intro
msgid "Now `exact h` finishes the job."
msgstr ""

#: Game.Levels.AdvAddition.L05add_right_eq_zero
msgid "add_right_eq_zero"
msgstr ""

#: Game.Levels.Power.L04one_pow
msgid "For all naturals $m$, $1 ^ m = 1$."
msgstr ""

#: Game.Levels.Tutorial.L05add_zero
msgid "Adding zero"
msgstr ""

#: Game.Levels.Addition.L05add_right_comm
msgid "`add_comm b c` is a proof that `b + c = c + b`. But if your goal\n"
"is `a + b + c = a + c + b` then `rw [add_comm b c]` will not\n"
"work! Because the goal means `(a + b) + c = (a + c) + b` so there\n"
"is no `b + c` term *directly* in the goal.\n"
"\n"
"Use associativity and commutativity to prove `add_right_comm`.\n"
"You don't need induction. `add_assoc` moves brackets around,\n"
"and `add_comm` moves variables around.\n"
"\n"
"Remember that you can do more targetted rewrites by\n"
"adding explicit variables as inputs to theorems. For example `rw [add_comm b]`\n"
"will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\n"
"will only do rewrites of the form `b + c = c + b`."
msgstr ""

#: Game.Levels.Algorithm.L07succ_ne_succ
msgid "Start with `contrapose! h`, to change the goal into its\n"
"contrapositive, namely a hypothesis of `succ m = succ n` and a goal of `m = n`."
msgstr ""

#: Game.Levels.Addition.L03add_comm
msgid "[boss battle music]\n"
"\n"
"Look in your inventory to see the proofs you have available.\n"
"These should be enough."
msgstr ""

#: Game.Levels.LessOrEqual.L03le_succ_self
msgid "Here's a two-liner:\n"
"```\n"
"use 1\n"
"exact succ_eq_add_one x\n"
"```\n"
"\n"
"This works because `succ_eq_add_one x` is a proof of `succ x = x + 1`."
msgstr ""

#: Game.Levels.Multiplication.L07mul_add
msgid "Multiplication is distributive over addition on the left.\n"
"In other words, for all natural numbers $a$, $b$ and $c$, we have\n"
"$a(b + c) = ab + ac$."
msgstr ""

#: Game.Levels.AdvMultiplication.L06mul_right_eq_one
msgid "Now you can `apply le_mul_right at h2`."
msgstr ""

#: Game.Levels.Power.L02zero_pow_succ
msgid "zero_pow_succ"
msgstr ""

#: Game.Levels.LessOrEqual.L07or_symm
msgid "Ready for the boss level of this world?"
msgstr ""

#: Game.Levels.Tutorial.L07add_succ
msgid "And finally `rfl`."
msgstr ""

#: Game.Levels.Implication.L05succ_inj2
msgid "You can now finish with `exact h`."
msgstr ""

#: Game.Levels.Algorithm
msgid "Algorithm World"
msgstr ""

#: Game.Levels.Power.L10FLT
msgid "Congratulations! You have proved Fermat's Last Theorem!\n"
"\n"
"Either that, or you used magic..."
msgstr ""

#: Game.Levels.Tutorial.L04rw_backwards
msgid "rewriting backwards"
msgstr ""

#: Game.Levels.Multiplication.L08add_mul
msgid "`add_mul a b c` is a proof that $(a+b)c=ac+bc$."
msgstr ""

#: Game.Levels.Algorithm.L05pred
msgid "Start with `rw [← pred_succ a]` and take it from there."
msgstr ""