diff --git a/client/src/App.tsx b/client/src/App.tsx
index db553a2..7be4e5b 100644
--- a/client/src/App.tsx
+++ b/client/src/App.tsx
@@ -44,7 +44,7 @@ function App() {
   if (finished) {
     mainComponent = <GoodBye message={conclusion} />
   } else if (curLevel > 0) {
-    mainComponent = <Level nbLevels={5} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
+    mainComponent = <Level nbLevels={99} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
   } else {
     mainComponent = <Welcome setNbLevels={setNbLevels} startGame={startGame} setConclusion={setConclusion}/>
   }
diff --git a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
index 6b1329f..765544e 100644
--- a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
@@ -1,4 +1,5 @@
 import TestGame.Metadata
+import Mathlib
 
 Game "TestGame"
 World "TestWorld"
@@ -16,38 +17,40 @@ kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal
 das eine durch das andere zu ersetzen.
 "
 
-Statement umschreiben
-    "
-    Angenommen man hat die Gleichheiten
-    `a = b`, `a = d`, `c = d`.
-    Zeige dass `b = c`.
-    "
-    (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
-  rw [h₁]
-  rw [←h₂]
+Statement (A : Prop) (hA : A) : A := by
   assumption
 
--- Gleich am Anfang anzeigen.
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste
-`c` im Goal mit `d` ersetzen."
-
-Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man schreibt diese mit
-`\\1`, `\\2`, `\\3`, …"
-
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
-"Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses
-`(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."
-
--- TODO: Muss ich das wirklich mehrmals auflisten?
-Message (x : ℕ) : x = x =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
+-- Statement umschreiben
+--     "
+--     Angenommen man hat die Gleichheiten
+--     `a = b`, `a = d`, `c = d`.
+--     Zeige dass `b = c`.
+--     "
+--     (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+--   rw [h₁]
+--   rw [←h₂]
+--   assumption
+
+-- -- Gleich am Anfang anzeigen.
+-- Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
+-- "Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste
+-- `c` im Goal mit `d` ersetzen."
+
+-- Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
+-- "Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man schreibt diese mit
+-- `\\1`, `\\2`, `\\3`, …"
+
+-- Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
+-- "Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses
+-- `(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."
+
+-- -- TODO: Muss ich das wirklich mehrmals auflisten?
+-- Message (x : ℕ) : x = x =>
+-- "Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
+-- anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
 
 Conclusion "Übrigens, mit `rw [h₁] at h₂` kann man auch eine andere Annahme umschreiben
 anstatt dem Goal."
 -- TODO: Das macht es doch unmöglich mit den Messages...
 
-Tactics assumption
-Tactics rw
+Tactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
index f10e1c7..bbc1e80 100644
--- a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
+++ b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean
@@ -1,5 +1,7 @@
 import TestGame.Metadata
 
+set_option tactic.hygienic false
+
 Game "TestGame"
 World "TestWorld"
 Level 8
@@ -8,7 +10,8 @@ Title "Implikation"
 
 Introduction
 "
-Wenn das Goal von der Form `A → B` ist, kann man mit `intro` annehmen, dass `A` wahr ist
+Wenn das Goal von der Form `A → B` ist, kann man mit `intro hA` annehmen, dass `A` wahr ist
+(i.e. erstellt eine Annahme `(hA : A)`)
 und das Goal wird zu `B`.
 "
 
diff --git a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
index 506d103..9d2f9d6 100644
--- a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean
@@ -26,5 +26,4 @@ Statement
   rw [←h₂]
   assumption
 
-Tactics rw
-Tactics assumption
+Tactics rw assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
index 1940f8e..d5b35cd 100644
--- a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
+++ b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean
@@ -33,7 +33,6 @@ aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean,
 ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
 "
 
-Tactics constructor
-Tactics assumption
+Tactics constructor assumption
 
 -- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
diff --git a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
index 7de302e..c2ec0a2 100644
--- a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
+++ b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean
@@ -55,4 +55,4 @@ Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
 Message (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
 "Ein UND im Goal kann mit `constructor` aufgeteilt werden."
 
-Tactics left right assumption constructor rcases
+Tactics left right assumption constructor rcases apply