Merge pull request #1 from he7d3r/fix-typos

Improve spelling across game

Author: ZRTMRH

.i18n/en/Game.pot

@@ -161,7 +161,7 @@ msgid "You have now completed Vector Space World! The theorems proven here will
 msgstr ""
 
 #: Game.Levels.LinearIndependenceSpanWorld.Level01
-msgid "`Finset.sum` is how we difine summing over a set. It uses Mathlib's `Finset` Type, which means that we\n"
+msgid "`Finset.sum` is how we define summing over a set. It uses Mathlib's `Finset` Type, which means that we\n"
 "can only sum over arbitrary finite sets. The syntax is as follows: With a additive group or field `K`, some Type `T`,\n"
 "some `s : Finset T`, and some `f : T → K`, `Finset.sum s (fun x => f x)` sums `f x` over all `x ∈ s`."
 msgstr ""
@@ -958,7 +958,7 @@ msgstr ""
 #: Game.Levels.InnerProductWorld.Level06
 msgid "One of the most important theorems in linear algebra is orthogonal decomposition. This allows you to\n"
 "represent a vector as a scalar multiple of one vector, along with a vector orthogonal to that vector.\n"
-"This includes the concepts of projections and othogonal components.\n"
+"This includes the concepts of projections and orthogonal components.\n"
 "\n"
 "## The Goal\n"
 "In this level, we are given two vectors, `u` and `v`. `u` is the vector we want to rewrite, and `v`\n"
@@ -1815,7 +1815,7 @@ msgid "## Vector Space Definition\n"
 "to get it as `0 • w + 0 • w`. Lastly, cancelling out a `0 • w` on each side gets `0 = 0 • w`.\n"
 "\n"
 "However, this proof relies on our assumptions and constructs the goal from them. This can be done in\n"
-"Lean, however, it requires using the `have` tactic, and is unnescessarily complex. In Lean, proofs are\n"
+"Lean, however, it requires using the `have` tactic, and is unnecessarily complex. In Lean, proofs are\n"
 "often done backwards, working from the goal and creating the hypotheses.\n"
 "\n"
 "Doing the proof backwards thus must first involve adding `0 • w` to both sides of the goal, undoing\n"
@@ -1853,7 +1853,7 @@ msgid "## Vector Space Definition\n"
 "\n"
 "### Note on simp and linarith\n"
 "\n"
-"In this world, we are primarilly proving simple statements about vector spaces. This is exactly what\n"
+"In this world, we are primarily proving simple statements about vector spaces. This is exactly what\n"
 "the `simp` and `linarith` tactics are meant to do. In fact, the `simp` tactic alone would be able to\n"
 "solve the first three levels of this world. Because of this, you will not be able to use those tactics\n"
 "in this world.\n"
@@ -1881,7 +1881,7 @@ msgstr ""
 msgid "`linear_combination_unique` is a proof that representation as a linear combination of a linearly independent\n"
 "set of vectors is unique. It takes in two subsets of a linearly independent set, along with two functions\n"
 "representing the linear combinations. The functions must be zero outside of the sets, and their sums\n"
-"must be equal. In this case, this prooves that functions will be equal."
+"must be equal. In this case, this proves that functions will be equal."
 msgstr ""
 
 #: Game.Levels.VectorSpaceWorld.Level03
@@ -2049,7 +2049,7 @@ msgid "This is the \"boss level\" of the Linear Independence and Span World. Thi
 "\n"
 "### The `funext` tactic\n"
 "The `funext` tactic lets you prove statements about functions. It works similarly to the `intro` tactic,\n"
-"where you introduce an arbitrary object, but instead of introducing from a `∀` statment, it works if\n"
+"where you introduce an arbitrary object, but instead of introducing from a `∀` statement, it works if\n"
 "you have a goal of the form `f = g`, where `funext x` will change the goal to the form `f x = g x`, and\n"
 "give you an arbitrary `x` in the domain of `f` and `g`.\n"
 "\n"
@@ -2224,7 +2224,7 @@ msgid "## Summary\n"
 "\n"
 "## Example\n"
 "\n"
-"If `h : ∃ (a : ℝ), a * a = 0` is a hypothesis, thatn `cases' h with a ha` will create a variable\n"
+"If `h : ∃ (a : ℝ), a * a = 0` is a hypothesis, then `cases' h with a ha` will create a variable\n"
 "`a : Nat` and a hypothesis `ha : a * a = 0`"
 msgstr ""
 
@@ -2416,7 +2416,7 @@ msgid "In this level, we will introduce two tactics: `intro`, and `exact`\n"
 "say `h: P` and we must construct a proof of `Q` from it.\n"
 "\n"
 "### Intro\n"
-"This idea is exatly what the `intro` tactic does. If the goal is of the form `P → Q`, `intro h` will\n"
+"This idea is exactly what the `intro` tactic does. If the goal is of the form `P → Q`, `intro h` will\n"
 "create a new hypothesis `h: P`, and change the goal into `Q`.\n"
 "\n"
 "### Exact\n"
