From 3ff3c7eb6926c100257fab4624013137523160c5 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 10 Mar 2023 19:21:17 +0100
Subject: [PATCH] story world 2

---
 server/testgame/TestGame/LemmaDocs.lean       |  3 +
 .../testgame/TestGame/Levels/Implication.lean |  5 +-
 .../Levels/Implication/L01_Intro.lean         |  4 +-
 .../Levels/Implication/L02_Revert.lean        |  8 +-
 .../Levels/Implication/L03_Apply.lean         | 18 ++---
 .../Levels/Implication/L04_Apply.lean         | 17 ++--
 .../Levels/Implication/L05_Apply.lean         | 39 ++++-----
 .../TestGame/Levels/Implication/L06_Iff.lean  | 39 ++++-----
 .../TestGame/Levels/Implication/L07_Rw.lean   | 73 +++++------------
 .../TestGame/Levels/Implication/L08_Iff.lean  | 42 +++++-----
 .../TestGame/Levels/Implication/L09_Iff.lean  | 33 ++++----
 .../Levels/Implication/L10_Apply.lean         | 26 +++---
 .../Levels/Implication/L11_ByCases.lean       | 38 +++++++++
 .../TestGame/Levels/Implication/L11_Rw.lean   | 39 ---------
 .../TestGame/Levels/Implication/L12_Rw.lean   | 50 ++++++++++++
 .../Levels/Implication/L12_Summary.lean       | 81 -------------------
 .../Levels/Implication/L13_Summary.lean       | 63 +++++++++++++++
 17 files changed, 285 insertions(+), 293 deletions(-)
 create mode 100644 server/testgame/TestGame/Levels/Implication/L11_ByCases.lean
 delete mode 100644 server/testgame/TestGame/Levels/Implication/L11_Rw.lean
 create mode 100644 server/testgame/TestGame/Levels/Implication/L12_Rw.lean
 delete mode 100644 server/testgame/TestGame/Levels/Implication/L12_Summary.lean
 create mode 100644 server/testgame/TestGame/Levels/Implication/L13_Summary.lean

diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index 92ae7b7..7492cef 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -201,3 +201,6 @@ LemmaDoc congrArg as congrArg in "Function"
 ""
 LemmaDoc congrFun as congrFun in "Function"
 ""
+
+LemmaDoc Iff.symm as Iff.symm in "Logic"
+""
diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean
index cf41c7a..0d06e71 100644
--- a/server/testgame/TestGame/Levels/Implication.lean
+++ b/server/testgame/TestGame/Levels/Implication.lean
@@ -8,8 +8,9 @@ import TestGame.Levels.Implication.L07_Rw
 import TestGame.Levels.Implication.L08_Iff
 import TestGame.Levels.Implication.L09_Iff
 import TestGame.Levels.Implication.L10_Apply
-import TestGame.Levels.Implication.L11_Rw
-import TestGame.Levels.Implication.L12_Summary
+import TestGame.Levels.Implication.L11_ByCases
+import TestGame.Levels.Implication.L12_Rw
+import TestGame.Levels.Implication.L13_Summary
 
 Game "TestGame"
 World "Implication"
diff --git a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
index ffedd93..7a60817 100644
--- a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
+++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
@@ -27,7 +27,7 @@ Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
   assumption
   assumption
 
+Conclusion "Der Operationsleiter nickt bedacht."
+
 NewTactic intro
 DisabledTactic tauto
-
-Conclusion "Der Operationsleiter nickt bedacht."
diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
index 03551fb..f05a5c9 100644
--- a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
+++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
@@ -11,7 +11,7 @@ Title "Revert"
 Introduction
 "Jemand aus der Gruppe gibt dir ein Blatt Papier mit einer Zeile Text:"
 
