fix escaped backspaces

.i18n/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.6.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Thu Feb 29 17:11:36 2024\n"
+"POT-Creation-Date: Mon Mar 11 19:04:55 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -426,7 +426,7 @@ msgid "`add_zero a` is a proof that `a + 0 = a`.\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"
+"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 ""
@@ -1651,7 +1651,7 @@ 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"
+"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"
@@ -1716,20 +1716,20 @@ 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"
+"$ (\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"
+"$ ( \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"
+"$\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"
@@ -1831,12 +1831,12 @@ msgstr ""
 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"
+"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"
+"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 ""
@@ -1872,7 +1872,7 @@ msgid " Let's see if you can use the tactics we've learnt to prove $x+1=y+1\impl
 msgstr ""
 
 #: Game.Levels.Implication.L07intro2
-msgid "$x+1=y+1\implies x=y$."
+msgid "$x+1=y+1 \implies x=y$."
 msgstr ""
 
 #: Game.Levels.Implication.L07intro2
@@ -2521,7 +2521,7 @@ msgid "add_right_cancel"
 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.$"
+msgid "`add_right_cancel a b n` is the theorem that $a+n=b+n \implies a=b.$"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L01add_right_cancel
@@ -2548,7 +2548,7 @@ msgid "add_left_cancel"
 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.$"
+msgid "`add_left_cancel a b n` is the theorem that $n+a=n+b \implies a=b.$"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L02add_left_cancel
@@ -2575,7 +2575,7 @@ msgid "add_left_eq_self"
 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.$"
+msgid "`add_left_eq_self x y` is the theorem that $x + y = y \implies x=0.$"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L03add_left_eq_self
@@ -2608,7 +2608,7 @@ msgid "add_right_eq_self"
 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.$"
+msgid "`add_right_eq_self x y` is the theorem that $x + y = x \implies y=0.$"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L04add_right_eq_self
@@ -2716,7 +2716,7 @@ msgid "## Summary\n"
 msgstr ""
 
 #: Game.Levels.AdvAddition.L05add_right_eq_zero
-msgid "A proof that $a+b=0 \\implies a=0$."
+msgid "A proof that $a+b=0 \implies a=0$."
 msgstr ""
 
 #: Game.Levels.AdvAddition.L05add_right_eq_zero
@@ -2743,7 +2743,7 @@ msgid "You can just mimic the previous proof to do this one -- or you can figure
 msgstr ""
 
 #: Game.Levels.AdvAddition.L06add_left_eq_zero
-msgid "A proof that $a+b=0 \\implies b=0$."
+msgid "A proof that $a+b=0 \implies b=0$."
 msgstr ""
 
 #: Game.Levels.AdvAddition.L06add_left_eq_zero
@@ -2820,7 +2820,7 @@ 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$\""
+"The reason for the name is that this lemma is "reflexivity of $\le$""
 msgstr ""
 
 #: Game.Levels.LessOrEqual.L01le_refl
@@ -2890,15 +2890,15 @@ 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"
+"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$."
+"$P \implies Q \implies R$; for them, this usually means that $P \implies Q$\n"
+"and $Q \implies R$."
 msgstr ""
 
 #: Game.Levels.LessOrEqual.L04le_trans
@@ -3016,7 +3016,7 @@ msgid "# Summary\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"
+"saying that $P \implies P \lor Q.$\n"
 "\n"
 "Note that this tactic can turn a solvable goal into an unsolvable\n"
 "one."
@@ -3029,7 +3029,7 @@ msgid "# Summary\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"
+"saying that $Q \implies P \lor Q.$\n"
 "\n"
 "Note that this tactic can turn a solvable goal into an unsolvable\n"
 "one."

Game/Levels/AdvAddition/L01add_right_cancel.lean

@@ -9,7 +9,7 @@ namespace MyNat
 
 TheoremTab "+"
 
-/-- `add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$ -/
+/-- `add_right_cancel a b n` is the theorem that $a+n=b+n \implies a=b.$ -/
 TheoremDoc MyNat.add_right_cancel as "add_right_cancel" in "+"
 
 Introduction

Game/Levels/AdvAddition/L02add_left_cancel.lean

@@ -8,7 +8,7 @@ namespace MyNat
 
 TheoremTab "+"
 
-/-- `add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$ -/
+/-- `add_left_cancel a b n` is the theorem that $n+a=n+b \implies a=b.$ -/
 TheoremDoc MyNat.add_left_cancel as "add_left_cancel" in "+"
 
 Introduction

Game/Levels/AdvAddition/L03add_left_eq_self.lean

@@ -8,7 +8,7 @@ namespace MyNat
 
 TheoremTab "+"
 