@@ -2695,7 +2695,7 @@ msgid "In this level, the goal is to prove `x ≤ 1 + x`. This requires understa
 "clearly also true when working with real numbers. This is because the theorem \"le_iff_exists_add\"\n"
 "does not work with the real numbers, so the proof would be slightly different.\n"
 "\n"
-"We have this statment as a theorem, \"le_iff_exists_add\".\n"
+"We have this statement as a theorem, \"le_iff_exists_add\".\n"
 "\n"
 "However, note that this theorem will rewrite the goal to have a `∃` symbol. In this case, we have to\n"
 "find a number that satisfies a certain property. Once you find such a number, you can use the `use`\n"
@@ -2732,12 +2732,12 @@ msgid "`linear_independent_v` means that a set of vectors is linearly independen
 msgstr ""
 
 #: Game.Levels.TutorialWorld.Level10
-msgid "The `induction` tactic is a powerful tool to help you to prove statments involving natural numbers.\n"
+msgid "The `induction` tactic is a powerful tool to help you to prove statements involving natural numbers.\n"
 "It splits a proof into two cases: a base case and an inductive step. The base case is the smallest\n"
 "natural number you need to prove the proof for. The inductive step proves the theorem for all other\n"
 "numbers. In the inductive step, you can assume the theorem holds for some value `n`, and must then\n"
 "prove that it holds for `n + 1`, also written as `Nat.succ n`, the successor of `n`. Induction can\n"
-"also be used to prove theorems about objects indexed my natural numbers, such as vectors whose\n"
+"also be used to prove theorems about objects indexed by natural numbers, such as vectors whose\n"
 "dimension can be described by a natural number.\n"
 "\n"
 "The syntax for the `induction` tactic in Lean 4 is `induction n with | zero => ... | succ n h => ...`.\n"

Game/Levels/InnerProductWorld/Level06.lean

@@ -10,7 +10,7 @@ Title "Orthogonal Decomposition"
 Introduction "
 One of the most important theorems in linear algebra is orthogonal decomposition. This allows you to
 represent a vector as a scalar multiple of one vector, along with a vector orthogonal to that vector.
-This includes the concepts of projections and othogonal components.
+This includes the concepts of projections and orthogonal components.
 
 ## The Goal
 In this level, we are given two vectors, `u` and `v`. `u` is the vector we want to rewrite, and `v`
@@ -25,7 +25,7 @@ is trivial, since we are adding and subtracting the same vector to `u` on the ri
 
 /--
 `ortho_decom` is a proof that given vectors `u v : V` and `h : v ≠ 0`, then `orthogonal (u - (⟪u,v⟫ / (‖v‖^2)) • v) v`.
-This allows you to rewrite `u` as a scalar multiple of `v` added to a vector orthogonal to `v`. 
+This allows you to rewrite `u` as a scalar multiple of `v` added to a vector orthogonal to `v`.
 -/
 TheoremDoc LinearAlgebraGame.ortho_decom as "ortho_decom" in "Inner Product"
 

Game/Levels/LinearIndependenceSpanWorld/Level01.lean

@@ -57,7 +57,7 @@ and a function `f : V → K`, such that `x` is the sum over `s` of `f(v) • v`.
 DefinitionDoc is_linear_combination as "is_linear_combination"
 
 /--
-`Finset.sum` is how we difine summing over a set. It uses Mathlib's `Finset` Type, which means that we
+`Finset.sum` is how we define summing over a set. It uses Mathlib's `Finset` Type, which means that we
 can only sum over arbitrary finite sets. The syntax is as follows: With a additive group or field `K`, some Type `T`,
 some `s : Finset T`, and some `f : T → K`, `Finset.sum s (fun x => f x)` sums `f x` over all `x ∈ s`.
 -/

Game/Levels/LinearIndependenceSpanWorld/Level07.lean

@@ -40,7 +40,7 @@ goal into two subgoals: one where you have a hypothesis `hv : v = 0`, and anothe
 
 ### The `funext` tactic
 The `funext` tactic lets you prove statements about functions. It works similarly to the `intro` tactic,
-where you introduce an arbitrary object, but instead of introducing from a `∀` statment, it works if
+where you introduce an arbitrary object, but instead of introducing from a `∀` statement, it works if
 you have a goal of the form `f = g`, where `funext x` will change the goal to the form `f x = g x`, and
 give you an arbitrary `x` in the domain of `f` and `g`.
 
@@ -176,7 +176,7 @@ TheoremDoc Finset.notMem_union as "notMem_union" in "Sets"
 `linear_combination_unique` is a proof that representation as a linear combination of a linearly independent
 set of vectors is unique. It takes in two subsets of a linearly independent set, along with two functions
 representing the linear combinations. The functions must be zero outside of the sets, and their sums
