diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index 7330183..d79cdf3 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -8,6 +8,7 @@ import TestGame.Levels.Prime
 import TestGame.Levels.Induction
 
 import TestGame.Levels.Numbers
+import TestGame.Levels.Inequality
 
 import TestGame.Levels.LeanStuff
 import TestGame.Levels.SetTheory
@@ -43,9 +44,10 @@ Conclusion
 
 Path Proposition → Implication → Predicate → Prime
 Path Predicate → Contradiction → LeanStuff → SetTheory → SetTheory2 → SetFunction
-Path Predicate → Induction → LeanStuff → Function → SetFunction
 Path SetTheory2 → Numbers
 
 Path Module → Basis → Module2
 
+Path Contradiction → Inequality → Induction → LeanStuff → Function → SetFunction
+
 MakeGame
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index 14622ce..fbbafdb 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -37,6 +37,15 @@ LemmaDoc imp_iff_not_or as imp_iff_not_or in "Logic"
 `(A B : Prop)`
 "
 
+
+LemmaDoc Nat.succ_pos as Nat.succ_pos in "Nat"
+"
+"
+
+LemmaDoc zero_lt_iff as zero_lt_iff in "Nat"
+"
+"
+
 LemmaDoc zero_add as zero_add in "Addition"
 "This lemma says `∀ a : ℕ, 0 + a = a`."
 
diff --git a/server/testgame/TestGame/Levels/Function/L03_Composition.lean b/server/testgame/TestGame/Levels/Function/L03_Composition.lean
index 2f64c34..ba637b3 100644
--- a/server/testgame/TestGame/Levels/Function/L03_Composition.lean
+++ b/server/testgame/TestGame/Levels/Function/L03_Composition.lean
@@ -17,4 +17,4 @@ TODO
 Statement
 "TODO: Find an exercise."
     (U S T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x)  := by
