From c88326577690ed48c2a21e46855d5d3d0cfea70a Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 16 Mar 2023 13:24:34 +0100
Subject: [PATCH] levels

---
 server/testgame/TestGame/LemmaDocs.lean       |  2 ++
 .../TestGame/Levels/Inequality/L01_LE.lean    |  3 +-
 .../Levels/Lean/L04_InstanceArguments.lean    |  4 +--
 .../testgame/TestGame/Levels/SetTheory.lean   |  2 +-
 .../TestGame/Levels/SetTheory/L01_Univ.lean   | 35 +++++++++----------
 .../TestGame/Levels/SetTheory/L02_Empty.lean  | 13 +++----
 .../TestGame/Levels/SetTheory/L03_Subset.lean | 15 ++++----
 .../TestGame/Levels/Sum/T01_Induction.lean    |  2 --
 .../TestGame/Levels/Sum/T02_Induction.lean    |  1 -
 9 files changed, 38 insertions(+), 39 deletions(-)

diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index d4af11a..ff18389 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -204,3 +204,5 @@ LemmaDoc congrFun as "congrFun" in "Function"
 
 LemmaDoc Iff.symm as "Iff.symm" in "Logic"
 ""
+
+DefinitionDoc subset as "⊆" "Test"
diff --git a/server/testgame/TestGame/Levels/Inequality/L01_LE.lean b/server/testgame/TestGame/Levels/Inequality/L01_LE.lean
index 81eec99..d03dcce 100644
--- a/server/testgame/TestGame/Levels/Inequality/L01_LE.lean
+++ b/server/testgame/TestGame/Levels/Inequality/L01_LE.lean
@@ -30,4 +30,5 @@ Statement
 
 OnlyTactic rfl
 
