diff --git a/Game.lean b/Game.lean
index cbe403b..33df0ae 100755
--- a/Game.lean
+++ b/Game.lean
@@ -175,5 +175,5 @@ CaptionShort "Lean intro to Logic"
 CaptionLong "A mostly self-contained introduction to constructive logic using Lean. Learn how each propositional connective can be introduced and eliminated using both terms and tactics."
 CoverImage "images/logic0101_v4.png"
 
-/-! Build the game. Show's warnings if it found a problem with your game. -/
+/-! Build the game. Shows warnings if it found a problem with your game. -/
 MakeGame
diff --git a/Game/Doc/Definitions.lean b/Game/Doc/Definitions.lean
index 73eb986..5131e4a 100755
--- a/Game/Doc/Definitions.lean
+++ b/Game/Doc/Definitions.lean
@@ -16,7 +16,7 @@ q : Q
 have h₁ := and_intro p q
 have h₂ := and_intro (left := p) (right := q)
 -- Implicit Constructuer, annotations based on context
--- Type these angle brackets with “\\<” and “\\>”
+-- Type these angle brackets with “\<” and “\>”
 have h₆ : P ∧ Q := ⟨p,q⟩
 have h₇ := (⟨p,q⟩ : P ∧ Q)
 ```
@@ -68,7 +68,7 @@ h₂ : Q → P
 have h₁ := iff_intro h₁ h₂
 have h₂ := iff_intro (mp := h₁) (mpr := h₂)
 -- Implicit Constructuer, annotations based on context
--- Type these angle brackets with “\\<” and “\\>”
+-- Type these angle brackets with “\<” and “\>”
 have h₆ : P ↔ Q := ⟨h₁, h₂⟩
 have h₇ := (⟨h₁, h₂⟩ : P ↔ Q)
 ```
@@ -139,16 +139,16 @@ DefinitionDoc GameLogic.FunIntro as "→ intro"
 | --- | :---: | :---: | --- |
 | True | `True` |  |  |
 | False | `False` |  |  |
-| Not | `Not` | ¬ | `\\n` `\\not` `\\neg` `\\lnot` |
-| And | `/\\` | ∧ | `\\and` `\\an` `\\wedge` |
-| Or | `\\/` | ∨ | `\\v` `\\or` `\\vee` |
-| Implies | `->` | → | `\\r` `\\imp` `\\\\->` `\\to` `\\r-` `\\rightarrow` |
-| Iff | `<->` | ↔ | `\\iff` `\\lr-` `\\lr` `\\<->` `\\leftrightarrow` |
-| For All | `foral` | ∀ | `\\all` `\\forall` |
-| Exists | `exists` | ∃ | `\\ex` `\\exists` |
+| Not | `Not` | ¬ | `\n` `\not` `\neg` `\lnot` |
+| And | `/\` | ∧ | `\and` `\an` `\wedge` |
+| Or | `\/` | ∨ | `\v` `\or` `\vee` |
+| Implies | `->` | → | `\r` `\imp` `\->` `\to` `\r-` `\rightarrow` |
+| Iff | `<->` | ↔ | `\iff` `\lr-` `\lr` `\<->` `\leftrightarrow` |
+| For All | `foral` | ∀ | `\all` `\forall` |
+| Exists | `exists` | ∃ | `\ex` `\exists` |
 
 ### **Anonymous Function**
-Example:\\
+Example:
 An anonymous function that swaps a conjunction
 ```
 -- Ascii
