From e7a10ee19fd14c19a5f877a0167dd1b9a0e68b26 Mon Sep 17 00:00:00 2001
From: Trequetrum <trequetrum@gmail.com>
Date: Fri, 15 Dec 2023 23:07:26 +0000
Subject: [PATCH] lvl updates

---
 Game.lean                     |  4 +--
 Game/Doc/Definitions.lean     | 57 +++++++++++++++++++++++++++--------
 Game/Doc/Lemmas.lean          | 27 +++++++++++------
 Game/Doc/Tactics.lean         | 51 +++++++++++++++++++++++++++++++
 Game/Levels/AndIntro/L01.lean |  5 +--
 Game/Levels/AndIntro/L02.lean |  5 ++-
 Game/Levels/AndIntro/L03.lean |  7 +++--
 Game/Levels/AndIntro/L04.lean |  4 ++-
 Game/Levels/AndIntro/L05.lean |  4 ++-
 Game/Levels/AndIntro/L06.lean |  2 ++
 Game/Levels/AndIntro/L07.lean |  2 ++
 Game/Levels/AndIntro/L08.lean |  2 ++
 Game/Levels/IffIntro.lean     | 13 ++++++--
 Game/Levels/IffIntro/L01.lean | 36 +++++++++++++++++-----
 Game/Levels/IffIntro/L02.lean | 29 ++++++++++++++++++
 Game/Levels/ImpIntro/L01.lean | 13 ++++++--
 Game/Levels/ImpIntro/L02.lean |  4 ++-
 Game/Levels/ImpIntro/L03.lean |  4 ++-
 Game/Levels/ImpIntro/L04.lean |  4 ++-
 Game/Levels/ImpIntro/L05.lean |  4 ++-
 Game/Levels/ImpIntro/L06.lean |  2 ++
 Game/Levels/ImpIntro/L07.lean |  2 ++
 Game/Levels/ImpIntro/L08.lean |  2 ++
 Game/Levels/ImpIntro/L09.lean |  2 ++
 Game/Levels/L01-template.lean |  2 ++
 Game/Levels/NotIntro.lean     | 12 --------
 Game/Levels/NotIntro/L01.lean |  2 ++
 Game/Levels/NotIntro/L02.lean |  4 ++-
 Game/Levels/NotIntro/L03.lean |  3 +-
 Game/Levels/NotIntro/L04.lean |  2 ++
 Game/Levels/NotIntro/L05.lean |  2 ++
 Game/Levels/NotIntro/L06.lean |  4 ++-
 Game/Levels/NotIntro/L07.lean |  2 ++
 Game/Levels/NotIntro/L08.lean |  2 ++
 Game/Levels/NotIntro/L09.lean |  2 ++
 Game/Levels/NotIntro/L10.lean |  2 ++
 Game/Levels/NotIntro/L11.lean |  2 ++
 Game/Levels/NotIntro/L12.lean |  4 ++-
 Game/Levels/OrIntro.lean      |  2 +-
 Game/Levels/OrIntro/L01.lean  |  4 ++-
 Game/Levels/OrIntro/L02.lean  |  4 ++-
 Game/Levels/OrIntro/L03.lean  |  4 ++-
 Game/Levels/OrIntro/L04.lean  |  8 ++++-
 Game/Levels/OrIntro/L05.lean  |  4 ++-
 Game/Levels/OrIntro/L06.lean  | 31 +++++++++++++++++--
 Game/Levels/OrIntro/L07.lean  | 16 +++++++++-
 Game/Levels/OrIntro/L08.lean  | 12 +++++---
 47 files changed, 335 insertions(+), 80 deletions(-)
 create mode 100644 Game/Levels/IffIntro/L02.lean

diff --git a/Game.lean b/Game.lean
index ef08abc..0ea4b16 100755
--- a/Game.lean
+++ b/Game.lean
@@ -129,9 +129,7 @@ Info "
 
 This game is currently in its initial development phase, designed to be largely self-contained and accessible without requiring a programming or math background to navigate. Feedback about meeting that goal is welcome!
 