-/-- `add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$ -/
+/-- `add_left_eq_self x y` is the theorem that $x + y = y \implies x=0.$ -/
 TheoremDoc MyNat.add_left_eq_self as "add_left_eq_self" in "+"
 
 Introduction

Game/Levels/AdvAddition/L04add_right_eq_self.lean

@@ -8,7 +8,7 @@ TheoremTab "+"
 
 namespace MyNat
 
-/-- `add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$ -/
+/-- `add_right_eq_self x y` is the theorem that $x + y = x \implies y=0.$ -/
 TheoremDoc MyNat.add_right_eq_self as "add_right_eq_self" in "+"
 
 Introduction

Game/Levels/AdvAddition/L05add_right_eq_zero.lean

@@ -68,7 +68,7 @@ TacticDoc cases
 
 NewTactic cases
 
-/--  A proof that $a+b=0 \\implies a=0$. -/
+/--  A proof that $a+b=0 \implies a=0$. -/
 TheoremDoc MyNat.add_right_eq_zero as "add_right_eq_zero" in "+"
 
 -- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?

Game/Levels/AdvAddition/L06add_left_eq_zero.lean

@@ -13,7 +13,7 @@ Introduction
 of using it.
 "
 
-/--  A proof that $a+b=0 \\implies b=0$. -/
+/--  A proof that $a+b=0 \implies b=0$. -/
 TheoremDoc MyNat.add_left_eq_zero as "add_left_eq_zero" in "+"
 
 /-- If $a+b=0$ then $b=0$. -/

Game/Levels/Implication/L03apply.lean

@@ -11,7 +11,7 @@ TheoremTab "Peano"
 /--
 ## Summary
 
-If `t : P → Q` is a proof that $P\\implies Q$, and `h : P` is a proof of `P`,
+If `t : P → Q` is a proof that $P \implies Q$, and `h : P` is a proof of `P`,
 then `apply t at h` will change `h` to a proof of `Q`. The idea is that if
 you know `P` is true, then you can deduce from `t` that `Q` is true.
 

Game/Levels/Implication/L04succ_inj.lean

@@ -26,20 +26,20 @@ walk you through this level.
 
 If $a$ and $b$ are numbers, then
 `succ_inj a b` is the proof that
-$ (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b$.
+$ (\operatorname{succ}(a) = \operatorname{succ}(b)) \implies a=b$.
 
 ## More technical details
 
 There are other ways to think about `succ_inj`.
 
 You can think about `succ_inj` itself as a function which takes two
 numbers $$a$$ and $$b$$ as input, and outputs a proof of
-$ (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b$.
+$ ( \operatorname{succ}(a) = \operatorname{succ}(b)) \implies a=b$.
 
 You can think of `succ_inj` itself as a proof; it is the proof
 that `succ` is an injective function. In other words,
 `succ_inj` is a proof of
-$\\forall a, b\\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b$.
+$\forall a, b \in  \mathbb{N}, ( \operatorname{succ}(a) = \operatorname{succ}(b)) \implies a=b$.
 
 `succ_inj` was postulated as an axiom by Peano, but
 in Lean it can be proved using `pred`, a mathematically

Game/Levels/Implication/L06intro.lean

@@ -10,12 +10,12 @@ namespace MyNat
 ## Summary
 
 If the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,
-and change the goal to `Q`. Mathematically, it says that to prove $P\\implies Q$,
+and change the goal to `Q`. Mathematically, it says that to prove $P \implies Q$,
 we can assume $P$ and then prove $Q$.
 
 ### Example:
 
-If your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1\\implies x=y$)
+If your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1 \implies x=y$)
 then `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal
 will change to $x=y$.
 -/

Game/Levels/Implication/L07intro2.lean

@@ -11,7 +11,7 @@ Introduction
 Try this one by yourself; if you need help then click on \"Show more help!\".
 "
 
-/-- $x+1=y+1\implies x=y$. -/
+/-- $x+1=y+1 \implies x=y$. -/
 Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
   Hint (hidden := true) "Start with `intro h` to assume the hypothesis."
   intro h

Game/Levels/LessOrEqual/L01le_refl.lean

@@ -52,7 +52,7 @@ Let's see an example.
 /--
 `le_refl x` is a proof of `x ≤ x`.
 
-The reason for the name is that this lemma is \"reflexivity of $\\le$\"
+The reason for the name is that this lemma is "reflexivity of $\le$"
 -/
 TheoremDoc MyNat.le_refl as "le_refl" in "≤"
 

Game/Levels/LessOrEqual/L04le_trans.lean

@@ -11,15 +11,15 @@ namespace MyNat
 /--
 `le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.
 More precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,