@@ -158,16 +158,16 @@ fun h : P ∧ Q => and_intro (and_right h) (and_left h)
 ```
 | $Ascii~~~$ | $Unicode~~~$ | $Unicode Cmd$ |
 | --- | :---: | --- |
-| `fun` | λ | `\\fun` `\\la` `\\lambda` `\\lamda` `\\lam` `\\Gl` |
-| `=>` | ↦ | `\\map` `\\mapsto` |
+| `fun` | λ | `\fun` `\la` `\lambda` `\lamda` `\lam` `\Gl` |
+| `=>` | ↦ | `\map` `\mapsto` |
 
 ### **Other Unicode**
 | $Name$ | $Unicode~~~$ | $Unicode Cmd$ |
 | --- | :---: | --- |
-| Angle brackets | ⟨ ⟩ | `\\<` `\\>` `\\langle` `\\rangle` |
-| Subscript Numbers | ₁ ₂ ₃ ... | `\\1` `\\2` `\\3` ... |
-| Left Arrow | ← | `\\l` `\\leftarrow` `\\gets` `\\<-` |
-| Turnstyle | ⊢ | `\\│-` `\\entails` `\\vdash` `\\goal` |
+| Angle brackets | ⟨ ⟩ | `\<` `\>` `\langle` `\rangle` |
+| Subscript Numbers | ₁ ₂ ₃ ... | `\1` `\2` `\3` ... |
+| Left Arrow | ← | `\l` `\leftarrow` `\gets` `\<-` |
+| Turnstyle | ⊢ | `\│-` `\entails` `\vdash` `\goal` |
 -/
 DefinitionDoc GameLogic.AsciiTable as "Unicode Table"
 
diff --git a/Game/Doc/Lemmas.lean b/Game/Doc/Lemmas.lean
index 420ffca..404cd81 100755
--- a/Game/Doc/Lemmas.lean
+++ b/Game/Doc/Lemmas.lean
@@ -181,6 +181,10 @@ There is are infix operators for function application; they look like `|>` and `
 It's twin, `|>` chains such that `x |> f |> g` is interpreted as `g (f x)`.
 
 What makes the infix operators usefull is that they can often replace a pair of brackets `(...)` making expressions easier to read.
+
+----
+# Computer Science
+If you've done some programming before, you might recognise `Modus Ponens` as the identity function for implications. So `(modus_ponens and_left)` is extensionally equal to `and_left`. There's a conspiracy at work here!
 -/
 TheoremDoc GameLogic.modus_ponens as "modus_ponens" in "→"
 
@@ -196,15 +200,15 @@ def and_comm {P Q : Prop}: P ∧ Q ↔ Q ∧ P :=
 -/
 TheoremDoc GameLogic.and_comm as "and_comm" in "∧"
 
-def and_assoc {P Q R : Prop}: P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R :=
-  ⟨ λ⟨p,q,r⟩ ↦ ⟨⟨p,q⟩,r⟩,
-    λ⟨⟨p,q⟩,r⟩ ↦ ⟨p,q,r⟩
+def and_assoc {P Q R : Prop}: (P ∧ Q) ∧ R ↔ P ∧ Q ∧ R :=
+  ⟨ λ⟨⟨p,q⟩,r⟩ ↦ ⟨p,q,r⟩,
+    λ⟨p,q,r⟩ ↦ ⟨⟨p,q⟩,r⟩
   ⟩
 
 /--
 # ∧ is Associative
 
-`and_assoc` is evidence that `P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R`
+`and_assoc` is evidence that `(P ∨ Q) ∨ R ↔ P ∨ Q ∨ R`
 -/
 TheoremDoc GameLogic.and_assoc as "and_assoc" in "∧"
 
@@ -221,13 +225,13 @@ def or_comm {P Q : Prop}: P ∨ Q ↔ Q ∨ P :=
 TheoremDoc GameLogic.or_comm as "or_comm" in "∨"
 
 -- or_assoc