-must be equal. In this case, this prooves that functions will be equal.
+must be equal. In this case, this proves that functions will be equal.
 -/
 TheoremDoc LinearAlgebraGame.linear_combination_unique as "linear_combination_unique" in "Vector Spaces"
 

Game/Levels/LinearIndependenceSpanWorld/Level08.lean

@@ -165,7 +165,7 @@ Statement linear_independent_insert_of_not_in_span
   (hS : linear_independent_v K V S)
   (hv_not_span : v ∉ span K V S):
   linear_independent_v K V (S ∪ {v}) := by
-    Hint "First, unfold the definitions, intro the variables and hypotheses we need, and simp where nescessary"
+    Hint "First, unfold the definitions, intro the variables and hypotheses we need, and simp where necessary"
     Hint "Linear independence means: if a linear combination equals zero, all coefficients must be zero."
     Hint (hidden := true) "Try `unfold linear_independent_v at *`"
     unfold linear_independent_v at *
@@ -178,7 +178,7 @@ Statement linear_independent_insert_of_not_in_span
     Hint (hidden := true) "Try `simp at hv_not_span`"
     simp at hv_not_span
 
-    Hint "We want to prove two seperate cases: v ∈ s and v ∉ s. If v ∉ s, then we know s ⊆ S, so since S
+    Hint "We want to prove two separate cases: v ∈ s and v ∉ s. If v ∉ s, then we know s ⊆ S, so since S
     is linearly independent, so is s. If v ∈ s, then we have more work to do. "
     Hint "Strategy: Split based on whether the new vector v appears in our linear combination."
     Hint (hidden := true) "Try `by_cases hvIns : v ∈ s`"

Game/Levels/LinearIndependenceSpanWorld/Level09.lean

@@ -259,7 +259,7 @@ Statement remove_redundant_span
 
   Hint "Now, let's consider the function we will be summing. To get a sum of `x`, we need two parts:
   the sum over `S` getting `x`, and the sum over `S \\ \{{w}}` to get `w`. This can be thought of as
-  two seperate functions. The first function will be similar to `fx`, but since we do not know what
+  two separate functions. The first function will be similar to `fx`, but since we do not know what
   `fx` is outside of `sx`, we must make this function `0` outside of `sx`. We can define this first
   function with a `let` statement"
   Hint "Mathematical insight: We're decomposing x = Σ(fx v • v) into two parts: contributions from S\\\{{w}} and from w itself."

Game/Levels/TutorialWorld/Level03.lean

@@ -66,7 +66,7 @@ taking proofs of `P` to proofs of `Q`. In Lean, this means that we take an arbit
 say `h: P` and we must construct a proof of `Q` from it.
 
 ### Intro
-This idea is exatly what the `intro` tactic does. If the goal is of the form `P → Q`, `intro h` will
+This idea is exactly what the `intro` tactic does. If the goal is of the form `P → Q`, `intro h` will
 create a new hypothesis `h: P`, and change the goal into `Q`.
 
 ### Exact

Game/Levels/TutorialWorld/Level06.lean

@@ -25,7 +25,7 @@ you have finished the level.
 
 ## Example
 
-If `h : ∃ (a : ℝ), a * a = 0` is a hypothesis, thatn `cases' h with a ha` will create a variable
+If `h : ∃ (a : ℝ), a * a = 0` is a hypothesis, then `cases' h with a ha` will create a variable
 `a : Nat` and a hypothesis `ha : a * a = 0`
 
 -/

Game/Levels/TutorialWorld/Level09.lean

@@ -42,7 +42,7 @@ b = a + c. In this level, we have decided to use the natural numbers, although t
 clearly also true when working with real numbers. This is because the theorem \"le_iff_exists_add\"
 does not work with the real numbers, so the proof would be slightly different.
 
-We have this statment as a theorem, \"le_iff_exists_add\".
+We have this statement as a theorem, \"le_iff_exists_add\".
 
 However, note that this theorem will rewrite the goal to have a `∃` symbol. In this case, we have to
 find a number that satisfies a certain property. Once you find such a number, you can use the `use`

Game/Levels/TutorialWorld/Level10.lean

@@ -42,12 +42,12 @@ NewTactic induction
 NewTheorem Nat.add_succ
 
 Introduction "
-The `induction` tactic is a powerful tool to help you to prove statments involving natural numbers.
+The `induction` tactic is a powerful tool to help you to prove statements involving natural numbers.
 It splits a proof into two cases: a base case and an inductive step. The base case is the smallest
 natural number you need to prove the proof for. The inductive step proves the theorem for all other
 numbers. In the inductive step, you can assume the theorem holds for some value `n`, and must then
 prove that it holds for `n + 1`, also written as `Nat.succ n`, the successor of `n`. Induction can
-also be used to prove theorems about objects indexed my natural numbers, such as vectors whose
+also be used to prove theorems about objects indexed by natural numbers, such as vectors whose
 dimension can be described by a natural number.
 
 The syntax for the `induction` tactic in Lean 4 is `induction n with | zero => ... | succ n h => ...`.