-If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.
+If $x \le y$ then (pause) if $y \le z$ then $x \le z$.
 
 ## A note on associativity
 
 In Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However
 `→` is right associative. This means that `x ≤ y → y ≤ z → x ≤ z` in Lean means
 exactly that `≤` is transitive. This is different to how mathematicians use
-$P\\implies Q\\implies R$; for them, this usually means that $P\\implies Q$
-and $Q\\implies R$.
+$P \implies Q \implies R$; for them, this usually means that $P \implies Q$
+and $Q \implies R$.
 -/
 TheoremDoc MyNat.le_trans as "le_trans" in "≤"
 

Game/Levels/LessOrEqual/L07or_symm.lean

@@ -15,7 +15,7 @@ Use it when your hypotheses guarantee that the reason that `P ∨ Q`
 is true is because in fact `P` is true.
 
 Internally this tactic is just `apply`ing a theorem
-saying that $P\\implies P\\lor Q.$
+saying that $P \implies P \lor Q.$
 
 Note that this tactic can turn a solvable goal into an unsolvable
 one.
@@ -29,7 +29,7 @@ Use it when your hypotheses guarantee that the reason that `P ∨ Q`
 is true is because in fact `Q` is true.
 
 Internally this tactic is just `apply`ing a theorem
-saying that $Q\\implies P\\lor Q.$
+saying that $Q \implies P \lor Q.$
 
 Note that this tactic can turn a solvable goal into an unsolvable
 one.

Game/Levels/LessOrEqual/Level_1.lean

@@ -35,7 +35,7 @@ before it and comment it out. See that the proof still compiles.
 
 axiom TMP.add_comm (a b : ℕ) : a + b = b + a
 
-/-- If $x$ is a natural number, then $x\\le 1+x$.
+/-- If $x$ is a natural number, then $x \le 1+x$.
  -/
 Statement --one_add_le_self
     (x : ℕ) : x ≤ 1 + x := by

Game/Levels/LessOrEqual/Level_2.lean

@@ -14,8 +14,8 @@ Introduction
 Here's a nice easy one.
 "
 
-/-- The $\\le$ relation is reflexive. In other words, if $x$ is a natural number,
-then $x\\le x$. -/
+/-- The $\le$ relation is reflexive. In other words, if $x$ is a natural number,
+then $x \le x$. -/
 Statement
     (x : ℕ) : x ≤ x := by
   use 0

Game/Levels/LessOrEqual/Level_3.lean

@@ -42,7 +42,7 @@ Now use `use` wisely and you're home.
 
 "
 
-/-- For all naturals $a$, $b$, if $a\\leq b$ then $a\\leq \\operatorname{succ}(b)$.
+/-- For all naturals $a$, $b$, if $a \leq b$ then $a \leq  \operatorname{succ}(b)$.
  -/
 Statement
     (a b : ℕ) : a ≤ b → a ≤ (succ b) := by

Game/Levels/OldAdvMultiplication/Level_4.lean

@@ -54,7 +54,7 @@ to be impossible (judging by the comments I've had about it!)
 -- generalizing b` as the first line of the proof.
 
 
-/-- If $a \\neq 0$, $b$ and $c$ are natural numbers such that
+/-- If $a \neq 0$, $b$ and $c$ are natural numbers such that
 $ ab = ac, $
 then $b = c$. -/
 Statement MyNat.mul_left_cancel

Game/Levels/OldAdvProposition/Level_1.lean

@@ -15,7 +15,7 @@ $P\\land Q$ is the proposition \"$P$ and $Q$\".
 "
 namespace MySet
 
-/-- If $P$ and $Q$ are true, then $P\\land Q$ is true. -/
+/-- If $P$ and $Q$ are true, then $P \land Q$ is true. -/
 Statement
     (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
   Hint "If your *goal* is `P ∧ Q` then

Game/Levels/OldAdvProposition/Level_10.lean

@@ -18,7 +18,7 @@ constructive logic).
 "
 
 /-- If $P$ and $Q$ are true/false statements, then
-$$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$
+$$(\lnot Q \implies \lnot P) \implies(P \implies Q).$$
  -/
 Statement
     (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by

Game/Levels/OldAdvProposition/Level_2.lean

@@ -15,7 +15,7 @@ But what if `P ∧ Q` is a hypothesis? In this case, the `rcases` tactic will en
 us to extract proofs of `P` and `Q` from this hypothesis.
 "
 
-/-- If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. -/
+/-- If $P$ and $Q$ are true/false statements, then $P \land Q \implies Q \land P$. -/
 Statement -- and_symm
     (P Q : Prop) : P ∧ Q → Q ∧ P :=  by
   Hint "The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,