diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 6393c0c..e8ec637 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -136,7 +136,7 @@ export const Goal = React.memo((props: GoalProps) => {
             undefined,
         [locs, goal.mvarId])
     const goalLi = <div key={'goal'}>
-        <div className="goal-title">Target: </div>
+        <div className="goal-title">Goal: </div>
         <LocationsContext.Provider value={goalLocs}>
             <InteractiveCode fmt={goal.type} />
         </LocationsContext.Provider>
@@ -155,10 +155,10 @@ export const Goal = React.memo((props: GoalProps) => {
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
         { objectHyps.length > 0 &&
-            <div className="hyp-group"><div className="hyp-group-title">Objects:</div>
+            <div className="hyp-group"><div className="hyp-group-title">Objekte:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
         { assumptionHyps.length > 0 &&
-            <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
+            <div className="hyp-group"><div className="hyp-group-title">Annahmen:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
         {commandLine && commandLineMode && <CommandLine />}
         {!filter.reverse && goalLi}
diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
index 646374d..97de4d3 100644
--- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
@@ -16,7 +16,8 @@ True := by
   trivial
 
 Hint : True => "
-**Robo**  Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist.
+**Robo**  Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und
+bedingungslos wahr ist.
 
 **Du** Und was genau ist dann zu beweisen?
 
@@ -27,9 +28,11 @@ Conclusion
 "
 **Schelm**  Wollte nur mal sehen, dass Ihr nicht auf den Kopf gefallen seid …
 
-**Du** *(zu Robo)*  Können wir nicht einfach immer dieses `trivial` verwenden?  Wie in einer Mathe-Vorlesung?
+**Du** *(zu Robo)*  Können wir nicht einfach immer dieses `trivial` verwenden?
+Wie in einer Mathe-Vorlesung?
 
-**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung.  Das funktioniert nur in einer Handvoll Situationen.
+**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung.
+Das funktioniert nur in einer Handvoll Situationen.
 "
 
 NewTactics trivial
diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
index 3c5c77f..3800549 100644
--- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
@@ -16,7 +16,8 @@ Statement "" :
   trivial
 
 Hint : ¬False => "
-  **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)` wahr ist, dann ist  `¬A` falsch, und umgekehrt.
+  **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
+  wahr ist, dann ist  `¬A` falsch, und umgekehrt.
 
   **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
 
diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index 9d60083..eb689d2 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -41,7 +41,7 @@ Statement ""
   assumption
 
 HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
+"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
 
 HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
 "**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
@@ -60,7 +60,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
 "**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
 
 HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
+"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
 
 -- TODO: Hint nur Anhand der Annahmen?