-  trivial
+  simp only [Function.comp_apply]
diff --git a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
index f1fd429..7426901 100644
--- a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
+++ b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
@@ -32,8 +32,6 @@ Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
 lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
   sorry
 ```
-
-Mit `simp?` anstatt `simp` kannst du zudem schauen, welche Lemmas von `simp` benutzt wurde.
 "
 
 open BigOperators
diff --git a/server/testgame/TestGame/Levels/Prime.lean b/server/testgame/TestGame/Levels/Prime.lean
index f2de7ce..c9fb5f6 100644
--- a/server/testgame/TestGame/Levels/Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime.lean
@@ -1,10 +1,8 @@
-import TestGame.Levels.Prime.L01_Linarith
-import TestGame.Levels.Prime.L02_Linarith
-import TestGame.Levels.Prime.L03_Dvd
+import TestGame.Levels.Prime.L01_Dvd
 import TestGame.Levels.Prime.L04_Prime
 import TestGame.Levels.Prime.L05_Prime
 import TestGame.Levels.Prime.L06_ExistsUnique
 
 Game "TestGame"
 World "Prime"
-Title "mehr Nat"
+Title "Teilbarkeit"
diff --git a/server/testgame/TestGame/Levels/Prime/L01_Linarith.lean b/server/testgame/TestGame/Levels/Prime/L01_Linarith.lean
deleted file mode 100644
index 3bf672a..0000000
--- a/server/testgame/TestGame/Levels/Prime/L01_Linarith.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Linarith
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Prime"
-Level 1
-
-Title "Kleinergleich"
-
-Introduction
-"
-Ungleichheiten werden in Lean generell immer als Kleinergleich `≤` (`\\le`) oder `<`
-geschrieben.
-
-Die Symbole `≥` und `>` gibt es zwar auch, sind aber nur Notation für die gleiche
-Aussage mit `≤` und `<`.
-
-Die Taktik `linarith` kann alle Systeme von linearen (Un-)gleichungen über `ℤ`, `ℚ`, etc. lösen.
-Über `ℕ` ist sie etwas schwächer, aber einfache Aussagen kann sie trotzdem beweisen.
-"
-
-Statement
-"Wenn $n \\ge 2$, zeige, dass $n$ nich Null sein kann."
-    (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
-  linarith
-
-NewTactics linarith
diff --git a/server/testgame/TestGame/Levels/Prime/L02_Linarith.lean b/server/testgame/TestGame/Levels/Prime/L02_Linarith.lean
deleted file mode 100644
index 44c4af5..0000000
--- a/server/testgame/TestGame/Levels/Prime/L02_Linarith.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Linarith
-
-Game "TestGame"
-World "Prime"
-Level 2
-
-Title "Linarith"
-
-Introduction
-"
-Sobald man mit einem Ring arbeitet, der eine lineare Order hat (also z.B. `ℤ` oder `ℚ`),
-ist `linarith` stärker und kann Systeme von Gleichungen und Ungleichungen angehen.
-
-`linarith` kann aber nur mit linearen Ungleichungen umgehen, mit Termen der Form `x ^ 2`
-kann es nicht umgehen.
-"
-
-Statement
-"Angenommen man hat für zwei Ganzzahlen $x, y$ folgende Ungleichungen.
-$$
-\\begin{aligned} 5 * y &\\le 35 - 2 * x \\\\ 2 * y &\\le x + 3 \\end{aligned}
-$$
-Zeige, dass $y \\le 5$.
-
-"
-    (x y : ℤ)
-    (h₂ : 5 * y ≤ 35 - 2 * x)
-    (h₃ : 2 * y ≤ x + 3)
-    : y ≤ 5 := by
-  linarith
diff --git a/server/testgame/TestGame/Levels/Prime/L03_Dvd.lean b/server/testgame/TestGame/Levels/Prime/L03_Dvd.lean
deleted file mode 100644
index 47d2f76..0000000
--- a/server/testgame/TestGame/Levels/Prime/L03_Dvd.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib.Tactic.Ring
-
-Game "TestGame"
-World "Prime"
-Level 3
-
-Title "Teilbarkeit"
-
-Introduction
-"
-Die Aussage \"$m$ teilt $n$.\" wird in Lean als `m | n` (`\\|`) geschrieben.
-
-**Wichtig:** `∣` (Teilbarkeit) ist ein spezielles Unicode Symbol, das nicht dem
-senkrechten Strich auf der Tastatur (`|`) entspricht. Man erhält es mit `\\|`.
-
-`m ∣ n` bedeutet `∃ c, n = m * c`, das heisst, man kann damit genau gleich umgehen
-wie mit einem `∃`-Quantifier.
-"
-
-Statement dvd_add
-  "Wenn $m$ ein Teiler von $n$ und $k$ ist, dann teilt es die Summe."
-  (n m k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k := by
-  rcases h with ⟨x, h⟩
-  rcases g with ⟨y, g⟩
-  use x + y
-  rw [h, g]
-  ring
diff --git a/server/testgame/TestGame/Levels/Prime/L04_Prime.lean b/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
index 56a9937..54a0f3f 100644
--- a/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
@@ -11,20 +11,21 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Prime"
-Level 4
+Level 2
 
 Title "Primzahlen"
 
 Introduction
 "
-Um zu sagen, dass eine natürliche Zahl $n$ eine Primzahl ist, braucht man
-eine Aussage `Nat.Prime n`, ähnlich wie `Even n`.
+Eine Primzahl wird mit `(n : ℕ) (h : Nat.Prime n)` dargestellt.
 
-Primzahlen sind ein Objekt in Lean, das genug abstrakt definiert ist, dass es sich
-aus mathematischer Sicht nicht lohnt mit der Definition zu arbeiten.
+Wichtige Lemmas über Primzhalen werden mit
 
-Alle wichtigen Lemmas um mit Primzahlen zu arbeiten sind in
-[`import Data.Nat.Prime`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html)
+```
+import Data.Nat.Prime
+```
+importiert (siehe
+[Docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html))
 
 Insbesondere `Nat.prime_def_lt''` welches die aus der Schule bekannte Definition einer
 Primzahl `Prime p ↔ 2 ≤ p ∧ (∀ m, m ∣ p → m = 1 ∨ m = p)` gibt.
diff --git a/server/testgame/TestGame/Levels/Prime/L05_Prime.lean b/server/testgame/TestGame/Levels/Prime/L05_Prime.lean
index 09d5ac6..61497bd 100644
--- a/server/testgame/TestGame/Levels/Prime/L05_Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime/L05_Prime.lean
@@ -11,7 +11,7 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Prime"
-Level 5
+Level 3
 
 Title "Primzahlen"
 
diff --git a/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean b/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean
index b5b15e2..bd8a3dc 100644
--- a/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean
+++ b/server/testgame/TestGame/Levels/Prime/L06_ExistsUnique.lean
@@ -11,7 +11,7 @@ import TestGame.ToBePorted
 
 Game "TestGame"
 World "Prime"
-Level 6
+Level 4
 
 Title "Existiert eindeutig"
 
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index b1adad1..0e84224 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -61,12 +61,33 @@ TacticDoc rewrite
 Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
 "
 
+TacticDoc induction
+"
+## Beschreibung
+
+Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
+"
+
+
 TacticDoc linarith
 "
 ## Beschreibung
 
 "
 
+TacticDoc fin_cases
+"
+## Beschreibung
+
+"
+
+TacticDoc funext
+"
+## Beschreibung
+
+"
+
+
 TacticDoc rw
 "
 ## Beschreibung