diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
index a46e273..3c1fe38 100644
--- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
@@ -12,18 +12,17 @@ Introduction
 Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
 unterstützt und verifiziert schreiben kann.
 
-*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am beweisen
-bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals**
+In der *mittleren Spalte* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment
+beweisen musst. Falls es mehrere Dinge zu beweisen gibt, werden alle weiteren darunter unter **Further Goals**
 aufgelistet, diese musst du dann später auch noch zeigen.
 
 Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie
 man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen,
-andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der
-Seite.
+andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken in der *rechten Spalte*.
 
 Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\".
 
-Als erstes ein kleiner Preview, dass Lean auch vieles automatisch kann. So gibt es eine
+Als erste kleine Vorschau, dass Lean auch vieles automatisch kann, gibt es eine
 Taktik `tauto`, die alle wahren Aussagen der Prädikaten-Logik beweisen kann.
 
 Dieses Beispiel würde von Hand etwas Zeit in Anspruch nehmen. Lean ist da viel schneller.
@@ -44,7 +43,7 @@ $$
   tauto
 
 Hint (A B C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
-"Man schreibt eine Taktik pro Zeile, also gib `tauto` ein und geh mit Enter ⏎ auf eine neue Zeile."
+"Gib `tauto` ein und drücke Enter ⏎."
 
 Conclusion ""
 
diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
index 614490b..34d8ce0 100644
--- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
@@ -11,7 +11,7 @@ Introduction
 Jetzt gehen wir aber einen Schritt zurück und lernen, wie man konkret mit Lean arbeitet,
 damit du verstehst, was `tauto` hinter der Kulisse macht.
 
-Deine erste Taktik ist `rfl` (für \"reflexivity\"), welche dazu da ist,
+Eine der grundlegendsten Taktiken ist `rfl` (für \"reflexivity\"), welche dazu da ist,
 ein Goal der Form $X = X$ zu schließen.
 "
 
@@ -23,7 +23,7 @@ Statement
 -- "Die Taktik `rfl` beweist ein Goal der Form `X = X`."
 
 HiddenHint : 42 = 42 =>
-"Man schreibt eine Taktik pro Zeile, also gib `rfl` ein und geh mit Enter ⏎ auf eine neue Zeile."
+"Die beiden Seiten dieser Gleichung sind identisch, also gib `rfl` ein und drücke Enter ⏎"
 
 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
 
diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
index 754aae9..22b61f4 100644
--- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
@@ -22,7 +22,7 @@ Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` be
 "
 
 Statement
-"Angenommen $1 < n$. dann ist $1 < n$."
+"Angenommen $1 < n$. Dann ist $1 < n$."
     (n : ℕ) (h : 1 < n) : 1 < n := by
   assumption