-Statement "" (A B : Prop) (ha : A) (h : A → B) : B := by
+Statement (A B : Prop) (ha : A) (h : A → B) : B := by
   Hint "**Robo**: Mit `revert {ha}` kann man die Annahme `ha` als
   Implikationsprämisse vorne ans Goal anhängen, dann ist das Goal `{A} → {B}`.
 
@@ -21,10 +21,10 @@ Statement "" (A B : Prop) (ha : A) (h : A → B) : B := by
   revert ha
   assumption
 
-NewTactic revert
-DisabledTactic tauto
-
 Conclusion "**Du**: Aber das müsste doch auch anders gehen, ich hätte jetzt intuitiv
 die Implikation $A \\Rightarrow B$ angewendet und behauptet, dass es genügt $A$ zu zeigen…
 
 Daraufhin lächelt der Fragende nur vorahnend."
+
+NewTactic revert
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
index 9705197..5d917f4 100644
--- a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
@@ -20,25 +20,21 @@ Wenn man eine Implikation `(g : A → B)` in den Annahmen hat, bei welcher die K
 (also $B$) mit dem Goal übereinstimmt, kann man `apply g` genau dies machen.
 "
 
-Statement "" (A B : Prop) (hA : A) (h : A → B) : B := by
+Statement (A B : Prop) (hA : A) (h : A → B) : B := by
+  Hint "**Robo**: Du hast natürlich recht, normalerweise ist es viel schöner mit
+  `apply {h}` die Implikation anzuwenden."
   apply h
+  Hint "**Du**: Und jetzt genügt es also `A` zu zeigen."
   assumption
 
-NewTactic apply
-DisabledTactic revert tauto
-
-Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
-"**Robo**: Du hast natürlich recht, normalerweise ist es viel schöner mit
-`apply {h}` die Implikation anzuwenden."
-
-Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
-"**Du**: Und jetzt genügt es also `A` zu zeigen."
-
 Conclusion "**Robo** Übrigens mit `apply LEMMA` kannst auch jedes Lemma anwenden, dessen
 Aussage mit dem Goal übereinstimmt.
 
 Die beiden Fragenden schauen das Blatt an und murmeln zustimmend."
 
+NewTactic apply
+DisabledTactic revert tauto
+
 -- Katex notes
 -- `\\(    \\)` or `$   $` for inline
 -- and `$$  $$` block.
diff --git a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
index 42747fe..1d4a7a9 100644
--- a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
@@ -20,20 +20,19 @@ Gesteuert werden diese über Panels, und hier hab ich das Übungspanel, mit dem
 Ingeneure ausbilden:
 "
 