-While self-contained; in many ways, this game is targeted more at programmers than mathematicians. It doesn't use classical reasoning, sticking instead to constructive logic. The emphasis for most of the theorem proving is on writing proof terms — rather than using tactics. In fact, logic proof automation is such that if you use the tactic **`tauto`**, you can prove any propositional logic theorem.
-
-Constructive propositional logic is effectively decidable, in the sense that a finite constructive process applies uniformly to every propositional formula, either producing a proof of the formula or demonstrating that no such proof can exist. The fun is in thinking your way through a puzzle with the tools made available to you.
+While self-contained; in many ways, this game is targeted more at programmers than mathematicians. It doesn't use classical reasoning, sticking instead to constructive logic. The emphasis for most of the theorem proving is on writing proof terms — rather than using tactics.
 
 Please feel encouraged to visit the game's GitHub repository and initiate a discussion on any topic regarding this game. Just open a new issue or comment on an existing one.
 Github: [A Lean Intro to Logic](https://github.com/Trequetrum/lean4game-logic)
diff --git a/Game/Doc/Definitions.lean b/Game/Doc/Definitions.lean
index b877007..e3bb02d 100755
--- a/Game/Doc/Definitions.lean
+++ b/Game/Doc/Definitions.lean
@@ -1,8 +1,10 @@
 import GameServer.Commands
 
+namespace GameLogic
+
 def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h
 
-DefinitionDoc and_left as "∧-e left" "
+DefinitionDoc GameLogic.and_left as "∧ elim left" "
 # ∧ Elimination Left
 ### and_left : P ∧ Q -> P`
 
@@ -13,7 +15,7 @@ If `h` is a term with a type like `AP∧ Q`
 
 def and_right {P Q : Prop} (h : P ∧ Q) : Q := And.right h
 
-DefinitionDoc and_right as "∧-e right" "
+DefinitionDoc GameLogic.and_right as "∧ elim right" "
 # ∧ Elimination Right
 ### and_right : P ∧ Q -> Q`
 
@@ -24,7 +26,7 @@ If `h` is a term with a type like `P ∧ Q`
 
 def and_intro {P Q : Prop} (left : P) (right : Q) : P ∧ Q := And.intro left right
 
-DefinitionDoc and_intro as "∧ intro" "
+DefinitionDoc GameLogic.and_intro as "∧ intro" "
 # and_intro
 ### `and_intro : P -> Q -> P ∧ Q`
 `and_intro` is a function with two parameters. It takes two disparate pieces of evidence and combines them into a single piece of evidence. If `(e₁ : P)` and `(e₂ : Q)` are evidence, then
@@ -52,7 +54,7 @@ have h₇ := (⟨p,q⟩ : P ∧ Q)
 ```
 "
 
-DefinitionDoc FunElim as "→ elim" "
+DefinitionDoc GameLogic.FunElim as "→ elim" "
 # Function Application/Implication Elimination
 `P → Q` is propostion given to functions from evidence of `P` to evidence of `Q`.
 # Juxtaposition
@@ -86,7 +88,7 @@ exact (h₁ a)
 Takes `h₁` and applies `a` to it.
 "
 
-DefinitionDoc FunIntro as "→ intro" "
+DefinitionDoc GameLogic.FunIntro as "→ intro" "
 # `fun _ => _`
 You can create evidence for an implication by defining the appropriate function.
 - `have h₁ : P → P := fun p : P => p`
@@ -101,7 +103,7 @@ Generally, you don't need to repeat the types when they're obvious from the cont
 - `=>` can be written as `↦`
 "
 
-DefinitionDoc AsciiTable as "Symbol Table" "
+DefinitionDoc GameLogic.AsciiTable as "Symbol Table" "
 ### **Logic Constants & Operators**
 | $Name~~~$ | $Ascii~~~$ | $Unicode$ | $Unicode Cmd$ |
 | --- | :---: | :---: | --- |
@@ -136,7 +138,7 @@ fun h : P ∧ Q => and_intro (and_right h) (and_left h)
 | Subscript Numbers | ₁ ₂ ₃ ... | `\\1` `\\2` `\\3` ... |
 "
 
-DefinitionDoc Precedence as "Precedence" "
+DefinitionDoc GameLogic.Precedence as "Precedence" "
 # Remembering Algebra
 In math class, you may have learned an acronym like BEDMAS or PEMDAS to remember the precedence of operators in your math expressions:
 1. Brackets (or Parentheses)
@@ -152,6 +154,7 @@ Brackets group or disambiguate expressions. You can think of precedence rules as
 - non-associative: `P ↔ Q ↔ R` is an error
 # High to low Precedence
 Function application doesn't have an operator, it's just `function <space> argument`. It has max precedence and is left associative (meaning `and_intro p q` ≡ `(and_intro p) q`).
+### Propositional Operators
 | $Operator$ | $~~~Precedence$ | |
 | :---: | :---: | --- |
 | ¬ | max | |
@@ -159,8 +162,14 @@ Function application doesn't have an operator, it's just `function <space> argum
 | ∨ | 30 | right-associative |
 | → | 25 | right-associative |
 | ↔ | 20 | non-associative |
-| ∃ | _10_ | |
-| ∀ | _05_ | |
+| ∃ | __ | |
+| ∀ | __ | |
+### Expression Operators
+| $Operator$ | $~~~Precedence$ | |
+| :---: | :---: | --- |
+| ≫ | 85 | left-associative |
+| |> | min + 1 | right-associative |
+| <| | min | left-associative |
 ### Example:
 ```
 ¬P ∨ Q ∧ P → Q ↔ Q ∨ R ∨ ¬S
@@ -189,7 +198,7 @@ Here's a version where you can see it aligned
 
 def false_elim {P : Prop} (h : False) : P := h.rec
 
-DefinitionDoc false_elim as "false_elim" "
+DefinitionDoc GameLogic.false_elim as "False elim" "
 If
 ```
 -- Assumptions
@@ -204,7 +213,7 @@ will allow you to write any well formed proposition in place of `T`. This makes
 
 def or_inl {P Q : Prop} (p : P) : Or P Q := Or.inl p
 
-DefinitionDoc or_inl as "or_inl" "
+DefinitionDoc GameLogic.or_inl as "∨ intro left" "
 # Or Introduction Left
 Turns evidence for the lefthand of an `∨` proposition into a disjunction. The context must supply what the righthand side of the disjunction is.
 ```
@@ -223,7 +232,7 @@ have h := show P ∨ Q from or_inl p
 
 def or_inr {P Q : Prop} (q : Q) : Or P Q := Or.inr q
 
-DefinitionDoc or_inr as "or_inr" "
+DefinitionDoc GameLogic.or_inr as "∨ intro right" "
 # Or Introduction Right
 Turns evidence for the righthand of an `∨` proposition into a disjunction. The context must supply what the lefthand side of the disjunction is.
 ```
@@ -247,7 +256,7 @@ def or_elim
   (right : Q → R) : R :=
     Or.elim h left right
 
-DefinitionDoc or_elim as "or_elim" "
+DefinitionDoc GameLogic.or_elim as "∨ elim" "
 # Or Elimination
 If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
 
@@ -269,3 +278,25 @@ qr : Q → R
 have r : R := or_elim pvq pr qr
 ```
 "
+
+def iff_intro
+  {P Q : Prop}
+  (hpq: P → Q)
+  (hqp: Q → P) : P ↔ Q :=
+    Iff.intro hpq hqp
+
+DefinitionDoc GameLogic.iff_intro as "↔ intro" "
+  TODO 8888
+"
+
+def iff_mp {P Q : Prop} (h : P ↔ Q) : P → Q := h.mp
+
+DefinitionDoc GameLogic.iff_mp as "↔ elim mp" "
+  TODO 1234
+"
+
+def iff_mpr {P Q : Prop} (h : P ↔ Q) : Q → P := h.mpr
+
+DefinitionDoc GameLogic.iff_mpr as "↔ elim mpr" "
+  TODO 4321
+"
diff --git a/Game/Doc/Lemmas.lean b/Game/Doc/Lemmas.lean
index 863939c..e1b764d 100755
--- a/Game/Doc/Lemmas.lean
+++ b/Game/Doc/Lemmas.lean
@@ -1,8 +1,14 @@
 import GameServer.Commands
 
+namespace GameLogic
+
+def foo_bar(h : α) : α := h
+
+LemmaDoc GameLogic.foo_bar as "fb" in "∩" "TODO"
+
 def modus_ponens {P Q : Prop} (hpq: P → Q) (p: P) : Q := hpq p
 
-LemmaDoc modus_ponens as "modus_ponens" in "→" "
+LemmaDoc GameLogic.modus_ponens as "modus_ponens" in "→" "
 In this game, the deductive rule *modus_ponens* is just function application.
 ```
 intro h : A ∧ B
@@ -37,7 +43,7 @@ def and_comm {P Q : Prop}: P ∧ Q ↔ Q ∧ P :=
     λ⟨l,r⟩ ↦ ⟨r,l⟩
   ⟩
 
-LemmaDoc and_comm as "and_comm" in "↔" "
+LemmaDoc GameLogic.and_comm as "and_comm" in "↔" "
 # ∧ is commutative
 
 `and_comm` is evidence that `P ∧ Q ↔ Q ∧ P`
@@ -53,7 +59,7 @@ def or_comm {P Q : Prop}: P ∨ Q ↔ Q ∨ P :=
     (Or.elim · Or.inr Or.inl)
   ⟩
 
-LemmaDoc or_comm as "or_comm" in "↔" "
+LemmaDoc GameLogic.or_comm as "or_comm" in "↔" "
 # ∨ is commutative
 
 `or_comm` is evidence that `P ∨ Q ↔ Q ∨ P`
@@ -94,7 +100,7 @@ example {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R := by
 
 def imp_trans {P Q R : Prop} (hpq : P → Q) (hqr : Q → R) (p : P): R := hqr (hpq p)
 
-LemmaDoc imp_trans as "imp_trans" in "→" "
+LemmaDoc GameLogic.imp_trans as "imp_trans" in "→" "
 # → is transitive
 `P → Q` and `Q → R` implies `P → R`
 ```
@@ -110,15 +116,14 @@ Of course, because of `and_comm`, you know you can flip this around too.
 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.
 "
 
-infixl:85 " ≫ " => λa b ↦ Function.comp b a -- type as \gg
-
+infixl:85 " ≫ " => λa b ↦ Function.comp b a  -- type as \gg
 
 def not_not_not {P : Prop}: ¬¬¬P ↔ ¬P := ⟨
   (λh p ↦ h (λnp ↦ np p)),
-  (λh np ↦ np h)
+  (λnp nnp ↦ nnp $ np)
 ⟩
 
-LemmaDoc not_not_not as "not_not_not" in "↔" "
+LemmaDoc GameLogic.not_not_not as "not_not_not" in "↔" "
 # Negation is stable
 A nice result of this theorem is that any more than 2 negations can be simplified down to 1 or 2 negations.
 ```
@@ -126,7 +131,9 @@ not_not_not : ¬¬¬P ↔ ¬P
 ```
 "
 
-LemmaDoc mt as "mt" in "→" "
+def mt {P Q : Prop} (h: P → Q) (nq: ¬Q) : ¬P := h ≫ nq
+
+LemmaDoc GameLogic.mt as "mt" in "→" "
 # Modus Tollens
 Denying the consequent. We've given this theorem an extra short name because it appears so often.
 
@@ -143,7 +150,7 @@ mt : (P → Q) → ¬Q → ¬P
 
 def identity {P : Prop}(p : P) : P := p
 
-LemmaDoc identity as "identity" in "→" "
+LemmaDoc GameLogic.identity as "identity" in "→" "
 # Propositional Identity
 This is the \"I think therefore I am\" of propositional logic. Like `True` it is a simple tautology whose truth requires no premises or assumptions — only reason alone.
 ```
diff --git a/Game/Doc/Tactics.lean b/Game/Doc/Tactics.lean
index ea0a86e..af8d216 100755
--- a/Game/Doc/Tactics.lean
+++ b/Game/Doc/Tactics.lean
@@ -90,3 +90,54 @@ Goal:
 ¬P
 ```
 "
+
+TacticDoc rw "
+## Summary
+
+If `h` is a proof of an equality `X = Y`, then `rw [h]` will change
+all `X`s in the goal to `Y`s. It's the way to \"substitute in\".
+
+## Variants
+
+* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)
+
+* `rw [h1, h2]` (a sequence of rewrites)
+
+* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)
+
+* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;
+get the `⊢` symbol with `\\|-`.)
+
+* `repeat rw [add_zero]` will keep changing `? + 0` to `?`
+until there are no more matches for `? + 0`.
+
+* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.
+"
+
+TacticDoc «repeat» "
+## Summary
+
+`repeat t` repeatedly applies the tactic `t`
+to the goal. You don't need to use this
+tactic, it just speeds things up sometimes.
+
+## Example
+
+`repeat rw [add_zero]` will turn the goal
+`a + 0 + (0 + (0 + 0)) = b + 0 + 0`
+into the goal
+`a = b`.
+"
+
+TacticDoc nth_rewrite "
+## Summary
+
+If `h : X = Y` and there are several `X`s in the goal, then
+`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.
+
+## Example
+
+If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
+will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
+will change the goal to `succ 1 + succ 1 = 4`.
+"
diff --git a/Game/Levels/AndIntro/L01.lean b/Game/Levels/AndIntro/L01.lean
index 5c84930..0b82d1c 100755
--- a/Game/Levels/AndIntro/L01.lean
+++ b/Game/Levels/AndIntro/L01.lean
@@ -1,12 +1,13 @@
-
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 1
 Title "Exactly! It's in the premise"
 
 NewTactic exact
-NewDefinition AsciiTable
+NewDefinition GameLogic.AsciiTable
 
 Introduction "
 # Introduction
diff --git a/Game/Levels/AndIntro/L02.lean b/Game/Levels/AndIntro/L02.lean
index 96dd9a5..82fef46 100755
--- a/Game/Levels/AndIntro/L02.lean
+++ b/Game/Levels/AndIntro/L02.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 2
 Title "And Introduction"
 
-NewDefinition and_intro
+NewDefinition GameLogic.and_intro
 
 Introduction "
 # Sending Invitations in a Single Package
@@ -37,6 +39,7 @@ Statement (P S : Prop)(p: P)(s : S) : P ∧ S := by
   Hint (hidden := true) "exact and_intro p s"
   exact and_intro (left := p) (right := s)
 
+
 Conclusion "
 You've got evidence that Paul and Sarah are invited to the party.\\
 \\
diff --git a/Game/Levels/AndIntro/L03.lean b/Game/Levels/AndIntro/L03.lean
index a8882fc..e7aaa2c 100755
--- a/Game/Levels/AndIntro/L03.lean
+++ b/Game/Levels/AndIntro/L03.lean
@@ -1,10 +1,13 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 3
 Title "The Have Tactic"
 
-NewDefinition Precedence
+NewDefinition GameLogic.Precedence
+NewTactic «have»
 
 Introduction "
 # Too Many Invites
@@ -44,8 +47,6 @@ ou: O ∧ U
 Finally, now you can place these two boxes — `ai` and `ou` — into a third box and submit your answer using the `exact` tactic.
 "
 
-NewTactic «have»
-
 /-- Three × and_intro. -/
 Statement (A I O U : Prop)(a : A)(i : I)(o : O)(u : U) : (A ∧ I) ∧ O ∧ U := by
   have ai := and_intro a i
diff --git a/Game/Levels/AndIntro/L04.lean b/Game/Levels/AndIntro/L04.lean
index a9343c3..7140a82 100755
--- a/Game/Levels/AndIntro/L04.lean
+++ b/Game/Levels/AndIntro/L04.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 4
 Title "And Elimination"
 
-NewDefinition and_left
+NewDefinition GameLogic.and_left
 
 Introduction "
 # Using Only What Is Needed
diff --git a/Game/Levels/AndIntro/L05.lean b/Game/Levels/AndIntro/L05.lean
index f0a030a..82cd421 100755
--- a/Game/Levels/AndIntro/L05.lean
+++ b/Game/Levels/AndIntro/L05.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 5
 Title "And Elimination 2"
 
-NewDefinition and_right
+NewDefinition GameLogic.and_right
 
 Introduction "
 # Another Unlock
diff --git a/Game/Levels/AndIntro/L06.lean b/Game/Levels/AndIntro/L06.lean
index 8366115..3e5bf59 100755
--- a/Game/Levels/AndIntro/L06.lean
+++ b/Game/Levels/AndIntro/L06.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 6
 Title "Mix and Match"
diff --git a/Game/Levels/AndIntro/L07.lean b/Game/Levels/AndIntro/L07.lean
index df9434d..d677f01 100755
--- a/Game/Levels/AndIntro/L07.lean
+++ b/Game/Levels/AndIntro/L07.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 7
 Title "More Elimination"
diff --git a/Game/Levels/AndIntro/L08.lean b/Game/Levels/AndIntro/L08.lean
index 70dd570..cd2e69f 100755
--- a/Game/Levels/AndIntro/L08.lean
+++ b/Game/Levels/AndIntro/L08.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 8
 Title "Rearranging Boxes"
diff --git a/Game/Levels/IffIntro.lean b/Game/Levels/IffIntro.lean
index d7ff44c..8b607d3 100644
--- a/Game/Levels/IffIntro.lean
+++ b/Game/Levels/IffIntro.lean
@@ -1,9 +1,18 @@
 import Game.Levels.IffIntro.L01
+import Game.Levels.IffIntro.L02
 
 World "IffIntro"
 Title "↔ Tutorial"
 
 Introduction "
-# Propositional Equality
-## If and only iff
+# Propositional Equivalence
+## Biconditional: If and only if
+The `↔` operator doesn't introduce anything new. `P ↔ Q` can be constructed whenever evidence for both `P → Q` and `Q → P` is available. In general, if `h₁` and `h₂` are evidence as follows:
+```
+h₁ : P ↔ Q
+h₂ : (P → Q) ∧ (Q → P)
+```
+Then `h₁` and `h₂` have roughly the same capabilities. Also, proof of either P or Q or ¬P or ¬Q, immediately translates to the same proof for the logically equivalent proposition. The following levels will explain the details.\\
+\\
+The main new idea introduced in this tutorial world is the `rw` tactic. The *rewrite* tactic offers a principled way to alter the current goal or available hypotheses of your current proof state.
 "
diff --git a/Game/Levels/IffIntro/L01.lean b/Game/Levels/IffIntro/L01.lean
index 380e513..d454438 100755
--- a/Game/Levels/IffIntro/L01.lean
+++ b/Game/Levels/IffIntro/L01.lean
@@ -1,21 +1,43 @@
 import Game.Metadata
 
+open GameLogic
+
 World "IffIntro"
 Level 1
-Title "Title"
+Title "Iff_Intro"
+
+NewTactic rw
+NewHiddenTactic «repeat» nth_rewrite
+NewDefinition GameLogic.iff_intro
 
 Introduction "
-# Flavor Title
-Flavor Text
+# Coupled Conditionals
+Sarah and Jason are a couple. In effect, this means that if Sarah is attending the party, then Jason is attending and vise versa. Therefore Sarah is attending if and only if Jason is attending.
 # Proposition Key:
-- P — Pig
-- Q — Quack
+- J — Jason is attending
+- S — Sarah is attending
+# Unlocked `↔ intro`
+Assuming `e₁ : P → Q` and `e₂ : Q → P`, you can introduce a biconditional with `have h := iff_intro e₁ e₂`, though the anonymous constructor syntax works just like it does for conjunctions: `have h : P ↔ Q := ⟨e₁, e₂⟩`
 "
 
 /-- Statement -/
-Statement: ¬False := by
-  exact identity
+Statement (J S : Prop) (hsj: S → J) (hjs: J → S) : S ↔ J := by
+  exact iff_intro hsj hjs
+
+example (J S : Prop) (hsj: S → J) (hjs: J → S) : S ↔ J := by
+  exact ⟨hsj, hjs⟩
 
 Conclusion "
 Onward and upward
+
+----
+```
+exact iff_intro hsj hjs
+```
+---
+```
+exact ⟨hsj, hjs⟩
+```
 "
+
+-- example (P Q : Prop): (P ∧ Q) ∨ (¬P ∧ ¬Q) → (P → Q) ∧ (Q → P) := by tauto
diff --git a/Game/Levels/IffIntro/L02.lean b/Game/Levels/IffIntro/L02.lean
new file mode 100644
index 0000000..2f43f86
--- /dev/null
+++ b/Game/Levels/IffIntro/L02.lean
@@ -0,0 +1,29 @@
+import Game.Metadata
+
+open GameLogic
+
+World "IffIntro"
+Level 2
+Title "Title"
+
+NewDefinition GameLogic.iff_mp GameLogic.iff_mpr
+
+Introduction "
+# Two sides to every coin
+You're flipping a coin to decide what color placemats you you want. Heads means blue placemats and tails means purple placemats. Here's the thing, you're secretly hoping it comes up blue.
+# Proposition Key:
+- B — Blue Placemats
+- P — Purple Placemats
+# Unlocked `↔-e mp` and `↔-e mpr`
+For a biconditional like `h : P ↔ Q`,
+1. You can extract `P → Q` using `iff_mp h` or `h.mp`. `mp` here is short of modus ponens.
+2. You can extra `Q → P` using `iff_mpr h` or `h.mpr`. `mpr` here is short of modus ponens reversed.
+"
+
+/-- Statement -/
+Statement (B P : Prop) (h : B ↔ ¬P) : (B → ¬P) ∧ (¬P → B) := by
+  exact and_intro (iff_mp h) (iff_mpr h)
+
+Conclusion "
+Onward and upward
+"
diff --git a/Game/Levels/ImpIntro/L01.lean b/Game/Levels/ImpIntro/L01.lean
index a39e826..a4d1f24 100755
--- a/Game/Levels/ImpIntro/L01.lean
+++ b/Game/Levels/ImpIntro/L01.lean
@@ -1,12 +1,13 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 1
 Title "Cake Delivery Service"
 
-NewDefinition FunElim
-
-NewLemma modus_ponens
+NewDefinition GameLogic.FunElim
+NewLemma GameLogic.modus_ponens
 
 Introduction "
 # Let there be cake!
@@ -52,6 +53,12 @@ Statement (P C: Prop)(p: P)(bakery_service : P → C) : C := by
   have c := bakery_service p
   exact c
 
+example (P C: Prop)(p: P)(bakery_service : P → C) : C := by
+  exact bakery_service p
+
+example (P C: Prop)(p: P)(bakery_service : P → C) : C := by
+  exact modus_ponens bakery_service p
+
 Conclusion "
 Congratulations. You have evidence that your party will have cake!
 
diff --git a/Game/Levels/ImpIntro/L02.lean b/Game/Levels/ImpIntro/L02.lean
index 439ceb5..5444841 100755
--- a/Game/Levels/ImpIntro/L02.lean
+++ b/Game/Levels/ImpIntro/L02.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 2
 Title "Identity"
 
-NewDefinition FunIntro
+NewDefinition GameLogic.FunIntro
 
 Introduction "
 # Is it Cake!?
diff --git a/Game/Levels/ImpIntro/L03.lean b/Game/Levels/ImpIntro/L03.lean
index d055d4c..1a5dcc5 100755
--- a/Game/Levels/ImpIntro/L03.lean
+++ b/Game/Levels/ImpIntro/L03.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 3
 Title "Cake Form Swap"
 
-NewLemma identity
+NewLemma GameLogic.identity
 
 Introduction "
 # Trouble with the cake
diff --git a/Game/Levels/ImpIntro/L04.lean b/Game/Levels/ImpIntro/L04.lean
index 3a4ae83..87ca0b2 100755
--- a/Game/Levels/ImpIntro/L04.lean
+++ b/Game/Levels/ImpIntro/L04.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 4
 Title "Chain Reasoning"
 
-NewLemma and_comm
+NewLemma GameLogic.and_comm
 
 Introduction "
 # A Chain of Reasoning
diff --git a/Game/Levels/ImpIntro/L05.lean b/Game/Levels/ImpIntro/L05.lean
index e727e03..b4b2289 100755
--- a/Game/Levels/ImpIntro/L05.lean
+++ b/Game/Levels/ImpIntro/L05.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 5
 Title "Robbie Snacks"
 
-NewLemma imp_trans
+NewLemma GameLogic.imp_trans
 
 Introduction "
 # Is Robbie bringing something?
diff --git a/Game/Levels/ImpIntro/L06.lean b/Game/Levels/ImpIntro/L06.lean
index 61c891a..0a14b4d 100755
--- a/Game/Levels/ImpIntro/L06.lean
+++ b/Game/Levels/ImpIntro/L06.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 6
 Title "and_imp"
diff --git a/Game/Levels/ImpIntro/L07.lean b/Game/Levels/ImpIntro/L07.lean
index f3f883b..d68a4ba 100755
--- a/Game/Levels/ImpIntro/L07.lean
+++ b/Game/Levels/ImpIntro/L07.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 7
 Title "and_imp 2"
diff --git a/Game/Levels/ImpIntro/L08.lean b/Game/Levels/ImpIntro/L08.lean
index 1888fbd..c93fdc4 100755
--- a/Game/Levels/ImpIntro/L08.lean
+++ b/Game/Levels/ImpIntro/L08.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 8
 Title "Distribute"
diff --git a/Game/Levels/ImpIntro/L09.lean b/Game/Levels/ImpIntro/L09.lean
index 0c8bbdc..b2e71a5 100755
--- a/Game/Levels/ImpIntro/L09.lean
+++ b/Game/Levels/ImpIntro/L09.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "ImpIntro"
 Level 9
 Title "Uncertain Snacks"
diff --git a/Game/Levels/L01-template.lean b/Game/Levels/L01-template.lean
index 380e513..13a109d 100644
--- a/Game/Levels/L01-template.lean
+++ b/Game/Levels/L01-template.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "IffIntro"
 Level 1
 Title "Title"
diff --git a/Game/Levels/NotIntro.lean b/Game/Levels/NotIntro.lean
index b4d3251..1e7abe4 100755
--- a/Game/Levels/NotIntro.lean
+++ b/Game/Levels/NotIntro.lean
@@ -32,15 +32,3 @@ On casual scrutiny, one might naively conclude that adhering to this contract ma
 \\
 By signing the contract, you're agreeing that “If there appears a number that is both greater than 0 and less 0, then I will transform into a cucumber.” Your grandiose claims remain secure as they hinge on an eventuality that defies logical possibility.\\
 "
--- This is a second double not elim
-example {P : Prop} : ¬¬¬¬P ↔ ¬¬P := ⟨
-  show ¬¬¬¬P → ¬¬P from λnnnp np ↦ nnnp λnnp ↦ nnp np,
-  show ¬¬P → ¬¬¬¬P from λnnp nnnp ↦ nnnp nnp
-⟩
-
-example {P : Prop} : ¬¬¬¬P ↔ ¬¬P := not_not_not
-
-example {P : Prop}(h: ¬¬¬¬¬¬¬P) : ¬P := by
-  have h₁ := not_not_not.mp h
-  have h₂ := not_not_not.mp h₁
-  exact not_not_not.mp h₂
diff --git a/Game/Levels/NotIntro/L01.lean b/Game/Levels/NotIntro/L01.lean
index 4f50a41..9c195d5 100755
--- a/Game/Levels/NotIntro/L01.lean
+++ b/Game/Levels/NotIntro/L01.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 1
 Title "Not False"
diff --git a/Game/Levels/NotIntro/L02.lean b/Game/Levels/NotIntro/L02.lean
index 6139c30..5252c44 100755
--- a/Game/Levels/NotIntro/L02.lean
+++ b/Game/Levels/NotIntro/L02.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 2
 Title "False implies anything"
 
-NewDefinition false_elim
+NewDefinition GameLogic.false_elim
 
 Introduction "
 # Sarah's Punctuality
diff --git a/Game/Levels/NotIntro/L03.lean b/Game/Levels/NotIntro/L03.lean
index e71fb6b..eab7bed 100755
--- a/Game/Levels/NotIntro/L03.lean
+++ b/Game/Levels/NotIntro/L03.lean
@@ -1,6 +1,7 @@
-
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 3
 Title "Double False!"
diff --git a/Game/Levels/NotIntro/L04.lean b/Game/Levels/NotIntro/L04.lean
index a37543f..2acec67 100755
--- a/Game/Levels/NotIntro/L04.lean
+++ b/Game/Levels/NotIntro/L04.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 4
 Title "Self Contradictory"
diff --git a/Game/Levels/NotIntro/L05.lean b/Game/Levels/NotIntro/L05.lean
index 970d259..ce8357d 100755
--- a/Game/Levels/NotIntro/L05.lean
+++ b/Game/Levels/NotIntro/L05.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 5
 Title "Modus Tollens"
diff --git a/Game/Levels/NotIntro/L06.lean b/Game/Levels/NotIntro/L06.lean
index caf3b39..2803be4 100755
--- a/Game/Levels/NotIntro/L06.lean
+++ b/Game/Levels/NotIntro/L06.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 6
 Title "Jason"
 
-NewLemma mt
+NewLemma GameLogic.mt
 
 Introduction "
 # The Jason Effect
diff --git a/Game/Levels/NotIntro/L07.lean b/Game/Levels/NotIntro/L07.lean
index 28cdf12..d39f138 100755
--- a/Game/Levels/NotIntro/L07.lean
+++ b/Game/Levels/NotIntro/L07.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 7
 Title "Negation"
diff --git a/Game/Levels/NotIntro/L08.lean b/Game/Levels/NotIntro/L08.lean
index e9e4280..6b8fbb1 100755
--- a/Game/Levels/NotIntro/L08.lean
+++ b/Game/Levels/NotIntro/L08.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 8
 Title "Negated Conjunction"
diff --git a/Game/Levels/NotIntro/L09.lean b/Game/Levels/NotIntro/L09.lean
index 9363fa8..e024204 100755
--- a/Game/Levels/NotIntro/L09.lean
+++ b/Game/Levels/NotIntro/L09.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 9
 Title "Implies a Negation"
diff --git a/Game/Levels/NotIntro/L10.lean b/Game/Levels/NotIntro/L10.lean
index 0baf644..1fa0daa 100755
--- a/Game/Levels/NotIntro/L10.lean
+++ b/Game/Levels/NotIntro/L10.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 10
 Title "Conjunction Implicaiton"
diff --git a/Game/Levels/NotIntro/L11.lean b/Game/Levels/NotIntro/L11.lean
index 5dc6a15..c9de617 100755
--- a/Game/Levels/NotIntro/L11.lean
+++ b/Game/Levels/NotIntro/L11.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 11
 Title "not_not_not"
diff --git a/Game/Levels/NotIntro/L12.lean b/Game/Levels/NotIntro/L12.lean
index de8909a..57ed5ee 100755
--- a/Game/Levels/NotIntro/L12.lean
+++ b/Game/Levels/NotIntro/L12.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "NotIntro"
 Level 12
 Title "¬Intro Boss"
 
-NewLemma not_not_not
+NewLemma GameLogic.not_not_not
 
 Introduction "
 # BOSS Level
diff --git a/Game/Levels/OrIntro.lean b/Game/Levels/OrIntro.lean
index a54df5b..956ff49 100755
--- a/Game/Levels/OrIntro.lean
+++ b/Game/Levels/OrIntro.lean
@@ -8,7 +8,7 @@ import Game.Levels.OrIntro.L07
 import Game.Levels.OrIntro.L08
 
 World "OrIntro"
-Title "∨ Tutorial"
+Title "∨ Tutorial: The Kraken"
 
 Introduction "
 # The ∨ Tutorial World!
diff --git a/Game/Levels/OrIntro/L01.lean b/Game/Levels/OrIntro/L01.lean
index f372d1b..0d1ca3b 100755
--- a/Game/Levels/OrIntro/L01.lean
+++ b/Game/Levels/OrIntro/L01.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 1
 Title "Left Evidence"
 
-NewDefinition or_inl
+NewDefinition GameLogic.or_inl
 
 Introduction "
 # Or Introduction Left
diff --git a/Game/Levels/OrIntro/L02.lean b/Game/Levels/OrIntro/L02.lean
index 9e43813..c4b699d 100755
--- a/Game/Levels/OrIntro/L02.lean
+++ b/Game/Levels/OrIntro/L02.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 2
 Title "Right Evidence"
 
-NewDefinition or_inr
+NewDefinition GameLogic.or_inr
 
 Introduction "
 # Or Introduction Right
diff --git a/Game/Levels/OrIntro/L03.lean b/Game/Levels/OrIntro/L03.lean
index 86aa93a..e15dfc3 100755
--- a/Game/Levels/OrIntro/L03.lean
+++ b/Game/Levels/OrIntro/L03.lean
@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 3
 Title "Or Elimination"
 
-NewDefinition or_elim
+NewDefinition GameLogic.or_elim
 
 Introduction "
 # Party Games
diff --git a/Game/Levels/OrIntro/L04.lean b/Game/Levels/OrIntro/L04.lean
index 73f3d3c..e3b7586 100755
--- a/Game/Levels/OrIntro/L04.lean
+++ b/Game/Levels/OrIntro/L04.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 4
 Title "Or is Commutative"
@@ -12,6 +14,10 @@ Chocolate chip oatmeal cookies, which ingredient goes first?
 # Proposition Key:
 C — Chocolate chips
 O — Oatmeal
+
+This time they're not under assumptions, but you have the evidence in your inventory.
+- `or_inr : C → O ∨ C`
+- `or_inl : O → O ∨ C`
 "
 
 /-- Commutativity of "`∨`" -/
@@ -20,8 +26,8 @@ Statement (C O : Prop)(h : C ∨ O) : O ∨ C := by
 
 Conclusion "
 Well, done.
+
 ---
-This one is nice becuase the `→`s you need already have names!
 ```
 exact or_elim h or_inr or_inl
 ```
diff --git a/Game/Levels/OrIntro/L05.lean b/Game/Levels/OrIntro/L05.lean
index ffc62af..3968711 100755
--- a/Game/Levels/OrIntro/L05.lean
+++ b/Game/Levels/OrIntro/L05.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 5
 Title "Carry On Effects"
@@ -18,5 +20,5 @@ Statement (C J R : Prop)(h₁ : C → J)(h₂ : C ∨ R) : J ∨ R := by
   exact or_elim h₂ (h₁ ≫ or_inl) or_inr
 
 Conclusion "
-Concluded
+Well done, you're getting good at this!
 "
diff --git a/Game/Levels/OrIntro/L06.lean b/Game/Levels/OrIntro/L06.lean
index c80f940..3c6fbef 100755
--- a/Game/Levels/OrIntro/L06.lean
+++ b/Game/Levels/OrIntro/L06.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 6
 Title "or distributes over and"
@@ -18,9 +20,34 @@ Statement (G H U : Prop)(h : G ∨ H ∧ U) : (G ∨ H) ∧ (G ∨ U) := by
   have fg : G → (G ∨ H) ∧ (G ∨ U) :=
     λg ↦ ⟨or_inl g, or_inl g⟩
   have fhu : H ∧ U → (G ∨ H) ∧ (G ∨ U) :=
-    λhu ↦ ⟨or_inr hu.left,or_inr hu.right⟩
+    λhu ↦ ⟨or_inr hu.left, or_inr hu.right⟩
   exact or_elim h fg fhu
 
+example (G H U : Prop)(h : G ∨ H ∧ U) : (G ∨ H) ∧ (G ∨ U) := by
+  exact or_elim h
+    (λg ↦ ⟨or_inl g, or_inl g⟩)
+    λhu ↦ ⟨or_inr hu.left, or_inr hu.right⟩
+
 Conclusion "
-Concluded
+As proof terms start getting bigger, it makes more sense to use Editor mode instead of typewritter mode.
+
+----
+```
+exact or_elim h
+  (λg ↦ ⟨or_inl g, or_inl g⟩)
+  (λhu ↦ ⟨or_inr hu.left, or_inr hu.right⟩)
+```
+You can split this up a bit, but you'll need to write out a lot of propositions in full.
+```
+-- the case for g
+have fg : G → (G ∨ H) ∧ (G ∨ U) :=
+    λg ↦ ⟨or_inl g, or_inl g⟩
+
+-- the case for H ∧ U
+have fhu : H ∧ U → (G ∨ H) ∧ (G ∨ U) :=
+    λhu ↦ ⟨or_inr hu.left, or_inr hu.right⟩
+
+-- Finish it out with or_elim
+exact or_elim h fg fhu
+```
 "
diff --git a/Game/Levels/OrIntro/L07.lean b/Game/Levels/OrIntro/L07.lean
index b08f972..12191a6 100755
--- a/Game/Levels/OrIntro/L07.lean
+++ b/Game/Levels/OrIntro/L07.lean
@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 7
 Title "and distributes over or"
@@ -22,6 +24,18 @@ Statement (G H U : Prop)(h : G ∧ (H ∨ U)) : (G ∧ H) ∨ (G ∧ U) := by
     λx ↦ or_inr ⟨h.left, x⟩
   exact or_elim hvu ffh ffu
 
+example (G H U : Prop)(h : G ∧ (H ∨ U)) : (G ∧ H) ∨ (G ∧ U) := by
+  exact or_elim h.right
+    (and_intro h.left ≫ or_inl)
+    (and_intro h.left ≫ or_inr)
+
 Conclusion "
-Concluded
+This is a great example of how the infix `imp_trans` operator can streamline a level:
+
+---
+```lean
+exact or_elim h.right
+  (and_intro h.left ≫ or_inl)
+  (and_intro h.left ≫ or_inr)
+```
 "
diff --git a/Game/Levels/OrIntro/L08.lean b/Game/Levels/OrIntro/L08.lean
index f58f988..d6c52b3 100755
--- a/Game/Levels/OrIntro/L08.lean
+++ b/Game/Levels/OrIntro/L08.lean
@@ -1,22 +1,24 @@
 import Game.Metadata
 
+open GameLogic
+
 World "OrIntro"
 Level 8
 Title "The Implication"
 
 Introduction "
 # BOSS LEVEL
-If we summon the Kraken, then we shall assuredly perish. Sure that sounds bad, but soncider that if we summon the Kraken or have icecream, then we shall perish or (hear me out here) **have icecream!**.
+If we summon the Kraken, then we shall assuredly perish. While that might sound ominous, consider this: if we summon the Kraken or **have icecream**, then we shall **have icecream!** or we shall perish.
 # Proposition Key:
-- I — We have have icecream!
+- I — **We have have icecream!**
 - K — We summon the Kraken
 - P — We shall assuredly perish
 "
 
 /-- Implication of ∨ -/
-Statement (I K P : Prop)(h : K → P) : K ∨ I → P ∨ I := by
-  exact λpvr ↦ or_elim pvr (h ≫ or_inl) or_inr
+Statement (I K P : Prop)(h : K → P) : K ∨ I → I ∨ P := by
+  exact (or_elim · (h ≫ or_inr) or_inl)
 
 Conclusion "
-Concluded
+Okay, that was a bit easy for a boss level. Don't sweat it, just enjoy the icecream!
 "