-Conclusion "**Du**: Ha. ha… Na aber jetzt mal ehrlich, wie funktioniert das eigentlich?"
+Conclusion "**Du**: Ha. ha… Na aber jetzt mal ehrlich, könnt ihr mir ein bisschen mehr
+erzählen?"
diff --git a/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean b/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean
index 380a181..8339fbf 100644
--- a/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean
+++ b/server/testgame/TestGame/Levels/Lean/L04_InstanceArguments.lean
@@ -51,7 +51,7 @@ sein neustes Buch, das er leider nicht lesen kann. Nich tnur ist es der zweite B
 (der Erste hat offensichtlich was mit \"Urbildern\" zu tun), sondern ist es auch in einem
 Dialekt geschrieben, der anscheinend nur auf einem Nachbarsmond gesprochen wird.
 
-Ihr beschliesst dem herzlichen Golem zu helfen und sowohl dem Mond einen Besuch abzustatten,
-um den Dialekt zu lernen, wie auch auf dem zweiten Mond in der Bibliothek nach dem
+Ihr beschliesst dem herzlichen Golem zu helfen und beiden Monden einen Besuch abzustatten,
+sowohl um den Dialekt zu lernen, wie auch in der Bibliothek auf dem anderen Mond nach dem
 ersten Band zu suchen.
 "
diff --git a/server/testgame/TestGame/Levels/SetTheory.lean b/server/testgame/TestGame/Levels/SetTheory.lean
index 0f9a789..298c096 100644
--- a/server/testgame/TestGame/Levels/SetTheory.lean
+++ b/server/testgame/TestGame/Levels/SetTheory.lean
@@ -34,7 +34,7 @@ vermutlich noch viel besser mit alter Sprache und Schrift auskennt.
 
 **Du**: Hoffen wir, dass sie uns weiterhelfen können dieses Buch der Urbilder zu entschlüsseln.
 
-Sofort begrüßt euch eine ältere Frau, die sich als *Mengitte*, die Beschützerin des Mondes,
+Sofort begrüßt euch eine ältere Frau, die sich als *Mengea*, die Beschützerin des Mondes,
 vorstellt.
 "
 
diff --git a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
index e46618c..8e67b91 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
@@ -14,11 +14,11 @@ Title "Mengen"
 
 Introduction
 "
-**Mengitte**: Ich würde leider den Inhalt jenes Buches eh nicht verstehen. Aber der beste Weg für
+**Mengea**: Ich würde leider den Inhalt jenes Buches eh nicht verstehen. Aber der beste Weg für
 euch, dieses zu entschlüsseln ist, euch ausgiebig mit der Bevölkerung hier zu unterhalten.
 Lebt mit ihnen, redet mit ihnen und ihr werdet die Sprache automatisch lernen.
 
-**Mengitte**: Seit aber vorgewarnt, die Leute hier denken ganz viel über Mengen nach,
+**Mengea**: Seit aber vorgewarnt, die Leute hier denken ganz viel über Mengen nach,
 womit sie immer *homogene Mengen* meinen. Eine Menge natürlicher Zahlen `{1, 4, 6}` ist
 verständlich, aber sowas wie eine Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` gibt es hier
 einfach nicht. Punkt.
@@ -26,35 +26,32 @@ einfach nicht. Punkt.
 **Robo**: Als Kontext: Wenn `A` ein beliebiger `Type` ist, dann ist `(U : Set A)` eine Menge
 mit Elementen aus `A`
 
-**Mengitte**: Damit ich weiss, dass ihr euch grundsätzlich mit den Leuten austauschen könnt,
+**Mengea**: Damit ich weiss, dass ihr euch grundsätzlich mit den Leuten austauschen könnt,
 erklärt mir doch folgendes:
 "
 
 open Set
 
 Statement mem_univ "" {A : Type} (x : A) : x ∈ (univ : Set A) := by
-  trivial
-
-Hint (A : Type) (x : A) : x ∈ (univ : Set A) =>
-"**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
+  Hint "**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
 
-**Robo** … und `univ` ist die Menge aller Elemente in `A`.
+  **Robo** … und `univ` ist die Menge aller Elemente in `A`.
 
-**Du** ist das nicht einfach `A` selber?
+  **Du** ist das nicht einfach `A` selber?
 
-**Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
+  **Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
 
-**Du**: Unlogisch.
+  **Du**: Unlogisch.
 
-**Mengites**: Naja, Typen und Mengen sind halt zwei unterschiedliche Sachen und wenn ihr
-über Mengen sprechen wollt, müssen alles Mengen sein.
+  **Mengites**: Naja, Typen und Mengen sind halt zwei unterschiedliche Sachen und wenn ihr
+  über Mengen sprechen wollt, müssen alles Mengen sein.
 
-**Du**: Na gut. Und wieso `x ∈ univ` und nicht `x : univ` wie bei Typen?
+  **Du**: Na gut. Und wieso `x ∈ univ` und nicht `x : univ` wie bei Typen?
 
-**Robo**: Jedes Element `(x : A)` hat entweder die Eigenschaft `x ∈ U` oder `x ∉ U` für eine
-Menge `(U : Set A)`. (`\\in`, `\\nin`)
+  **Robo**: Jedes Element `(x : A)` hat entweder die Eigenschaft `x ∈ U` oder `x ∉ U` für eine
+  Menge `(U : Set A)`. (`\\in`, `\\nin`)
 
-**Du**: Also das ist ja dann trivial. Hoffentlich sehen die das hier auch so…
-"
+  **Du**: Also das ist ja dann `trivial`. Hoffentlich sehen die das hier auch so…"
+  trivial
 
-Conclusion "**Mengitte**: Ja das stimmt schon. Dann wünsche ich euch viel Erfolg auf eurer Reise!"
+Conclusion "**Mengea**: Ja das stimmt schon. Dann wünsche ich euch viel Erfolg auf eurer Reise!"
diff --git a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
index 193a6a6..a990e16 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
@@ -20,15 +20,16 @@ open Set
 
 Statement not_mem_empty "" {A : Type} (x : A) :
     x ∉ (∅ : Set A) := by
+  Hint "**Du**: Kein Element ist in der leeren Menge enthalten? Das ist ja alles
+  tautologisches Zeugs...
+
+  **Robo**: Dann behaupte das doch."
   tauto
 
 NewLemma mem_univ
 
-Hint (A : Type) (x : A) : x ∉ (∅ : Set A) =>
-"**Du**: Kein Element ist in der leeren Menge enthalten? Das ist ja alles tautologisches Zeugs...
-
-**Robo**: Dann behaupte das doch. (`\\empty`)"
-
 Conclusion "Der Junge rennt weiter.
 
-**Du**: So wird das ganze schon angenehmer."
+**Du**: So wird das ganze schon angenehmer.
+
+**Robo**: Die Leere Menge schreibst du mit `\\empty` falls du die nochmals brauchst."
diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
index a876537..5fd9ccb 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
@@ -13,6 +13,10 @@ Title "Teilmengen"
 
 Introduction
 "
+Ihr bemerkt, dass mit dem Jungen noch zwei andere
+Kinder zuhörten. Eines der beiden Mädchen hat ebenfalls eine Frage.
+
+
 Hat man zwei Mengen `(A B : Set ℕ)` kann man fragen, ob diese Teilmengen
 voneinander sind: `A ⊆ B` (`\\sub`/`\\ss`) ist die Notation für Teilmengen, die auch gleich
 sein können.
@@ -28,18 +32,15 @@ namespace MySet
 
 open Set
 
--- theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by
---   trivial
-
--- theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
---   tauto
+Statement (A : Set ℕ) : A ⊆ univ := by
+  Hint "**Robo**: `A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert.
 
-Statement subset_empty_iff
-"." (A : Set ℕ) : A ⊆ univ := by
+  **Du**: Also kann ich mit `intro` anfangen, wie ich das bei einem `∀`?"
   intro h hA
   trivial --apply mem_univ -- or `trivial`.
 
 NewTactic intro trivial apply
+NewDefinition subset
 -- blocked: tauto simp
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/Sum/T01_Induction.lean b/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
index 1e2c033..9b095f7 100644
--- a/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
@@ -36,5 +36,3 @@ example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n
 | 0 | 1 | 2 | 3 | 4 => by
   sorry
 | n + 5  => by sorry
-
-NewTactic rw simp ring
diff --git a/server/testgame/TestGame/Levels/Sum/T02_Induction.lean b/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
index aa25628..b424a4d 100644
--- a/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
+++ b/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
@@ -32,4 +32,3 @@ Statement
 --   ring
 --   rw [Nat.succ_eq_one_add]
 --   rw []
-NewTactic rw simp ring