-def or_assoc {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R :=
+def or_assoc {P Q R : Prop}: (P ∨ Q) ∨ R ↔ P ∨ Q ∨ R :=
   have mp := (Or.elim ·
-    (Or.inl ∘ Or.inl)
-    (Or.elim · (Or.inl ∘ Or.inr) Or.inr))
-  have mpr := (Or.elim ·
     (Or.elim · Or.inl (Or.inr ∘ Or.inl))
     (Or.inr ∘ Or.inr))
+  have mpr := (Or.elim ·
+    (Or.inl ∘ Or.inl)
+    (Or.elim · (Or.inl ∘ Or.inr) Or.inr))
   ⟨mp,mpr⟩
 
 -- or_assoc expanded
@@ -273,9 +277,9 @@ Of course, because of `and_comm`, you know you can flip this around too.
 `Q → R` and `P → Q` implies `P → R` has a near-identical proof.
 
 ### Infix Operator:
-`imp_trans` has an infix operator. This looks like `≫` (which is written as “`\\gg`”).
+`imp_trans` has an infix operator. This looks like `≫` (which is written as “`\gg`”).
 
-For the math-inclined, because the expression for an implication is a function, you can also use function composition for the same purpose (`∘` is written as “`\\o`”). Just remember that `∘` has the parameters swapped from the way `imp_trans` is defined.
+For the math-inclined, because the expression for an implication is a function, you can also use function composition for the same purpose (`∘` is written as “`\o`”). Just remember that `∘` has the parameters swapped from the way `imp_trans` is defined.
 -/
 TheoremDoc GameLogic.imp_trans as "imp_trans" in "→"
 
@@ -301,15 +305,15 @@ def modus_tollens {P Q : Prop} (h: P → Q) (nq: ¬Q) : ¬P := h ≫ nq
 # Modus Tollens
 Denying the consequent.
 
-If P, then Q.\\
-Not Q.\\
+If P, then Q.\
+Not Q.\
 Therefore, not P.
 ```
 mt : (P → Q) → ¬Q → ¬P
 ```
 
 ### Infix Operator:
-`modus_tollens` is a specialized version of `imp_trans`, which makes it possible to use `≫` (which is written as “`\\gg`”) as an infix operator for `modus_tollens`.
+`modus_tollens` is a specialized version of `imp_trans`, which makes it possible to use `≫` (which is written as “`\gg`”) as an infix operator for `modus_tollens`.
 -/
 TheoremDoc GameLogic.modus_tollens as "modus_tollens" in "→"
 
diff --git a/Game/Doc/Tactics.lean b/Game/Doc/Tactics.lean
index 2c411f5..2d81c64 100755
--- a/Game/Doc/Tactics.lean
+++ b/Game/Doc/Tactics.lean
@@ -101,14 +101,14 @@ all `P`s in the goal to `Q`s. It's the way to “substitute in”.
 
 ## Variants
 
-* `rw [← h₁]` — changes `Q`s to `P`s; get the back arrow by typing `\\left ` or `\\l`.
+* `rw [← h₁]` — changes `Q`s to `P`s; get the back arrow by typing `\left ` or `\l`.
 
 * `rw [h₁, h₂, h₃, h₄]` — a sequence of rewrites
 
 * `rw [h₁] at h₂` — changes `P`s to `Q`s in hypothesis `h₂`
 
 * `rw [h₁] at h₂ h₃ ⊢` — changes `X`s to `Y`s in two hypotheses and the goal;
-get the `⊢` symbol with `\\|-`.
+get the `⊢` symbol with `\|-`.
 
 * `repeat rw [h₁]` — keep attempting to `rw` until there are no more matches. For example, if the goal is `¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬P` you can use `rw [not_not_not]` 9 times or just use `repeat rw [not_not_not]` once to get `¬P`
 
diff --git a/Game/Levels/AndIntro.lean b/Game/Levels/AndIntro.lean
index bd97411..96cb2c4 100755
--- a/Game/Levels/AndIntro.lean
+++ b/Game/Levels/AndIntro.lean
@@ -17,7 +17,7 @@ You're hosting your yearly soirée, and it's time to start planning! Last year y
 \\
 This year will be different‼ This year, if you want to be sure that there will be fancy cheeses, you had better have evidence that somebody is bringing the cheese platter.
 
-World 1: **Party Invites** is a tutorial world that is meant to introduce you to conjunction — the logical “and”. The symbol used to denote an “and” looks like “`∧`”. You'll learn to how to use evidence to create an `∧` and how also how to get evidence out when it's been `∧`ed together.\\
+World 1: **Party Invites** is a tutorial world that is meant to introduce you to conjunction — the logical “and”. The symbol used to denote an “and” looks like “`∧`”. You'll learn to how to use evidence to create an `∧` and also how to get evidence out when it's been `∧`ed together.\\
 \\
 The real-world analogues for evidence of `A ∧ B` might be a box with evidence for `A` and evidence for `B`, an audio recording with both pieces of evidence, or a tree with evidence in its branches.\\
 \\
diff --git a/Game/Levels/AndIntro/L01.lean b/Game/Levels/AndIntro/L01.lean
index 6487863..dc8c75e 100755
--- a/Game/Levels/AndIntro/L01.lean
+++ b/Game/Levels/AndIntro/L01.lean
@@ -20,7 +20,7 @@ You've made a todo list, so you've begun to plan your 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 expression looks like `exact e` were `e` is an expression the game will accept for the current Goal.\\
+The input will look like `exact e` were `e` is an expression the game will accept for the current Goal.\\
 \\
 ⋆Spoilers!⋆ If you enter “`exact todo_list`,” you will have completed this level.
 
diff --git a/Game/Levels/AndIntro/L02.lean b/Game/Levels/AndIntro/L02.lean
index fa61249..ca76dd5 100755
--- a/Game/Levels/AndIntro/L02.lean
+++ b/Game/Levels/AndIntro/L02.lean
@@ -22,7 +22,7 @@ You've labelled the box explicitly, specifying that Pippin's invitation is on th
 - P — “**P**ippin is invited to the party”
 - S — “**S**ybeth is invited to the party”
 
-In this game, that means anything operating as evidence for `A ∧ B` will have a left part and a right part as well. The box described in the intro works this way.
+Like the box described in the intro, any evidence for a conjunction like `A ∧ B` will have a left part and a right part.
 # Assumptions
 - `p : P` — Your invitation for Pippin is evidence that Pippin is invited to the party
 - `s : S` — Your invitation for Sybeth is evidence that Sybeth is invited to the party
@@ -30,9 +30,9 @@ In this game, that means anything operating as evidence for `A ∧ B` will have
 Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use evidence (generally lowercase letters), to deduce new propositions (generally uppercase letters)
 
 # Using the `∧` Construtor
-This level has unlocked “`∧`” under definitions. This has made the `and_intro` constructor available. You can use `and_intro` by giving it the two relevant pieces of evidence. The expression looks like: `and_intro e₁ e₂` where `e₁` and `e₂` are evidence.\\
+This level has unlocked “`∧`” under definitions. This has made the `and_intro` theorem available. You can use `and_intro` by giving it the two relevant pieces of evidence. The expression looks like: `and_intro e₁ e₂` where `e₁` and `e₂` are evidence.\\
 \\
-The help-page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackers `⟨` `⟩`).
+The help-page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackers `⟨` `,` `⟩` ).
 
 # A reminder
 Use the `exact` tactic to exhibit evidence for a goal
