Merge pull request #34 from pitmonticone/main

Fix typos

Game/Doc/Definitions.lean

@@ -13,7 +13,7 @@ import GameServer.Commands
 -- This notation is for our own version of the natural numbers, called `MyNat`.
 -- The natural numbers implemented in Lean's core are called `Nat`.
 
--- If you end up getting someting of type `Nat` in this game, you probably
+-- If you end up getting something of type `Nat` in this game, you probably
 -- need to write `(4 : ℕ)` to force it to be of type `MyNat`.
 
 -- *Write with `\\N`.*

Game/Levels/LessOrEqual/L03le_succ_self.lean

@@ -34,7 +34,7 @@ This works because `succ_eq_add_one x` is a proof of `succ x = x + 1`.
 /-
 Introduction
 "
-Because constanly rewriting `zero_add` and `add_zero` is a bit dull,
+Because constantly rewriting `zero_add` and `add_zero` is a bit dull,
 let's unlock the `ring` tactic. This will prove any goal which is \"true
 in the language of ring theory\", for example `a + b + c = c + b + a`.
 It doesn't understand `succ` though, so use `succ_eq_add_one` in this

Game/Levels/LessOrEqual/inequality_world_tactic_notes.txt

@@ -1,21 +1,21 @@
 Function world:
-lvel 1 exact
-level 2 intro
-lwcwl 3 have
-level 4 apply
-
-Prop world
-LEvel 1 exact again
+level 1 exact
 level 2 intro
 level 3 have
 level 4 apply
-leevl 8 not P = P -> false (no explanation of false?)
+
+Prop world
+level 1 exact again
+level 2 intro
+level 3 have
+level 4 apply
+level 8 not P = P -> false (no explanation of false?)
 
 Advanced Prop world ;
 level 1 split
 level 2 rcases
 (for and)
-(note that level 1 is now consructor)
+(note that level 1 is now constructor)
 level 6 left and right
 level 9 exfalso (because \not is involved)
 level 10 by_cases

Game/Levels/Map.txt

@@ -35,9 +35,9 @@ What about succ m ≤ succ n ↔ m ≤ n? This was a lost level (but not about <
 
 If a ≤ b then a + x ≤ b + x. And iff version?
 
-## Advanced Multiplication world: you can cancel muliplication
+## Advanced Multiplication world: you can cancel multiplication
 by nonzero x. ad+bc=ac+bd -> a=b or c=d? This should be preparation
-for divisilibity world.
+for divisibility world.
 
 ## Divisibility world
 

Game/Levels/OldAdvProposition/Level_3.lean

@@ -24,7 +24,7 @@ Statement --and_trans
   intro h
   rcases h with ⟨p, q⟩
   ```
-  i.e. introducing a new assumption and then immediately take it appart.
+  i.e. introducing a new assumption and then immediately take it apart.
 
   In that case you could do that in a single step:
 

Game/Levels/OldAdvProposition/Level_7.lean

@@ -51,5 +51,5 @@ Well done! Note that the syntax for `rcases` is different whether it's an \"or\"
 * `rcases h with ⟨p, q⟩` splits an \"and\" in the assumptions into two parts. You get two assumptions
 but still only one goal.
 * `rcases h with p | q` splits an \"or\" in the assumptions. You get **two goals** which have different
-assumptions, once assumping the lefthand-side of the dismantled \"or\"-assumption, once the righthand-side.
+assumptions, once assuming the lefthand-side of the dismantled \"or\"-assumption, once the righthand-side.
 "

Game/Levels/Power/L06pow_add.lean

@@ -6,7 +6,7 @@ Title "pow_add"
 
 namespace MyNat
 
-Introduction "Let's now begin our approch to the final boss,
+Introduction "Let's now begin our approach to the final boss,
 by proving some more subtle facts about powers."
 
 LemmaDoc MyNat.pow_add as "pow_add" in "^" "

Game/Levels/Power/L09add_sq.lean

@@ -14,7 +14,7 @@ Introduction
 -- **TODO** get the `ring` hack working again.
 
 LemmaDoc MyNat.add_sq as "add_sq" in "^" "
-`add_sq a b` is the statment that $(a+b)^2=a^2+b^2+2ab.$
+`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$
 "
 
 /-- For all numbers $a$ and $b$, we have