-Statement "" (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+Statement (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+  Hint "**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
+  kombinieren?
+
+  **Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch."
   intro hA
+  Hint (hidden := true) "**Robo**: Das ist wieder eine Anwendung von `apply`."
   apply g
   apply f
   assumption
 
-Hint (A B C : Prop) (f : A → B) (g : B → C) : A → C =>
-"**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
-kombinieren?
-
-**Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch.
-"
+Conclusion "**Du**: Ich hab das Konzept verstanden.
 
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
-"**Robo**: Das ist wieder eine Anwendung von `apply`."
+Die Mitarbeiterin ist zufrieden und wünscht euch Glück auf der Mission."
 
 DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
index 566198c..78b48cc 100644
--- a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
@@ -22,43 +22,32 @@ $$
 "
 
 Statement
-    "Beweise $A \\Rightarrow F$."
     (A B C D E F G H I : Prop)
     (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
     (n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
+  Hint "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
+
+  **Robo**: Und dann fängst du am besten wieder mit `intro` an."
   intro ha
+  Branch
+    apply r
+    Hint "**Robo**: Das sieht nach einer Sackgasse aus…"
+  Hint (hidden := true) "**Robo**: Na wieder `apply`, was sonst."
   apply p
   apply k
   apply h
+  Branch
+    apply g
+    Hint "**Robo**: Nah, da stimmt doch was nicht…"
   apply f
   assumption
 
-Hint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
-    (n : H → E) (p : F → I) (q : H → G) (r : H → I)  : A → I =>
-"**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
-
-**Robo**: Und dann fängst du am besten wieder mit `intro` an."
-
-HiddenHint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
-    (n : H → E) (p : F → I) (q : H → G) (r : H → I) (a : A) : I =>
-"**Robo**: Na wieder `apply`, was sonst."
-
--- TODO: Dieser wird falscherweise bei `F` angezeigt
-Hint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
-    (n : H → E) (p : F → I) (q : H → G) (r : H → I) (a : A) : H =>
-"**Robo**: Das sieht nach einer Sackgasse aus…"
+Conclusion
+"Mit einem lauten Ratteln springen die Förderbänder wieder an.
 
-Hint (A B C D E F G H I : Prop)
-    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
-    (n : H → E) (p : F → I) (q : H → G) (r : H → I) (a : A) : C =>
-"**Robo**: Nah, da stimmt doch was nicht…"
+**Operationsleiter**: Vielen Dank euch! Kommt ich geb euch eine Führung und stell euch den
+Technikern hier vor."
 
 DisabledTactic tauto
 
-Conclusion
-"Mit einem lauten Ratteln springen die Förderbänder wieder an."
-
 -- https://www.jmilne.org/not/Mamscd.pdf
diff --git a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
index 3291e10..9e87b93 100644
--- a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
@@ -8,36 +8,37 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Genau-dann-wenn, $A \\Leftrightarrow B$, wird als `A ↔ B` (`\\iff`) geschrieben.
-`A ↔ B` ist eine Struktur (ähnlich wie das logische UND), die aus zwei Teilen besteht:
+Als erstes kommt ihr in einen kleinen Raum mit ganz vielen Bildschirmen.
 
-- `mp`: die Implikation $A \\Rightarrow B$.
-- `mpr`: die Implikation $B \\Rightarrow A$.
+Ein junges Wesen dreht sich auf dem Stuhl um, und sagt:
 
-Hat man ein $\\Leftrightarrow$ im Goal, nimmt man dieses ebenfalls mit der Taktik
-`constructor` auseinander und zeigt dann beide Richtungen einzeln.
+**Mitarbeiter**: Oh hallo! Schaut euch mal das hier an!
 "
 
-Statement
-    "Zeige dass `B ↔ C`."
-    (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
+Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
+  Hint "**Robo**: Das ist ein genau-dann-wenn Pfeil: `\\iff`. Er besteht aus zwei Teilen:
+  `A ↔ B` ist als `⟨A → B, B → A⟩` definiert.
+
+  **Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
+
+  **Robo**: Genau. Entsprechend kannst du hier auch mit `constructor` anfangen."
   constructor
+  Hint "**Du**: Ah und die beiden hab ich schon in den Annahmen."
   assumption
   assumption
 
-HiddenHint (A : Prop) (B : Prop) : A ↔ B =>
-"Eine Struktur wie `A ↔ B` kann man mit `constructor` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (h : A → B) : A → B =>
-"Such mal in den Annahmen."
-
 Conclusion
 "
-Die Taktik `constructor` heisst so, weil `↔` als \"Struktur\" definiert ist, die
-aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean, es soll versuchen,
-ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
+**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheissen,
+hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`.
+
+**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
+
+**Operationsleiter**: Das steht Modulo Ponens, aber das ist doch nicht wichtig. Und das \"r\"
+  steht für \"reverse\" weils die Gegenrichtung ist.
 "
 
-NewTactic constructor assumption
+NewTactic constructor
+DisabledTactic tauto rw
 
 -- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
diff --git a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
index 0f17917..a224432 100644
--- a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
+++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
@@ -11,64 +11,35 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Hat man ein `(h : A ↔ B)` in den Annahmen, hat man die gleichen beiden Optionen wie beim
-logischen UND plus noch eine neue:
+Als nächstes begenet ihr jemandem im Flur.
 
-1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen
-   direkt auswählen.
-2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei
-   separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)`
-3. **Mit** `rw [h]` **kann man im Goal `A` durch `B` ersetzen.**
-
-Wir widmen uns zuerst `rw`. Dies steht für \"rewrite\". Da $A$ und $B$ logisch äquivalent
-sind, kann man beliebig das eine mit dem anderen vertauschen.
-`rw [h]` ersetzt $A$ durch $B$.
-Dabei gibt es noch einige Tricks:
-
-- `rw [← h]` ersetzt umgekehrt $B$ durch $A$ (`\\l`, kleines L).
-- `rw [h, g]` ist das gleiche wie `rw [h]` gefolgt von `rw [g]`.
+Dieser hat schon von euch gehört und will sofort wissen, ob ihr ihm helfen könnt:
 "
 
-Statement
-    "Zeige dass `B ↔ C`."
-    (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
-  rw [h₁]
-  rw [←h₂]
-  assumption
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C =>
-"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
-Probiers doch mit `rw [h₁]`."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : A ↔ C =>
-"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
-Probiers doch mit `rw [h₁]`."
+Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
+  Hint "**Du**: $B \\iff A \\iff D \\iff C$, die sind doch alle äquivalent…
 
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D =>
-"Man kann auch rückwärts umschreiben:
-`rw [←h₂]` ersetzt man im Goal `B` durch `a` (`\\l`, also ein kleines L)"
-
-HiddenHint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B =>
-"Schau mal durch die Annahmen durch."
-
-
--- These should not be necessary if they don't use `rw [] at`.
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ C) : B ↔ C =>
-"Auch eine Möglichkeit... Kannst du das Goal so umschreiben,
-dass es mit einer Annahme übereinstimmt?"
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : B ↔ D) : B ↔ C =>
-"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?"
+  **Robo**: Ja aber du musst ihm helfen umzuschreiben. Mit `rw [h₁]` kannst du `C` durch `D`
+  ersetzen."
+  rw [h₁]
+  Hint "**Du** Und wenn ich in die andere Richtung umschreiben möchte?
 
-Hint (A : Prop) (B : Prop) (h : B ↔ A) : A ↔ B =>
-"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `A ↔ A` umschreibst, kann man es mit
-`rfl` beweisen (rsp. das passiert automatisch.)"
+  **Robo**: Dann schreibst du ein `←` vor den Namen, also `rw [← hₓ]`."
+  Branch
+    rw [← h₃]
+    Hint "**Du**: Ehm, das ist verkehrt.
 
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : D ↔ A) : B ↔ C =>
-"Das ist nicht der optimale Weg..."
+    **Robo**: Andersrum wär's besser gewesen, aber wenn du jetzt einfach weitermachst bis du
+    sowas wie `A ↔ A` kriegst, kann `rfl` das beweisen.
 
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : A ↔ D) : B ↔ C =>
-"Das ist nicht der optimale Weg..."
+    **Robo: Da fällt mir ein, `rw` versucht automatisch `rfl` am Ende. Das heisst, du musst
+    das nicht einmal mehr schreiben."
+    rw [h₂]
+  rw [←h₂]
+  assumption
 
+Conclusion "Ihr geht weiter und der Operationsleiter zeigt euch die Küche."
 
 NewTactic rw assumption
+DisabledTactic tauto
+-- NewLemma Iff.symm
diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
index 0808a39..8801210 100644
--- a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
@@ -10,35 +10,35 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Nun schauen wir uns Option 1) an, die du schon von UND kennst:
+Der Koch kommt erfreut hinter einem grossen Topf hervor.
 
-1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen
-   direkt auswählen.
-
-`h.mp` und `h.mpr` (oder `h.1` und `h.2`) sind die einzelnen Implikationen, und du kannst
-mit denen ensprechend arbeiten. Insbesondere kannst du mit `apply h.mp` die Implikation
-$A \\Rightarrow B$ anwenden, wenn das Goal $B$ ist.
-
-*(PS: das `.mp` kommt von \"Modus Ponens\", ein Ausdruck as der Logik.)*
+**Koch**: Sagt mal, gestern hat mir jemand was erzählt und es will einfach nicht aus
+meinem Kopf…
 "
 
-Statement
-"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
-    (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+Statement (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+  Hint "**Du**: Naja ich kann wohl immerhin mal mit `intro` anfangen und annehmen,
+  dass `{A}` wahr sei…
+
+  **Robo**: und dann schauen wir weiter!"
   intro hA
+  Hint "**Robo**: Also eine Implikation wendet man mit apply an…
+
+  **Du**: Weiss ich ja!"
   apply g
-  apply h.mp
-  assumption
+  Hint "**Robo**: …und du kannst die Implikation `{A} → {B}` genau gleich mit
+  `apply {h}.mp` anwenden.
 
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C =>
-"Fange wie immer mit `intro` an."
+  **Du**: Aber ich könnte hier auch `rw [← h]` sagen, oder?
 
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C =>
-"Wie im Implikationen-Level kannst du nun `apply` verwenden."
+  **Robo**: Klar, aber offenbar versteht der Koch das `rw` nicht.
+  "
+  apply h.mp
+  assumption
 
-Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
-"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
+Conclusion "**Koch**: Danke vielmals! Jetzt muss ich aber schauen dass die Suppe nicht verkocht!
 
-Conclusion "Im nächsten Level findest du die zweite Option."
+Und er eilt davon."
 
 NewTactic apply assumption
+DisabledTactic tauto rw
diff --git a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
index 4ee0cb8..eb57b75 100644
--- a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
@@ -10,33 +10,30 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Und noch die letzte Option:
+Noch während der Koch wieder zu seiner Suppe geht, kommt sein erster Gehilfe hervor.
 
-2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei
-   separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)`
-
-Als letzte Option kannst du `rcases h with ⟨h₁, h₂⟩` auch auf eine Annahme `(h : A ↔ B)`
-anwenden, genau wie du dies bei einer Annahme `(h' : A ∧ B)` gemacht hast.
+**Gehilfe**: Ich hab gestern noch was anderes gehört, könnt ihr mir da auch helfen?
+Aber ich versteh nicht ganz was ihr meinem Chef erklärt habt.
 "
-Statement
-"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
-    (A B : Prop) : (A ↔ B) → (A → B) := by
-  intro h
-  rcases h
-  assumption
 
-HiddenHint (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
-"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
-
-HiddenHint (A : Prop) (B : Prop) (h : A ↔ B) : A → B =>
-"Mit `rcases h with ⟨h₁, h₂⟩` kannst du jetzt die Annahme `(h : A ↔ B)` zerlegen."
+Statement (A B : Prop) : (A ↔ B) → (A → B) := by
+  Hint "**Du**: Hmm, mindestens mit der Implikation kann ich anfangen."
+  Hint (hidden := true) "**Robo**: Genau, das war `intro`."
+  intro h
+  Hint "**Du**: Also ich kenn `rw [h]` und `apply h.mp`, aber das will er wohl nicht hören.
 
+  **Robo**: Was du machen könntest ist mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
+  Teile aufteilen."
+  rcases h with ⟨mp, mpr⟩
+  Hint (hidden := true) "**Du**: Ah und jetzt ist das Resultat in den Annahmen."
+  assumption
 
 Conclusion
 "
+**Gehilfe**: Ah danke! Und jetzt versteh ich auch die Zusammenhänge!
 "
 
-NewTactic intro apply rcases assumption
+DisabledTactic rw apply tauto
 
 -- -- TODO: The new `cases` works differntly. There is also `cases'`
 -- example (A B : Prop) : (A ↔ B) → (A → B) := by
diff --git a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
index 2926e69..baacf71 100644
--- a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
@@ -11,6 +11,12 @@ Title "Lemmas"
 
 Introduction
 "
+Ihr setzt euch hin und der Gehilfe bringt euch allen Suppe. Neben euch sitzt eine Mechanikerin
+über ihre Suppe geneigt.
+
+**Mechanikerin**: Sagt mal, ich hab unten über folgendes tiefgründiges Problem nachgedacht:
+
+
 Bewiesene Resultate möchte man in späteren Aufgaben als Sätze wieder verwenden.
 
 In Lean sind das Lemmas und Theoreme (wobei es keinen Unterschied zwischen `lemma` und `theorem`
@@ -33,23 +39,21 @@ Wenn also dein Goal `¬A ∨ B` ist, kannst du mit `apply not_or_of_imp` dieses
 Lemma anwenden. Danach musst du noch alle Annahmen zeigen.
 "
 
-Statement
-"Benutze `not_or_of_imp` um zu zeigen, dass $\\neg A \\lor A$ wahr ist."
-    (A : Prop) : ¬A ∨ A := by
+Statement (A : Prop) : ¬A ∨ A := by
+  Hint "**Du**: Das scheint ziemlich offensichtlich.
+
+  **Robo**: Ich glaube, sie will eine detailierte Antwort. Ich kenne ein Lemma
+  `not_or_of_imp`, was sagt `(A → B) → ¬ A ∨ B`. Da das Resultat des Lemmas mit
+  deinem Goal übreinstimmt, kannst du es mit `apply not_or_of_imp` anwenden."
   apply not_or_of_imp
+  Hint (hidden := true) "**Robo**: Ich würd wieder mit `intro` weitermachen."
   intro
   assumption
 
-HiddenHint (A : Prop) :  ¬A ∨ A =>
-"Das Lemma wendest du mit `apply not_or_of_imp` an."
-
-HiddenHint (A : Prop) : A → A =>
-"Wie immer, `intro` ist dein Freund."
-
 Conclusion
 "
+**Mechanikerin**: Danke vielmals, jetzt bin ich schon viel ruhiger.
 "
 
-NewTactic apply left right assumption
-
 NewLemma not_or_of_imp
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L11_ByCases.lean b/server/testgame/TestGame/Levels/Implication/L11_ByCases.lean
new file mode 100644
index 0000000..7493335
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Implication/L11_ByCases.lean
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib
+
+Game "TestGame"
+World "Implication"
+Level 11
+
+Title "by_cases"
+
+Introduction
+"
+**Du**: Sagt mal, hätte ich da nicht auch einfach zwei Fälle anschauen können:
+Wenn `A` wahr ist, beweis ich die rechte Seite, sonst die Linke.
+
+**Robo**: Tatsächlich, `by_cases h : A` würde genau das machen!
+"
+
+Statement (A : Prop) : ¬A ∨ A := by
+  Hint (hidden := true) "**Du**: Wie?
+
+  **Robo**: Also `by_cases h : A` erstellt zwei Goals. Im ersten hast Du `(h : A)` zur
+  Verfügung, im zweiten `(h : ¬ A)`."
+  by_cases h : A
+  Hint "**Du**: "
+  right
+  assumption
+  left
+  assumption
+
+Conclusion
+"
+**Du**: Das kann noch ganz nützlich sein.
+"
+
+NewTactic by_cases
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
deleted file mode 100644
index cccdd84..0000000
--- a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Cases
-import Mathlib.Logic.Basic
-
-Game "TestGame"
-World "Implication"
-Level 11
-
-Title "Lemmas"
-
-Introduction
-"
-Wenn die Aussage eines Lemmas eine Äquivalenz ist, kann man dieses auch mit `rw` brauchen,
-wie du es von Äquivalenzen kennst.
-
-Ein wichtiges Lemma ist dass $\\neg(\\neg A))$ und $A$ äquivalent sind:
-
-```
-lemma not_not (A : Prop) : ¬¬A ↔ A := by
-  ...
-```
-
-Mit `rw [not_not]` sucht Lean also im Goal ein Term `¬¬(·)` und entfernt dort das `¬¬`.
-"
-
-Statement
-"Zeige, dass $A ∨ (¬¬B) ∧ C$ und $A ∨ B ∧ C$ äquivalent sind."
-    (A B C : Prop) : A ∨ (¬¬B) ∧ C ↔ A ∨ B ∧ C := by
-  rw [not_not]
-
-Conclusion
-"
-`rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet.
-"
-
-NewTactic rw
-
-NewLemma not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L12_Rw.lean b/server/testgame/TestGame/Levels/Implication/L12_Rw.lean
new file mode 100644
index 0000000..ed9683a
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Implication/L12_Rw.lean
@@ -0,0 +1,50 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib.Logic.Basic
+
+Game "TestGame"
+World "Implication"
+Level 12
+
+Title "Lemmas"
+
+Introduction
+"
+Der Arbeitskollegin der Mechanikerin, der die ganze Zeit gespannt zugehört hat, dreht sich zu
+euch.
+
+Er ist offensichtlich interessiert and existierenden Resultaten zu sein, aber offenbar
+kann er nicht viel mit `apply` anfangen.
+
+Er hat aber folgendes Resultat bereit:
+
+```
+lemma not_not (A : Prop) : ¬¬A ↔ A
+```
+
+und stellt euch folgende Frage:
+"
+
+Statement (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
+  Hint "**Robo**: Ein Lemma, das wie `not_not` ein `↔` oder `=` im Statement hat, kann
+  auch mit `rw [not_not]` verwendet werden."
+  rw [not_not]
+  Hint "**Du**: Häh, wieso hat das jetzt 2 von 3 der `¬¬` umgeschrieben?
+
+  **Robo**: `rw` schreibt nur das erste um, das es findet, also `¬¬C`. Aber weil dieses
+  mehrmals vorkommt, werden die alle ersetzt…
+
+  **Du**: Ah, und `¬¬B` ist was anderes, also brauch ich das Lemma nochmals."
+  rw [not_not]
+
+Conclusion
+"
+**Du**: Ah und wir sind fertig…?
+
+**Robo**: Ja, `rw` versucht immer anschliessend `rfl` aufzurufen, und das hat hier
+funktioniert.
+"
+
+DisabledTactic tauto apply
+NewLemma not_not
diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
deleted file mode 100644
index ef67410..0000000
--- a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
+++ /dev/null
@@ -1,81 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Implication"
-Level 12
-
-Title "Zusammenfassung"
-
-Introduction
-"
-Damit bist du am Ende der zweiten Lektion angekommen.
-Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
-Abschlussaufgabe.
-
-## Notationen / Begriffe
-
-|               | Beschreibung                                             |
-|:--------------|:---------------------------------------------------------|
-| →             | Eine Implikation.                                        |
-| ↔             | Genau-dann-wenn / Äquivalenz.                            |
-| `lemma`       | Ein Resultat mit einem Namen.                            |
-| `theorem`     | Das gleiche wie ein Lemma.                               |
-| `example`     | Wie ein Lemma aber ohne Namen (nicht weiter verwendbar.) |
-
-## Taktiken
-
-|     | Taktik                    | Beispiel                                               |
-|:----|:--------------------------|:-------------------------------------------------------|
-| 8   | `intro`                   | Für eine Implikation im Goal.                          |
-| 9   | `revert`                  | Umkehrung von `intro`.                                 |
-| 10  | `apply`                   | Wendet eine Implikation auf das Goal an.               |
-| 10ᵇ | `apply`                   | Wendet ein Lemma an.                                   |
-| 11  | `rw`                      | Umschreiben zweier äquivalenter Aussagen.              |
-| 11ᵇ | `rw`                      | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
-
-
-Als Abschlussübung kannst du folgende Äquivalenz zeigen:
-"
-
-Statement imp_iff_not_or
-"$A \\Rightarrow B$ ist äquivalent zu $\\neg A \\lor B$."
-    (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
-  constructor
-  apply not_or_of_imp
-  intro h ha
-  rcases h with h | h
-  contradiction
-  assumption
-
-HiddenHint (A : Prop) (B: Prop) : (A → B) ↔ ¬ A ∨ B =>
-"Eine Äquivalenz im Goal geht man immer mit `constructor` an."
-
-HiddenHint (A : Prop) (B: Prop) : (A → B) → ¬ A ∨ B =>
-"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet."
-
-HiddenHint (A : Prop) (B: Prop) (h : A → B) : ¬ A ∨ B =>
-"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet."
-
-HiddenHint (A : Prop) (B: Prop) : ¬ A ∨ B → (A → B) =>
-"Eine Implikation geht man fast immer mit `intro h` an."
-
-HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) =>
-"Nochmals `intro`."
-
-HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) =>
-"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen."
-
-HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B =>
-"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen."
-
-HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B =>
-"Findest du einen Widerspruch?"
-
-NewTactic rfl assumption trivial left right constructor rcases
-
-NewLemma not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L13_Summary.lean b/server/testgame/TestGame/Levels/Implication/L13_Summary.lean
new file mode 100644
index 0000000..d090e79
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Implication/L13_Summary.lean
@@ -0,0 +1,63 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Implication"
+Level 13
+
+Title "Zusammenfassung"
+
+Introduction
+"
+**Operationsleiter**: Damit endet unsere Führung langsam. Bevor ihr weitergeht
+habe ich noch ein Problem, an dem ich mir die Zähne ausbeisse. Wir haben die
+Herleitung eines unserer Programme `imp_iff_not_or` verloren, und wissen nicht mehr
+ob es einwandfrei funktioniert.
+
+**Du**: Nah gut, al sehen. Robo, was hab ich denn alles hier gelernt?
+
+**Robo**: Hier ist die Übersicht:
+
+## Notationen / Begriffe
+
+|               | Beschreibung                                             |
+|:--------------|:---------------------------------------------------------|
+| →             | Eine Implikation.                                        |
+| ↔             | Genau-dann-wenn / Äquivalenz.                            |
+
+## Taktiken
+
+|     | Taktik                    | Beispiel                                               |
+|:----|:--------------------------|:-------------------------------------------------------|
+| 8   | `intro`                   | Für eine Implikation im Goal.                          |
+| 9   | `revert`                  | Umkehrung von `intro`.                                 |
+| 10  | `apply`                   | Wendet eine Implikation auf das Goal an.               |
+| 10ᵇ | `apply`                   | Wendet ein Lemma an.                                   |
+| 11  | `by_cases`                | Fallunterscheidung `P` und `¬P`                        |
+| 12  | `rw`                      | Umschreiben zweier äquivalenter Aussagen.              |
+| 12ᵇ | `rw`                      | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
+"
+
+Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
+  constructor
+  Hint "**Du**: Das sieht kompliziert aus…
+
+  **Robo** *(flüsternd)*: Ja, aber die Richtung kennst du ja schon also Lemma,
+  wend doch einfach das an."
+  apply not_or_of_imp
+  Hint "**Du**: Gibt es für die Gegenrichtung auch ein Lemma?
+
+  **Robo**: Leider nicht. Da musst du manuell ran."
+  Hint (hidden := true) "**Robo**: Na Implikationen fangst du immer mit `intro` an."
+  intro h
+  intro ha
+  Hint (hidden := true) "**Robo**: Ich wür mal die Annahme `h` mit `rcases` aufteilen."
+  rcases h with h | h
+  contradiction
+  assumption
+
+DisabledTactic tauto