Fix more typos.

Game/Doc/Definitions.lean

@@ -12,18 +12,18 @@ An “And” can be introduced with the `and_intro` theorem. Conjunctions and bi
 p : P
 q : Q
 -- Each new term is evidence for P ∧ Q
--- Explicit Constructer, no annotations needed
+-- Explicit Constructor, no annotations needed
 have h₁ := and_intro p q
 have h₂ := and_intro (left := p) (right := q)
--- Implicit Constructuer, annotations based on context
+-- Implicit Constructor, annotations based on context
 -- Type these angle brackets with “\<” and “\>”
 have h₆ : P ∧ Q := ⟨p,q⟩
 have h₇ := (⟨p,q⟩ : P ∧ Q)
 ```
 ## Elimination
 An “And” like `h : P ∧ Q` can be reduced in two ways:
-1. Aquire evidence for `P` using `and_left h` or `h.left`
-2. Aquire evidence for `Q` using `and_right` or `h.right`
+1. Acquire evidence for `P` using `and_left h` or `h.left`
+2. Acquire evidence for `Q` using `and_right` or `h.right`
 -/
 DefinitionDoc GameLogic.and_def as "∧"
 
@@ -64,18 +64,18 @@ An “If and only if” can be introduced with the `iff_intro` theorem. Bicondit
 h₁ : P → Q
 h₂ : Q → P
 -- Each new term is evidence for P ↔ Q
--- Explicit Constructer, no annotations needed
+-- Explicit Constructor, no annotations needed
 have h₁ := iff_intro h₁ h₂
 have h₂ := iff_intro (mp := h₁) (mpr := h₂)
--- Implicit Constructuer, annotations based on context
+-- Implicit Constructor, annotations based on context
 -- Type these angle brackets with “\<” and “\>”
 have h₆ : P ↔ Q := ⟨h₁, h₂⟩
 have h₇ := (⟨h₁, h₂⟩ : P ↔ Q)
 ```
 ## Elimination
 An “If and only if” like `h : P ↔ Q` can be reduced in two ways:
-1. Aquire evidence for `P → Q` using `iff_mp h` or `h.mp`
-2. Aquire evidence for `Q → P` using `iff_mpr h` or `h.mpr`
+1. Acquire evidence for `P → Q` using `iff_mp h` or `h.mp`
+2. Acquire evidence for `Q → P` using `iff_mpr h` or `h.mpr`
 ## Rewrite
 Biconditionals let you use the `rewrite` tactic to change goals or assumptions.
 -/

Game/Levels/AndIntro.lean

@@ -43,7 +43,7 @@ and how some things which may look like expressions really are not:
 4 (++) 6
 (4 +) 6
 ```
-The expressions that this game is asking you to form are mostly in prefix form. In context, this means the operation is given a textual name instead of a symbol and the parameters are separated by spaces **after** the name. For example; the above expressions may look like:
+The expressions that this game is asking you to form are mostly in prefix form. In context, this means the operation is given a textual name instead of a symbol and the parameters are separated by spaces **after** the name. For example, the above expressions may look like:
 ```
 add 4 6
 add (4) 6

Game/Levels/AndIntro/L01.lean

@@ -19,7 +19,7 @@ You've made a todo list, so you've begun to plan your party.
 ## Assumptions
 `todo_list : P` — Can be read as “The `todo_list` is evidence that you're `P`lanning a party”
 # The Exact Tactic
-The Exact tactic is — for now — the means through which you give the game your answer. It's your way of declaring that you're done. In this level, you're just going to be using one of the assumptions directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\
+The `exact` tactic is — for now — the means through which you give the game your answer. It's your way of declaring that you're done. In this level, you're just going to be using one of the assumptions directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\
 \\
 The input will look like `exact e` where `e` is an expression the game will accept for the current Goal.\\
 \\

Game/Levels/AndIntro/L08.lean

@@ -49,7 +49,7 @@ have c := h.right.right.left.left
 -- build C ∧ P ∧ S
 have cps := and_intro c psa.left
 
--- exibit A ∧ C ∧ P ∧ S
+-- exhibit A ∧ C ∧ P ∧ S
 exact and_intro psa.right cps
 ```
 "

Game/Levels/ImpIntro/L01.lean

@@ -26,7 +26,7 @@ You use an implication the same way you've been using `and_intro`, `and_left`, a
 - assumption `h₁ : A → B`
 - have `b : B := h₁ a`
 
-You can read `h₁ a` as modus ponens. In fact, you've unlocked a theorem called modus_ponens that you could use here. Since modus ponens is implemented as function application, you can — and should — always just Juxtapose instead.
+You can read `h₁ a` as modus ponens. In fact, you've unlocked a theorem called `modus_ponens` that you could use here. Since modus ponens is implemented as function application, you can — and should — always just Juxtapose instead.
 # A note
 You'll often see assumptions given one or two letter names (`p`, `r`, `q`, `h₁`, `h₂`, `h₃`, etc). Assumptions are generally not long-lived. They are part of some expression, exhibit some implication, and then are discarded. Their names in this context don't need to be particularly memorable.\\
 \\

Game/Levels/NotTactic/L08.lean

@@ -14,7 +14,7 @@ OnlyTactic
 
 Introduction "
 # Pattern matching tip
-You can solve this level using the knowledge you've aquired so far. If you've used a language with destructuring or pattern matching before, then you can introduce and pattern-match in one step with `intro ⟨nq, p⟩`. Doing so means you won't need the `cases` tactic for this level.
+You can solve this level using the knowledge you've acquired so far. If you've used a language with destructuring or pattern matching before, then you can introduce and pattern-match in one step with `intro ⟨nq, p⟩`. Doing so means you won't need the `cases` tactic for this level.
 "
 
 /-- Negation into conjunction. -/