diff --git a/Game/Levels/IffIntro/L06.lean b/Game/Levels/IffIntro/L06.lean
index dcabcff..9af3e42 100644
--- a/Game/Levels/IffIntro/L06.lean
+++ b/Game/Levels/IffIntro/L06.lean
@@ -32,25 +32,11 @@ Two new theorems have been unlocked for this level. We'll make you prove them la
 "
 
 /-- Exactly 2 rewrites -/
-Statement (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
+Statement (P Q R : Prop) (h : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R)) : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R) := by
   rw [or_assoc, and_assoc]
   exact h
 
-example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
-  exact imp_trans
-    (λpvqvr ↦ h (or_elim pvqvr
-      (λp ↦ or_inl (or_inl p))
-      (λqvr ↦ or_elim qvr
-        (λq ↦ or_inl (or_inr q))
-        (λr ↦ or_inr r))
-    ))
-    λnpqr pqr ↦ npqr (
-      and_intro (
-        and_intro pqr.left pqr.right.left
-      ) pqr.right.right
-    )
-
-example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
+example (P Q R : Prop) (h : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R)) : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R) := by
   exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp
 
 Conclusion "
diff --git a/Game/Levels/IffTactic/L06.lean b/Game/Levels/IffTactic/L06.lean
index e133c98..7a591c7 100644
--- a/Game/Levels/IffTactic/L06.lean
+++ b/Game/Levels/IffTactic/L06.lean
@@ -16,7 +16,7 @@ Introduction "
 Even without the `rw` tactic, this can be solved in a few lines.
 "
 
-Statement (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
+Statement (P Q R : Prop) (h : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R)) : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R) := by
   intro _ _
   apply h
   apply or_assoc.mp
diff --git a/Game/Levels/OrTactic/L05.lean b/Game/Levels/OrTactic/L05.lean
index 8987ace..1d13175 100755
--- a/Game/Levels/OrTactic/L05.lean
+++ b/Game/Levels/OrTactic/L05.lean
@@ -8,6 +8,7 @@ Title "Old Hat"
 
 NewTheorem GameLogic.or_comm
 OnlyTactic
+  cases
   assumption
   apply
   left