From 23abcaf48838d1525d724be88d3eb902262d8ffb Mon Sep 17 00:00:00 2001
From: Marcus Zibrowius <marcus.zibrowius@cantab.net>
Date: Fri, 31 Mar 2023 10:25:07 +0200
Subject: [PATCH 1/3] =?UTF-8?q?Titelseite=20=C3=BCberarbeiten?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 server/adam/Adam.lean | 35 +++++++++++++++++------------------
 1 file changed, 17 insertions(+), 18 deletions(-)

diff --git a/server/adam/Adam.lean b/server/adam/Adam.lean
index ff52b0b..546d678 100644
--- a/server/adam/Adam.lean
+++ b/server/adam/Adam.lean
@@ -25,37 +25,36 @@ Introduction
 "
 # Game Over oder QED?
 
-Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du Computer-gestütztes
-Beweisen. Das Interface ist anfangs etwas vereinfacht, der \"Editor Mode\" funktioniert aber
-ziemlich gleich wie wenn du später Lean im VSCode benützt.
+Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du computer-gestützte
+Beweisführung. Das Interface ist etwas vereinfacht, aber wenn Du den *Editor Mode* aktivierst, fühlt es sich 
+fast genauso an wie eine professionalle IDE, etwa VSCode.
 
-Rechts siehst du eine Übersicht der Welt dieses Spiels. Jeder Planet hat mehrere Levels,
-die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden dann grün.
+Rechts siehst du eine Übersicht. Das Spiel besteht aus mehreren Planeten, und jeder Planet hat mehrere Levels,
+die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden grün.
 
-Klicke auf die erste Welt \"Aussagenlogik 1\" um deine Reise zu starten.
+Klicke auf den ersten Planeten \"Logo\", um deine Reise zu starten.
 
 ### Spielstand
 
-Dein Spielstand wird lokal in deinem Browser als \"site data\" gespeichert.
-Solltest du diese löschen, verlierst du deinen Spielstand! Du kannst aber jederzeit jeden
-Level spielen, auch wenn frühere Levels nicht grün sind.
-
-(oft werden *Site data & Cookies* zusammen gelöscht).
+Dein Spielstand wird lokal in deinem Browser als *site data* gespeichert.
+Solltest du diese löschen, verlierst du deinen Spielstand!  
+Viele Browser löschen *site data* und *cookies* zusammen.
+Du kannst aber jederzeit jedes Level spielen, auch wenn Du vorhergende Levels noch nicht gelöst hast.  
 
 ### Funding
 
-This game has been developed within the project
-[ADAM: Anticipating the Digital Age of Mathematics](https://hhu-adam.github.io/).
-The project is based at Heinrich Heine University Düsseldorf and funded by Stiftung
-Innovation in der Hochschullehre.
+Dieses Lernspiel wurde und wird im Rahmen des Projekts 
+[ADAM: Anticipating the Digital Age of Mathematics](https://hhu-adam.github.io/)
+an der Heinrich-Heine-Universität Düsseldorf entwickelt.
+Es wird finanziert durch das Programm *Freiraum 2022* der *Stiftung Innovation in der Hochschullehre*.
 
 ### Kontakt
 
-Wenn du Bugs findest, schreib doch ein Email oder erstelle einen
+Das Spiel befindet sich noch in der Entwicklung.  
+Wenn du Anregungen hast oder Bugs findest, schreib doch ein Email oder erstelle einen
 [Issue auf Github](https://github.com/leanprover-community/lean4game/issues).
 
-Jon Eugster, jon.eugster@hhu.de
-
+[Jon Eugster](https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster)
 "
 
 Conclusion

From e947c434a82ce483392bc6f57e8596d61b5d90f1 Mon Sep 17 00:00:00 2001
From: Marcus Zibrowius <marcus.zibrowius@cantab.net>
Date: Fri, 31 Mar 2023 10:44:50 +0200
Subject: [PATCH 2/3] konsequente Kleinschreibung von du, dein, dir

---
 server/adam/Adam.lean                         |  6 +++---
 server/adam/Adam/Levels/Contradiction.lean    |  2 +-
 .../Adam/Levels/Contradiction/L01_Have.lean   |  4 ++--
 .../Levels/Contradiction/L02_Suffices.lean    |  6 +++---
 .../Levels/Contradiction/L03_ByContra.lean    | 10 +++++-----
 .../Levels/Contradiction/L04_ByContra.lean    |  2 +-
 .../Levels/Contradiction/L05_Contrapose.lean  |  2 +-
 .../Adam/Levels/Function/L03_Piecewise.lean   |  2 +-
 .../Adam/Levels/Function/L09_Inverse.lean     |  2 +-
 .../Adam/Levels/Function/L11_Inverse.lean     |  2 +-
 .../Adam/Levels/Implication/L01_Intro.lean    |  6 +++---
 .../adam/Adam/Levels/Implication/L06_Iff.lean |  4 ++--
 .../adam/Adam/Levels/Implication/L07_Rw.lean  |  2 +-
 .../adam/Adam/Levels/Implication/L08_Iff.lean |  2 +-
 .../adam/Adam/Levels/Implication/L09_Iff.lean |  4 ++--
 .../Adam/Levels/Implication/L10_Apply.lean    |  8 ++++----
 .../Adam/Levels/Implication/L11_ByCases.lean  |  2 +-
 .../Adam/Levels/Implication/L13_Summary.lean  |  6 +++---
 .../adam/Adam/Levels/Inequality/L02_Pos.lean  |  2 +-
 .../Adam/Levels/Inequality/L04_Linarith.lean  |  2 +-
 server/adam/Adam/Levels/Lean.lean             |  2 +-
 server/adam/Adam/Levels/Predicate.lean        |  4 ++--
 .../adam/Adam/Levels/Predicate/L01_Ring.lean  |  2 +-
 .../Adam/Levels/Predicate/L03_Rewrite.lean    |  2 +-
 .../Adam/Levels/Predicate/L06_Exists.lean     | 16 +++++++--------
 .../Adam/Levels/Predicate/L07_Exists.lean     |  4 ++--
 .../Adam/Levels/Predicate/L08_Forall.lean     |  2 +-
 .../Adam/Levels/Predicate/L09_PushNeg.lean    | 18 ++++++++---------
 server/adam/Adam/Levels/Proposition.lean      | 14 ++++++-------
 .../Adam/Levels/Proposition/L00_Tauto.lean    |  4 ++--
 .../adam/Adam/Levels/Proposition/L01_Rfl.lean |  2 +-
 .../Levels/Proposition/L02_Assumption.lean    |  2 +-
 .../Levels/Proposition/L03_Assumption.lean    |  2 +-
 .../Adam/Levels/Proposition/L04_True.lean     |  2 +-
 .../Adam/Levels/Proposition/L06_False.lean    |  2 +-
 .../adam/Adam/Levels/Proposition/L09_And.lean |  6 +++---
 .../adam/Adam/Levels/Proposition/L10_And.lean |  4 ++--
 .../adam/Adam/Levels/Proposition/L11_Or.lean  |  6 +++---
 .../adam/Adam/Levels/Proposition/L12_Or.lean  | 18 ++++++++---------
 .../Adam/Levels/Proposition/L13_Summary.lean  | 20 +++++++++----------
 40 files changed, 104 insertions(+), 104 deletions(-)

diff --git a/server/adam/Adam.lean b/server/adam/Adam.lean
index 546d678..884e426 100644
--- a/server/adam/Adam.lean
+++ b/server/adam/Adam.lean
@@ -26,20 +26,20 @@ Introduction
 # Game Over oder QED?
 
 Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du computer-gestützte
-Beweisführung. Das Interface ist etwas vereinfacht, aber wenn Du den *Editor Mode* aktivierst, fühlt es sich 
+Beweisführung. Das Interface ist etwas vereinfacht, aber wenn du den *Editor Mode* aktivierst, fühlt es sich 
 fast genauso an wie eine professionalle IDE, etwa VSCode.
 
 Rechts siehst du eine Übersicht. Das Spiel besteht aus mehreren Planeten, und jeder Planet hat mehrere Levels,
 die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden grün.
 
-Klicke auf den ersten Planeten \"Logo\", um deine Reise zu starten.
+Klicke auf den ersten Planeten *Logo*, um deine Reise zu starten.
 
 ### Spielstand
 
 Dein Spielstand wird lokal in deinem Browser als *site data* gespeichert.
 Solltest du diese löschen, verlierst du deinen Spielstand!  
 Viele Browser löschen *site data* und *cookies* zusammen.
-Du kannst aber jederzeit jedes Level spielen, auch wenn Du vorhergende Levels noch nicht gelöst hast.  
+Du kannst aber jederzeit jedes Level spielen, auch wenn du vorhergende Levels noch nicht gelöst hast.  
 
 ### Funding
 
diff --git a/server/adam/Adam/Levels/Contradiction.lean b/server/adam/Adam/Levels/Contradiction.lean
index af58f48..127262c 100644
--- a/server/adam/Adam/Levels/Contradiction.lean
+++ b/server/adam/Adam/Levels/Contradiction.lean
@@ -17,7 +17,7 @@ Ein einziger, einsamer Formalosoph, der sich als Benedictus vorstellt, erwartet
 
 **Benedictus**: Schön, dass Ihr gekommen seid!  Ich habe schon auf Euch gewartet!  
 
-**Du**: Hast Du auch ein paar dringende Fragen … ? 
+**Du**: Hast du auch ein paar dringende Fragen … ? 
 
 **Benedictus**:  Ach nein, aus dem Alter bin ich heraus.  Aber ich kann mir denken, wie es Euch auf Implis und Quantus ergangen ist.  Und glaubt, mir auf den anderen Planeten wird es nicht viel besser.  Aber ich kann Euch vielleicht ein bisschen vorbereiten.  
 
diff --git a/server/adam/Adam/Levels/Contradiction/L01_Have.lean b/server/adam/Adam/Levels/Contradiction/L01_Have.lean
index ced66a2..89e9d7c 100644
--- a/server/adam/Adam/Levels/Contradiction/L01_Have.lean
+++ b/server/adam/Adam/Levels/Contradiction/L01_Have.lean
@@ -39,13 +39,13 @@ Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
   rcases k with ⟨h₁, h₂⟩
   Hint "**Du**: Und jetzt …
 
-  **Benedictus**: … solltest Du Dir ein passendes Zwischenresultat zurechtlegen.
+  **Benedictus**: … solltest du dir ein passendes Zwischenresultat zurechtlegen.
 
   **Robo**:  Ja!  Probier mal `have g : ¬ B`!"
   have g : ¬ B
   · Hint "**Du**: Was?  Jetzt hab ich einfach angenommen, dass sei richtig?
 
-    **Robo**: Nee, jetzt musst Du das erst noch beweisen, bevor Du es dann benutzen kannst."
+    **Robo**: Nee, jetzt musst du das erst noch beweisen, bevor du es dann benutzen kannst."
     Hint (hidden := true) "**Robo**: `apply` sollte helfen"
     apply h
     assumption
diff --git a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean
index 270402c..8b33da1 100644
--- a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean
+++ b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean
@@ -38,7 +38,7 @@ Introduction
 
 Statement
     (A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
-  Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst Du auch `suffices`
+  Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
   verwenden. Das funktioniert genau gleich, außer, dass dann die beiden Beweisziele vertauscht sind.
 
   **Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
@@ -46,9 +46,9 @@ Statement
 
   **Robo**: Genau!"
   suffices g : ¬ B
-  Hint "**Robo**: Also hier beendest Du den Beweis unter der Annahme `{g}` sei wahr."
+  Hint "**Robo**: Also hier beendest du den Beweis unter der Annahme `{g}` sei wahr."
   contradiction
-  Hint "**Robo**: Und hier beweist Du das Zwischenresultat."
+  Hint "**Robo**: Und hier beweist du das Zwischenresultat."
   apply h
   assumption
 
diff --git a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean
index db3ccb9..6d3e7cb 100644
--- a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean
+++ b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean
@@ -30,21 +30,21 @@ Introduction
 -- steht:
 
 Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
-  Hint "**Robo**: Ein `¬` im Goal heißt häufig, dass Du einen Widerspruchsbeweis führen
+  Hint "**Robo**: Ein `¬` im Goal heißt häufig, dass du einen Widerspruchsbeweis führen
   möchtest.
 
   **Du**: Und wie mache ich das? Mit `contradiction`?
 
-  **Robo**: Mit `by_contra h` fängst Du einen Widerspruchsbeweis an. Und mit `contradiction` schließt Du ihn ab."
+  **Robo**: Mit `by_contra h` fängst du einen Widerspruchsbeweis an. Und mit `contradiction` schließt du ihn ab."
   by_contra h
-  Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : {A}`, und damit musst Du einen Widerspruch herleiten.
+  Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : {A}`, und damit musst du einen Widerspruch herleiten.
 
-  Du könntest zum Beispiel jetzt mit `suffices` sagten, welchen Widerspruch Du gern herleiten möchtest, etwa `suffices k : B`
+  Du könntest zum Beispiel jetzt mit `suffices` sagten, welchen Widerspruch du gern herleiten möchtest, etwa `suffices k : B`
   "
   suffices k : B
   Hint "**Du**: Ah, und jetzt kann ich einfach sagen dass sich die Annahmen `{B}` und `¬{B}` sich widersprechen."
   contradiction
-  Hint "**Robo**: Und jetzt musst Du nur noch das Zwischenresultat herleiten, dass zu diesem Widerspruch geführt hat."
+  Hint "**Robo**: Und jetzt musst du nur noch das Zwischenresultat herleiten, dass zu diesem Widerspruch geführt hat."
   apply g
   assumption
 
diff --git a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean
index a285afc..0c75735 100644
--- a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean
+++ b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean
@@ -22,7 +22,7 @@ Introduction
 Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
   Hint "**Du**: Ja, das habe ich tatsächlich schon einmal gesehen.
 
-  **Robo**:  Ja, klar hast Du das schon einmal gesehen.  Das benutzen Mathematiker doch ständig.  Wenn ihnen zu $A ⇒ B$ nichts einfällt, zeigen sie stattdessen $¬B ⇒ ¬A$.  Ich würde das ja statt *Kontraposition* oder `not_imp_not` eher *von_hinten_durch_die_Brust_ins_Auge* nennen.  Aber gut, ich will mich nicht einmisschen.
+  **Robo**:  Ja, klar hast du das schon einmal gesehen.  Das benutzen Mathematiker doch ständig.  Wenn ihnen zu $A ⇒ B$ nichts einfällt, zeigen sie stattdessen $¬B ⇒ ¬A$.  Ich würde das ja statt *Kontraposition* oder `not_imp_not` eher *von_hinten_durch_die_Brust_ins_Auge* nennen.  Aber gut, ich will mich nicht einmisschen.
   " 
   Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
   constructor
diff --git a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean
index 396c31c..638f18e 100644
--- a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean
+++ b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean
@@ -42,7 +42,7 @@ Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
 
   **Du**:  Richtig. Von hinten durch die Brust … Aber warte, im Moment steht da doch gar kein `→`.
 
-  **Robo**:  Erinner Dich an `revert`.  Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Beweissziel schieben."
+  **Robo**:  Erinner dich an `revert`.  Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Beweissziel schieben."
   revert h
   Hint "**Du**: Und jetzt kann ich dieses Kontrapositionslemma anwenden?  Wie hieß das noch einmal?  
 
diff --git a/server/adam/Adam/Levels/Function/L03_Piecewise.lean b/server/adam/Adam/Levels/Function/L03_Piecewise.lean
index 87233b7..095b410 100644
--- a/server/adam/Adam/Levels/Function/L03_Piecewise.lean
+++ b/server/adam/Adam/Levels/Function/L03_Piecewise.lean
@@ -22,7 +22,7 @@ der andere eines mit
 def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
 ```
 
-und gibt Dir ein Blatt mit einer einzelnen Zeile am oberen Ende.
+und gibt dir ein Blatt mit einer einzelnen Zeile am oberen Ende.
 "
 
 open Set
diff --git a/server/adam/Adam/Levels/Function/L09_Inverse.lean b/server/adam/Adam/Levels/Function/L09_Inverse.lean
index 120ccbd..382f932 100644
--- a/server/adam/Adam/Levels/Function/L09_Inverse.lean
+++ b/server/adam/Adam/Levels/Function/L09_Inverse.lean
@@ -14,7 +14,7 @@ eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stun
 und der Gelehrte möchte wissen, wie das den genau ginge.
 
 Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
-aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
+aber er möchte, dass du ihm das hier und jetzt nochmals von Grund auf zeigst.
 "
 
 open Function
diff --git a/server/adam/Adam/Levels/Function/L11_Inverse.lean b/server/adam/Adam/Levels/Function/L11_Inverse.lean
index f6b0c68..be12aaa 100644
--- a/server/adam/Adam/Levels/Function/L11_Inverse.lean
+++ b/server/adam/Adam/Levels/Function/L11_Inverse.lean
@@ -14,7 +14,7 @@ eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stun
 und der Gelehrte möchte wissen, wie das den genau ginge.
 
 Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
-aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
+aber er möchte, dass du ihm das hier und jetzt nochmals von Grund auf zeigst.
 "
 
 open Function
diff --git a/server/adam/Adam/Levels/Implication/L01_Intro.lean b/server/adam/Adam/Levels/Implication/L01_Intro.lean
index b215b37..51a674f 100644
--- a/server/adam/Adam/Levels/Implication/L01_Intro.lean
+++ b/server/adam/Adam/Levels/Implication/L01_Intro.lean
@@ -20,7 +20,7 @@ Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
 
   **Du**: Einen Moment.  Das ist ja gerade so eine Implikation (`\\to`).  Wir nehmen an, dass `{B}` gilt, und wollen zeigen, dass dann gilt `{A}` impliziert `{A} und {B}`. Ja, klar! Natürlich stimmt das.
 
-  Der Operationsleiter sieht Dich erwartungsvoll an.
+  Der Operationsleiter sieht dich erwartungsvoll an.
 
   **Du** *(leise zu Robo)*:  Soll ich ihm `tauto` aufschreiben?
 
@@ -29,11 +29,11 @@ Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
 
   *Du**: Aber wie denn?  Ich glaube, ich würde als erstes gern so etwas sagen wie 'Nehmen wir also an, `{A}` gilt …'
 
-  **Robo**: Ja, gute Idee.  Wähle dazu für Deine Annahme einfach einen Namen, zum Beispiel `h`, und schreib `intro h`."
+  **Robo**: Ja, gute Idee.  Wähle dazu für deine Annahme einfach einen Namen, zum Beispiel `h`, und schreib `intro h`."
   intro hA
   Hint "**Du**: OK.  Jetzt habe ich also sowohl `{A}` als auch `{B}` in meinen Annahmen und muss `{A} ∧ {B}` zeigen.
 
-  **Robo**:  Genau.  Und wie das geht, weißt Du ja schon."
+  **Robo**:  Genau.  Und wie das geht, weißt du ja schon."
   constructor
   assumption
   assumption
diff --git a/server/adam/Adam/Levels/Implication/L06_Iff.lean b/server/adam/Adam/Levels/Implication/L06_Iff.lean
index fc022f0..73432b7 100644
--- a/server/adam/Adam/Levels/Implication/L06_Iff.lean
+++ b/server/adam/Adam/Levels/Implication/L06_Iff.lean
@@ -17,7 +17,7 @@ Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
 
   **Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
 
-  **Robo**: Genau. Entsprechend kannst Du auch hier mit `constructor` anfangen."
+  **Robo**: Genau. Entsprechend kannst du auch hier mit `constructor` anfangen."
   constructor
   Hint "**Du**: Ah, und die beiden Teile habe ich schon in den Annahmen."
   assumption
@@ -32,7 +32,7 @@ heißen bei `(h : A ↔ B)` die beiden Teile `h.mp` und `h.mpr`.
 
 **Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
 
-**Robo**: `mp` steht für Modus Ponens`.  Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen …  Ach nee, das wolltest Du ja nicht hören.  Das \"r\" in `mpr` steht für \"reverse\", weil's die Rückrichtung ist.
+**Robo**: `mp` steht für Modus Ponens`.  Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen …  Ach nee, das wolltest du ja nicht hören.  Das \"r\" in `mpr` steht für \"reverse\", weil's die Rückrichtung ist.
 "
 
 NewTactic constructor
diff --git a/server/adam/Adam/Levels/Implication/L07_Rw.lean b/server/adam/Adam/Levels/Implication/L07_Rw.lean
index ad12542..5ba2f53 100644
--- a/server/adam/Adam/Levels/Implication/L07_Rw.lean
+++ b/server/adam/Adam/Levels/Implication/L07_Rw.lean
@@ -33,7 +33,7 @@ Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) :
     sowas wie `A ↔ A` erhältst, kann `rfl` das beweisen.
 
     **Robo: Da fällt mir ein, `rw` wendet ohnehin auch versuchsweise `rfl` an. 
-  Das heißt, Du musst `rfl` nicht einmal ausschreiben."
+  Das heißt, du musst `rfl` nicht einmal ausschreiben."
     rw [h₂]
   rw [←h₂]
   assumption
diff --git a/server/adam/Adam/Levels/Implication/L08_Iff.lean b/server/adam/Adam/Levels/Implication/L08_Iff.lean
index 19820b5..ba0ba35 100644
--- a/server/adam/Adam/Levels/Implication/L08_Iff.lean
+++ b/server/adam/Adam/Levels/Implication/L08_Iff.lean
@@ -23,7 +23,7 @@ Statement (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
 
   **Du**: Weiß ich doch!"
   apply g
-  Hint "**Robo**: … und Du kannst die Implikation `{A} → {B}` genau gleich mit
+  Hint "**Robo**: … und du kannst die Implikation `{A} → {B}` genau gleich mit
   `apply {h}.mp` anwenden.
 
   **Du**: Aber normalerweise könnte ich hier auch `rw [← h]` sagen, oder?
diff --git a/server/adam/Adam/Levels/Implication/L09_Iff.lean b/server/adam/Adam/Levels/Implication/L09_Iff.lean
index d225eae..cb94a05 100644
--- a/server/adam/Adam/Levels/Implication/L09_Iff.lean
+++ b/server/adam/Adam/Levels/Implication/L09_Iff.lean
@@ -23,11 +23,11 @@ Statement (A B : Prop) : (A ↔ B) → (A → B) := by
   intro h
   Hint "**Du**: Also, ich kenne `rw [h]` und `apply h.mp`, aber das wollten wir ja diesmal vermeiden.
 
-  **Robo**: Was Du machen könntest, ist, mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
+  **Robo**: Was du machen könntest, ist, mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
   Teile aufteilen."
   Branch
     intro a
-    Hint "**Robo**: Hier müsstest Du jetzt `rw [←h]` oder `apply h.mp` benutzen.
+    Hint "**Robo**: Hier müsstest du jetzt `rw [←h]` oder `apply h.mp` benutzen.
     Geh lieber einen Schritt zurück, sodass das Goal `A → B` ist."
   rcases h with ⟨mp, mpr⟩
   Hint (hidden := true) "**Du**: Ah, und jetzt ist das Beweisziel in den Annahmen."
diff --git a/server/adam/Adam/Levels/Implication/L10_Apply.lean b/server/adam/Adam/Levels/Implication/L10_Apply.lean
index b883af1..e88a6ed 100644
--- a/server/adam/Adam/Levels/Implication/L10_Apply.lean
+++ b/server/adam/Adam/Levels/Implication/L10_Apply.lean
@@ -20,8 +20,8 @@ Statement (A : Prop) : ¬A ∨ A := by
   Hint "**Du**: Das scheint wieder ziemlich offensichtlich.
 
   **Robo**:  Nee, offensichtlich ist das nicht.  Aber ich glaube, es gibt ein wohlbekanntens Lemma, das hier weiterhilft:
-  `not_or_of_imp` besagt `(A → B) → ¬ A ∨ B`.  Da die rechte Seite der Implikation mit Deinem Beweisziel übereinstimmt, 
-  kannst Du es mit `apply not_or_of_imp` anwenden.
+  `not_or_of_imp` besagt `(A → B) → ¬ A ∨ B`.  Da die rechte Seite der Implikation mit deinem Beweisziel übereinstimmt, 
+  kannst du es mit `apply not_or_of_imp` anwenden.
 
   **Du**:  `Wohlbekannt` auf Implis?
 
@@ -30,12 +30,12 @@ Statement (A : Prop) : ¬A ∨ A := by
     right
     Hint "**Du**: Und jetzt?
 
-    **Robo**: `right/left` funktioniert hier nicht, da Du nicht weißt, ob `A` wahr oder falsch ist."
+    **Robo**: `right/left` funktioniert hier nicht, da du nicht weißt, ob `A` wahr oder falsch ist."
   Branch
     left
     Hint "**Du**: Und jetzt?
 
-    **Robo**: `right/left` funktioniert hier nicht, da Du nicht weißt, ob `A` wahr oder falsch ist."
+    **Robo**: `right/left` funktioniert hier nicht, da du nicht weißt, ob `A` wahr oder falsch ist."
   apply not_or_of_imp
   Hint (hidden := true) "**Robo**: Ich würde wieder mit `intro` weitermachen."
   intro
diff --git a/server/adam/Adam/Levels/Implication/L11_ByCases.lean b/server/adam/Adam/Levels/Implication/L11_ByCases.lean
index 7d749e0..ccdf73a 100644
--- a/server/adam/Adam/Levels/Implication/L11_ByCases.lean
+++ b/server/adam/Adam/Levels/Implication/L11_ByCases.lean
@@ -22,7 +22,7 @@ Wenn `A` wahr ist, beweisen wir die rechte Seite, sonst die Linke.
 Statement (A : Prop) : ¬A ∨ A := by
   Hint (hidden := true) "**Du**: Wie noch einmal?
 
-  **Robo**: Also `by_cases h : A` erstellt zwei Goals. Im ersten hast Du `(h : A)` zur
+  **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
   right
diff --git a/server/adam/Adam/Levels/Implication/L13_Summary.lean b/server/adam/Adam/Levels/Implication/L13_Summary.lean
index 11c82c0..660971a 100644
--- a/server/adam/Adam/Levels/Implication/L13_Summary.lean
+++ b/server/adam/Adam/Levels/Implication/L13_Summary.lean
@@ -15,7 +15,7 @@ Introduction
 "
 **Operationsleiter**: Ihr habt mir wirklich so geholfen!  Hier ist das letzte Problem.  Das habe ich von meinem Vorgänger geerbt.  Er hat behauptet, wenn wir das lösen können, dann läuft hier wieder alles.  Aber es sah mir immer viel zu schwierig aus, um es überhaupt zu versuchen. Wollt Ihr es einmal probieren?
 
-**Du**: Klar, zeig her!  Robo, kannst Du mir vielleicht auch noch einmal so eine nette Zusammenfassung anzeigen, was ich theoretisch in den letzten fünf Minuten gelernt habe?
+**Du**: Klar, zeig her!  Robo, kannst du mir vielleicht auch noch einmal so eine nette Zusammenfassung anzeigen, was ich theoretisch in den letzten fünf Minuten gelernt habe?
 
 **Robo**: Hier ist die Übersicht:     
 
@@ -49,8 +49,8 @@ Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
   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 gehst Du immer mit `intro` an."
+  **Robo**: Leider nicht. Da musst du manuell ran."
+  Hint (hidden := true) "**Robo**: Na Implikationen gehst du immer mit `intro` an."
   intro h
   intro ha
   Hint (hidden := true) "**Robo**: Ich würde mal die Annahme `h` mit `rcases` aufteilen."
diff --git a/server/adam/Adam/Levels/Inequality/L02_Pos.lean b/server/adam/Adam/Levels/Inequality/L02_Pos.lean
index f1a23bd..a32b5ac 100644
--- a/server/adam/Adam/Levels/Inequality/L02_Pos.lean
+++ b/server/adam/Adam/Levels/Inequality/L02_Pos.lean
@@ -50,5 +50,5 @@ LemmaTab "Nat"
 
 Conclusion "**Du**: Oh `simp` ist ja echt nicht schlecht…
 
-Die andere Person scheint beeindruckt, hat aber gleichzeitig auch das Bedürfnis, Dich aus
+Die andere Person scheint beeindruckt, hat aber gleichzeitig auch das Bedürfnis, dich aus
 der Reserve zu locken."
diff --git a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean
index 0cb1618..1509966 100644
--- a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean
+++ b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean
@@ -26,4 +26,4 @@ Statement (x y : ℤ) (h₂ : 5 * y ≤ 35 - 2 * x) (h₃ : 2 * y ≤ x + 3) : y
 
 Conclusion "**Du**: Boah, das ist schon gar nicht schlecht.
 
-Und damit endet auch Deine Erinnerung und wer weiss was du anschließend gemacht hast…"
+Und damit endet auch deine Erinnerung und wer weiss was du anschließend gemacht hast…"
diff --git a/server/adam/Adam/Levels/Lean.lean b/server/adam/Adam/Levels/Lean.lean
index ff5f672..d60af11 100644
--- a/server/adam/Adam/Levels/Lean.lean
+++ b/server/adam/Adam/Levels/Lean.lean
@@ -9,7 +9,7 @@ Title "Lean"
 
 Introduction
 "Während ihr weiter durch Täler, über Geröllhalden und zwischen monumentalen Steintürmen
-umherzieht, fragst Du eines Tages Robo.
+umherzieht, fragst du eines Tages Robo.
 
 **Du**: Sag mal, hast du dir je Gedanken dazu gemacht, wie du eigentlich funktionierts?
 
diff --git a/server/adam/Adam/Levels/Predicate.lean b/server/adam/Adam/Levels/Predicate.lean
index 202cbb4..e2f855b 100644
--- a/server/adam/Adam/Levels/Predicate.lean
+++ b/server/adam/Adam/Levels/Predicate.lean
@@ -30,9 +30,9 @@ Nun herrscht betretenes Schweigen.  Alle zucken mit den Schultern.
 
 **Du**: Ist das nicht ein Widerspruch?  
 
-**Robo**: Fragst Du, Du als Mathematiker?  Nein, das ist kein Widerspruch. Das ist einfach eine „reine Existenzaussage“.
+**Robo**: Fragst du, du als Mathematiker?  Nein, das ist kein Widerspruch. Das ist einfach eine „reine Existenzaussage“.
 
-Du bist Dir nicht ganz sicher, wie ernst er das meint.
+Du bist dir nicht ganz sicher, wie ernst er das meint.
 
 **Du**:  Dann ich schlage vor, wir übergeben das Päckchen einfach an *alle* Bewohner.  Dann haben wir es ja insbesondere der Königin übergeben.  
 
diff --git a/server/adam/Adam/Levels/Predicate/L01_Ring.lean b/server/adam/Adam/Levels/Predicate/L01_Ring.lean
index 3440023..af904a5 100644
--- a/server/adam/Adam/Levels/Predicate/L01_Ring.lean
+++ b/server/adam/Adam/Levels/Predicate/L01_Ring.lean
@@ -16,7 +16,7 @@ Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
   Hint "**Du**: Das ist doch Schulmathematik! Man rechnet das einfach aus,
   indem man die Terme umsortiert.
 
-  **Robo**: Wenn die Gleichung stimmt, kannst Du auf Leansch sogar einfach mit `ring` beweisen, dass das so ist.
+  **Robo**: Wenn die Gleichung stimmt, kannst du auf Leansch sogar einfach mit `ring` beweisen, dass das so ist.
 
   **Du**: Aber `ℕ` ist doch gar kein Ring?
 
diff --git a/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean
index c5b1ac5..073c907 100644
--- a/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean
+++ b/server/adam/Adam/Levels/Predicate/L03_Rewrite.lean
@@ -23,7 +23,7 @@ $$
 (a b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 := by
   Hint "**Du**: Hier muss man, glaube ich, einfach in Annahme `{g}` die Variable `{a}` durch `{b}` ersetzen.
 
-  **Robo**: Genau! Das machst Du mit `rw [{h}] at {g}`."
+  **Robo**: Genau! Das machst du mit `rw [{h}] at {g}`."
   rw [h] at g
   Hint (hidden := true) "**Robo**: Schau mal durch die Annahmen."
   assumption
diff --git a/server/adam/Adam/Levels/Predicate/L06_Exists.lean b/server/adam/Adam/Levels/Predicate/L06_Exists.lean
index 6b167ad..3b248e2 100644
--- a/server/adam/Adam/Levels/Predicate/L06_Exists.lean
+++ b/server/adam/Adam/Levels/Predicate/L06_Exists.lean
@@ -17,7 +17,7 @@ Title "Gerade/Ungerade"
 Introduction
 "
 Ihr habt nun alle Fragen aus dem königlichen Päckchen beantwortet, und die Formalosophinnen applaudieren.  Dann wollen Sie aber auch noch ein paar Fragen stellen, aber sie können sich nicht einigen, welche.  
-Ihr heute abwechselnd die Rufe „Even“ und „Odd“ aus der Menge heraus. Deshalb zeigt Dir Robo vorsichtshalber schon einmal die entsprechenden Definitionen an:
+Ihr heute abwechselnd die Rufe „Even“ und „Odd“ aus der Menge heraus. Deshalb zeigt dir Robo vorsichtshalber schon einmal die entsprechenden Definitionen an:
 
 ```
 def Even (n : ℕ) : Prop := ∃ r, n = r + r
@@ -33,14 +33,14 @@ Schließlich taucht von irgendwo aus der Menge folgendes Papier auf:
 "
 
 Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
-  Hint "**Robo**: Du kannst Dir mit `unfold Even` auch hier auf dem Papier die Definition sehen."
+  Hint "**Robo**: Du kannst dir mit `unfold Even` auch hier auf dem Papier die Definition sehen."
   Branch
     unfold Even
-    Hint "Robo**: Am besten machst Du auch noch `unfold Even at h`, damit Du verstehst, was los ist."
-  Hint "**Robo**: Wie Du oben siehst, ist `Even n` dadurch definiert,
+    Hint "Robo**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst, was los ist."
+  Hint "**Robo**: Wie du oben siehst, ist `Even n` dadurch definiert,
     dass ein `r` existiert so dass `r + r = n` ist. Am besten
     öffnest du diese Definition mit `unfold Even at *` einmal.
-    Dann siehst Du besser, was los ist. "
+    Dann siehst du besser, was los ist. "
   unfold Even at *
   Hint "**Du**: Also von `{h}` weiß ich jetzt, dass ein `r` existiert, so dass `r + r = n` …
 
@@ -50,17 +50,17 @@ Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
 
   **Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
   Hint (hidden := true) "**Robo**: Also sowas ähnliches wie `use 4 * r ^ 3`, aber ich kann
-  Dir leider nicht sagen, welche Zahl passt.
+  dir leider nicht sagen, welche Zahl passt.
   "
   Branch
     rw [hr]
-    Hint "**Robo**: Das geht auch, jetzt musst Du aber wirklich `use` verwenden."
+    Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
     use 2 * r ^ 2
     ring
   use 2 * r ^ 2
   Hint "**Du**: Ah, und jetzt `ring`!
 
-  **Robo**: Aber zuerst musst Du noch mit
+  **Robo**: Aber zuerst musst du noch mit
   `rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiß."
   rw [hr]
   ring
diff --git a/server/adam/Adam/Levels/Predicate/L07_Exists.lean b/server/adam/Adam/Levels/Predicate/L07_Exists.lean
index 30d2ee3..c6b1492 100644
--- a/server/adam/Adam/Levels/Predicate/L07_Exists.lean
+++ b/server/adam/Adam/Levels/Predicate/L07_Exists.lean
@@ -23,10 +23,10 @@ Statement odd_square (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by
   unfold Odd at *
   rcases h with ⟨r, hr⟩
   Hint "**Robo**: Ich hab noch einen Trick auf Lager:
-  Wenn du jetzt herausfinden willst, welche Zahl Du einsetzen musst, könntest
+  Wenn du jetzt herausfinden willst, welche Zahl du einsetzen musst, könntest
   Du schon jetzt mit `rw [{hr}]` weitermachen …"
   rw [hr]
-  Hint "**Robo**: Wenn Du jetzt `ring` benötigst, dann schreibt es einfach alles in
+  Hint "**Robo**: Wenn du jetzt `ring` benötigst, dann schreibt es einfach alles in
   Normalform um, das hilft beim Vergleichen."
   ring
   Hint "**Du**: Was bedeutet `ring_nf`?
diff --git a/server/adam/Adam/Levels/Predicate/L08_Forall.lean b/server/adam/Adam/Levels/Predicate/L08_Forall.lean
index a8ec81d..4e18c7d 100644
--- a/server/adam/Adam/Levels/Predicate/L08_Forall.lean
+++ b/server/adam/Adam/Levels/Predicate/L08_Forall.lean
@@ -37,7 +37,7 @@ Nach längerem Durcheinander findet ein weiteres Blatt aus der Menge zu Euch.
 Statement : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
   Hint "**Du**: Das `∀` heisst sicher \"für alle\".
 
-  **Robo**: Und man schreibt `\\forall`. Ein `∀ x, …` im Beweisziel kannst Du wie eine
+  **Robo**: Und man schreibt `\\forall`. Ein `∀ x, …` im Beweisziel kannst du wie eine
   Implikation mit `intro x` angehen."
   intro x h
   unfold Even at h
diff --git a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean
index 8771d83..74449f2 100644
--- a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean
+++ b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean
@@ -32,7 +32,7 @@ open Nat
 Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
   Hint "**Du**: Ich würde gern diese Negation `¬` am Quantor vorbeischieben.
 
-  **Robo**: `push_neg` macht genau das!  Oder Du könntest `rw` mit den folgenden Lemmas verwenden:
+  **Robo**: `push_neg` macht genau das!  Oder du könntest `rw` mit den folgenden Lemmas verwenden:
 
   ```
   not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)
@@ -44,12 +44,12 @@ Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
     push_neg
     Hint "**Robo**: Dieser Lösungsweg scheint mir etwas zu schwierig. 
     Ich würde nochmal zurückgehen und schauen,
-    dass Du irgendwie `¬Odd` erhältst.
-    Das kannst Du dann mit `rw [←even_iff_not_odd]`
+    dass du irgendwie `¬Odd` erhältst.
+    Das kannst du dann mit `rw [←even_iff_not_odd]`
     zu `Even` umwandeln."
   push_neg
   intro n
-  Hint "**Robo**: Jetzt brauchst Du eine Zahl mit `use`, und danach vermutlich das Lemma `←even_iff_not_odd` brauchen.
+  Hint "**Robo**: Jetzt brauchst du eine Zahl mit `use`, und danach vermutlich das Lemma `←even_iff_not_odd` brauchen.
 
   **Du**: Könnte ich jetzt schon `rw [←even_iff_not_odd]` anwenden?
 
@@ -61,19 +61,19 @@ Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
   Ich würde jetzt lieber mit `use` eine richtige Zahl angeben, und danach umschreiben."
   Branch
     use n + 2
-    Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
+    Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
   Branch
     use n + 4
-    Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
+    Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
   use n
-  Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
+  Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
   rw [←even_iff_not_odd]
   unfold Even
   use n
   --ring
 
 Conclusion "Die Formalosophinnen sind ganz begeistert.  
-Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage.
+Nachdem sich der Beifall gelegt hat, hast du auch einmal eine Frage.
 
 **Du**: Kann uns hier irgendjemand vielleicht ein bisschen Orientierung im Formaloversum geben?
 
@@ -83,7 +83,7 @@ Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage.
 
 Die Frage war wieder zu konkret.  Betretenes Schweigen.
 
-**Robo**:  Lass nur.  Ich schlage vor, wir machen als nächstes einen Ausflug auf den Asteroiden da drüben.  Und bevor Du fragst – hier ist wieder ein Überblick, was Du auf diesem Planeten gelernt hast.
+**Robo**:  Lass nur.  Ich schlage vor, wir machen als nächstes einen Ausflug auf den Asteroiden da drüben.  Und bevor du fragst – hier ist wieder ein Überblick, was du auf diesem Planeten gelernt hast.
 
 |               | Beschreibung                |
 |:--------------|:----------------------------|
diff --git a/server/adam/Adam/Levels/Proposition.lean b/server/adam/Adam/Levels/Proposition.lean
index ac5e3e3..fbea081 100644
--- a/server/adam/Adam/Levels/Proposition.lean
+++ b/server/adam/Adam/Levels/Proposition.lean
@@ -19,21 +19,21 @@ Title "Logo"
 
 Introduction "
 Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
-bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
-Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
+bist du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
+Richte dich besser darauf ein, hier bleiben und dich zurechtzufinden zu müssen.
 
 Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
 sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
 seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
-herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
-keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
+herumgesprochen, dass du in deinem früheren Universum Mathematiker warst. Du wirst hier
+keine Ruhe finden, solange du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
 
 Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
 überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik
-exklusiv in einem Dir fremden Dialekt, den sie Leansch [liːnʃ] nennen.
+exklusiv in einem dir fremden Dialekt, den sie Leansch [liːnʃ] nennen.
 
-Zum Glück hat Robo mit Dir das Universum gewechselt.
-Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir
+Zum Glück hat Robo mit dir das Universum gewechselt.
+Robo, das ist dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die du Dir
 in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leansch gelernt.
 Und das ist Gold wert.
 "
diff --git a/server/adam/Adam/Levels/Proposition/L00_Tauto.lean b/server/adam/Adam/Levels/Proposition/L00_Tauto.lean
index e4de457..bc0d692 100644
--- a/server/adam/Adam/Levels/Proposition/L00_Tauto.lean
+++ b/server/adam/Adam/Levels/Proposition/L00_Tauto.lean
@@ -14,7 +14,7 @@ Gerade seid Ihr auf Königin *Logisindes* Planeten. Sie kommt ohne Umschweife zu
 **Logisinde**  Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt …
 
 Und sie kritzelt etwas auf ein Stück Papier:  oben ein paar Annahmen, unten eine Schlussfolgerung.
-Dazwischen sollst Du offenbar einen Beweis eintragen.
+Dazwischen sollst du offenbar einen Beweis eintragen.
 Du siehst Robo hilflos an.
 "
 
@@ -23,7 +23,7 @@ Statement ""
     ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
   Hint "**Robo**  Das ist ganz einfach.  Mit `{A} {B} {C} : Prop` meint sie:
   `{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
-  Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
+  Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst du, oder?
 
   **Du** Ehhm, ja.  Aber da muss ich jetzt trotzdem erst einmal überlegen.
 
diff --git a/server/adam/Adam/Levels/Proposition/L01_Rfl.lean b/server/adam/Adam/Levels/Proposition/L01_Rfl.lean
index 984e7f9..f15ccb2 100644
--- a/server/adam/Adam/Levels/Proposition/L01_Rfl.lean
+++ b/server/adam/Adam/Levels/Proposition/L01_Rfl.lean
@@ -14,7 +14,7 @@ Fragen stellen würden. Logisinde winkt den ersten nach vorn. Er räuspert sich.
 **Untertan** Warum ist $42 = 42$?
 
 Du schaust ihn fassungslos an.
-Er schreibt es Dir wieder auf.
+Er schreibt es dir wieder auf.
 "
 
 Statement "" :
diff --git a/server/adam/Adam/Levels/Proposition/L02_Assumption.lean b/server/adam/Adam/Levels/Proposition/L02_Assumption.lean
index e3101cb..8466041 100644
--- a/server/adam/Adam/Levels/Proposition/L02_Assumption.lean
+++ b/server/adam/Adam/Levels/Proposition/L02_Assumption.lean
@@ -18,7 +18,7 @@ Statement ""
 
 **Du** Warum schreibt er dann nicht `{n} ∈ ℕ`??
 
-**Robo** Weil das hier alles komische Typen sind …  Ich kann Dir das später mal in Ruhe erklären.
+**Robo** Weil das hier alles komische Typen sind …  Ich kann dir das später mal in Ruhe erklären.
 Jetzt will ich erst einmal die Frage entschlüsseln.
 
 **Robo** Also, `{h₁}`, `{h₂}`, `{h₃}` sind einfach nur Namen für verschiedene Annahmen, und zwar
diff --git a/server/adam/Adam/Levels/Proposition/L03_Assumption.lean b/server/adam/Adam/Levels/Proposition/L03_Assumption.lean
index f341cbc..2f1ee24 100644
--- a/server/adam/Adam/Levels/Proposition/L03_Assumption.lean
+++ b/server/adam/Adam/Levels/Proposition/L03_Assumption.lean
@@ -20,7 +20,7 @@ Statement ""
 
 **Du** Und unter dieser Annahme sollen wir jetzt `{A}` beweisen?
 
-**Robo** Ja.  Da kommst Du jetzt selbst drauf, wie das geht, oder?
+**Robo** Ja.  Da kommst du jetzt selbst drauf, wie das geht, oder?
 "
   Hint (hidden := true) "**Robo**: Ist doch genau wie eben:
 die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
diff --git a/server/adam/Adam/Levels/Proposition/L04_True.lean b/server/adam/Adam/Levels/Proposition/L04_True.lean
index 2be1ea1..9332c3c 100644
--- a/server/adam/Adam/Levels/Proposition/L04_True.lean
+++ b/server/adam/Adam/Levels/Proposition/L04_True.lean
@@ -18,7 +18,7 @@ bedingungslos wahr ist.
 
 **Du** Und was genau ist dann zu beweisen?
 
-**Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben.
+**Robo** Ich glaube, nichts. Ich glaube, du kannst einfach `trivial` schreiben.
 "
   trivial
 
diff --git a/server/adam/Adam/Levels/Proposition/L06_False.lean b/server/adam/Adam/Levels/Proposition/L06_False.lean
index 7f9ebb1..6b888e6 100644
--- a/server/adam/Adam/Levels/Proposition/L06_False.lean
+++ b/server/adam/Adam/Levels/Proposition/L06_False.lean
@@ -28,7 +28,7 @@ Insbesondere die gesuchte Aussage `{A}`.
 
 **Du** Und wie erkläre ich das jetzt diesem Formalosophen?
 
-**Robo** Ich glaube, Du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen
+**Robo** Ich glaube, du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen
 Annahme `True` und seiner Annahme `False` ein Widerspruch besteht.  Probier mal `contradiction`."
   contradiction
 
diff --git a/server/adam/Adam/Levels/Proposition/L09_And.lean b/server/adam/Adam/Levels/Proposition/L09_And.lean
index 3ba43a8..2c0096e 100644
--- a/server/adam/Adam/Levels/Proposition/L09_And.lean
+++ b/server/adam/Adam/Levels/Proposition/L09_And.lean
@@ -41,7 +41,7 @@ konstruieren kann.
 **Robo**: Schau mal, das ist Zauberpapier.
 Jetzt haben wir auf einmal zwei Beweisziele.
 Hier ist dast Ziel `{A}`.
-Ich glaube, Du weißt schon, wie man die jeweils erreicht.
+Ich glaube, du weißt schon, wie man die jeweils erreicht.
 Die Ziele stehen ja jeweils in den *Annahmen*.
 "
   assumption
@@ -50,7 +50,7 @@ Die Ziele stehen ja jeweils in den *Annahmen*.
 **Robo**: Schau mal, das ist Zauberpapier.
 Jetzt haben wir auf einmal zwei Beweisziele.
 Hier ist dast Ziel `{B}`.
-Ich glaube, Du weißt schon, wie man die jeweils erreicht.
+Ich glaube, du weißt schon, wie man die jeweils erreicht.
 Die Ziele stehen ja jeweils in den *Annahmen*.
 "
   assumption
@@ -62,7 +62,7 @@ Conclusion
 
 Ihm scheinen diese Fragen inzwischen Spaß zu machen.
 
-**Robo** Meinst Du, dieser Hebel, an dem \"Editor mode\" steht, ist echt?
+**Robo** Meinst du, dieser Hebel, an dem \"Editor mode\" steht, ist echt?
 Oder ist der nur gemalt?  Probier mal!
 "
 
diff --git a/server/adam/Adam/Levels/Proposition/L10_And.lean b/server/adam/Adam/Levels/Proposition/L10_And.lean
index 0d4de0a..5422d66 100644
--- a/server/adam/Adam/Levels/Proposition/L10_And.lean
+++ b/server/adam/Adam/Levels/Proposition/L10_And.lean
@@ -23,8 +23,8 @@ Statement ""
 
 **Du** Moment, wie schreib ich *das* denn hier auf?
 
-**Robo** Die bleiden Klammern schreibst Du als `\\<` und `\\>`, oder gleichzeitig als `\\<>`.
-Und h₁ schreibst Du einfach als `h\\1`.  Aber Du kannst Dir auch einfach andere Namen
+**Robo** Die bleiden Klammern schreibst du als `\\<` und `\\>`, oder gleichzeitig als `\\<>`.
+Und h₁ schreibst du einfach als `h\\1`.  Aber du kannst dir auch einfach andere Namen
 für `h₁` und `h₂`, zum Beispiel `rcases {h} with ⟨hA, hBC⟩`
 "
   Branch
diff --git a/server/adam/Adam/Levels/Proposition/L11_Or.lean b/server/adam/Adam/Levels/Proposition/L11_Or.lean
index b3642a9..68904cc 100644
--- a/server/adam/Adam/Levels/Proposition/L11_Or.lean
+++ b/server/adam/Adam/Levels/Proposition/L11_Or.lean
@@ -20,8 +20,8 @@ Statement
     (A B : Prop) (hA : A) : A ∨ (¬ B) := by
   Hint "**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
 
-**Robo** Nein, viel einfacher.  Wenn Du eine Oder-Aussage beweisen sollst, musst Du Dich
-einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
+**Robo** Nein, viel einfacher.  Wenn du eine Oder-Aussage beweisen sollst, musst du Dich
+einfach entscheiden, ob du die linke oder rechte Seite beweisen willst.
 
 **Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde?
 Ich will natürlich `{A}` beweisen!
@@ -29,7 +29,7 @@ Ich will natürlich `{A}` beweisen!
 **Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?"
   Branch
     right
-    Hint "**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast.  Probier's nochmal."
+    Hint "**Robo** Wusste gar nicht, dass du eine Links-Rechts-Schwäche hast.  Probier's nochmal."
   left
   assumption
 
diff --git a/server/adam/Adam/Levels/Proposition/L12_Or.lean b/server/adam/Adam/Levels/Proposition/L12_Or.lean
index 8c6959c..58538d7 100644
--- a/server/adam/Adam/Levels/Proposition/L12_Or.lean
+++ b/server/adam/Adam/Levels/Proposition/L12_Or.lean
@@ -37,16 +37,16 @@ Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten we
 **Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`."
   rcases h with h | h
   Hint "**Robo**
-Jetzt musst Du Dein Ziel zweimal beweisen:
+Jetzt musst du dein Ziel zweimal beweisen:
 Einmal unter Annahme der linken Seite `{A} ∨ {B}`,
 und einmal unter Annahme der rechten Seite `{A}`.
 Hier haben nehmen wir an, die linke Seite
 sei wahr."
   Hint (hidden := true) " **Robo** Wie man mit einem Und in den Annahmen umgeht,
-weißt Du doch schon:
-`rcases h with ⟨h₁, h₂⟩`.  Zur Erinnerung: Für die Klammern schreibst Du `\\<>`."
+weißt du doch schon:
+`rcases h with ⟨h₁, h₂⟩`.  Zur Erinnerung: Für die Klammern schreibst du `\\<>`."
   rcases h with ⟨h₁, h₂⟩
-  Hint "**Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
+  Hint "**Robo** Jetzt musst du dein Ziel zweimal beweisen:
 Einmal unter Annahme der linken Seite `{A}`,
 und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
 sei wahr."
@@ -55,10 +55,10 @@ sei wahr."
 
 Conclusion
 "**Du**  Ok, das scheint ihn zufriedenzustellen. Nur noch eine Seele…
-Kannst Du mir vorher noch einmal kurz alles Leansch zusammenfassen,
-das Du mir bis hierher beigebracht hast?
+Kannst du mir vorher noch einmal kurz alles Leansch zusammenfassen,
+das du mir bis hierher beigebracht hast?
 
-Robo strahlt überglücklich.  Noch *nie* warst Du so auf ihn angewiesen.
+Robo strahlt überglücklich.  Noch *nie* warst du so auf ihn angewiesen.
 
 **Robo** Na klar, schau her!
 
@@ -89,7 +89,7 @@ Robo strahlt überglücklich.  Noch *nie* warst Du so auf ihn angewiesen.
 
 ## Taktiken
 
-Die Worte, die Du aktiv gebrauchen musst, heißen zusammengefasst `Taktiken`.  Hier sind alle Taktiken, die wir auf diesem Planeten gebraucht haben:
+Die Worte, die du aktiv gebrauchen musst, heißen zusammengefasst `Taktiken`.  Hier sind alle Taktiken, die wir auf diesem Planeten gebraucht haben:
 
 |    | Taktik                    | Beispiel                                          |
 |:---|:--------------------------|:--------------------------------------------------|
@@ -102,7 +102,7 @@ Die Worte, die Du aktiv gebrauchen musst, heißen zusammengefasst `Taktiken`.  H
 | 7ᵃ | `rcases h with ⟨h₁, h₂⟩`  | Teilt ein UND in den Annahmen auf.                |
 | 7ᵇ | `rcases h with h \\| h`   | Teilt ein ODER in den Annahmen in zwei Fälle auf. |
 
-**Du** Woher weißt Du das eigentlich alles?
+**Du** Woher weißt du das eigentlich alles?
 
 **Robo** Keine Ahnung.  War, glaube ich, vorinstalliert.
 "
diff --git a/server/adam/Adam/Levels/Proposition/L13_Summary.lean b/server/adam/Adam/Levels/Proposition/L13_Summary.lean
index 8d4c151..7f16956 100644
--- a/server/adam/Adam/Levels/Proposition/L13_Summary.lean
+++ b/server/adam/Adam/Levels/Proposition/L13_Summary.lean
@@ -14,8 +14,8 @@ Introduction
 "
 Der letzte Untertan tritt vor.  Ihr Anliegen ist etwas komplizierter als die vorherigen.
 
-**Robo** Wirf einfach alles drauf, was Du gelernt hast.
-Hier, ich bin sogar so nett und zeig Dir noch einmal die vier
+**Robo** Wirf einfach alles drauf, was du gelernt hast.
+Hier, ich bin sogar so nett und zeig dir noch einmal die vier
 wichtigsten Taktiken für diese Situation an.
 
 | (Übersicht) | Und (`∧`)                | Oder (`∨`)              |
@@ -45,7 +45,7 @@ Statement ""
         right
         assumption
   rcases h
-  Hint (hidden := true) "**Robo**: Jetzt kannst Du das `∧` im Goal mit `constructor` angehen."
+  Hint (hidden := true) "**Robo**: Jetzt kannst du das `∧` im Goal mit `constructor` angehen."
   · constructor
     · left
       assumption
@@ -80,26 +80,26 @@ Statement ""
 
 
 -- 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."
+-- "**Robo** Das `∧` im Goal kannst du mit `constructor` zerlegen."
 
 -- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (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) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
--- "**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) (h : A ∨ (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."
 
 
 -- 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."
+-- "**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?
 

From 96a8da9d9317884918eb7213684c5ba5616369b1 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 31 Mar 2023 12:10:09 +0200
Subject: [PATCH 3/3] Apply suggestions from code review

---
 server/adam/Adam.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/adam/Adam.lean b/server/adam/Adam.lean
index 884e426..1402b0c 100644
--- a/server/adam/Adam.lean
+++ b/server/adam/Adam.lean
@@ -27,7 +27,7 @@ Introduction
 
 Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du computer-gestützte
 Beweisführung. Das Interface ist etwas vereinfacht, aber wenn du den *Editor Mode* aktivierst, fühlt es sich 
-fast genauso an wie eine professionalle IDE, etwa VSCode.
+fast genauso an wie in VSCode, der standard IDE für Lean.
 
 Rechts siehst du eine Übersicht. Das Spiel besteht aus mehreren Planeten, und jeder Planet hat mehrere Levels,
 die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden grün.