levels

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"

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?"

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.
 "

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.
 "
 

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
+  Hint "**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
+
+  **Robo** … und `univ` ist die Menge aller Elemente in `A`.
+
+  **Du** ist das nicht einfach `A` selber?
+
+  **Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
+
+  **Du**: Unlogisch.
+
+  **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?
+
+  **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…"
   trivial
 
-Hint (A : Type) (x : A) : x ∈ (univ : Set A) =>
-"**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
-
-**Robo** … und `univ` ist die Menge aller Elemente in `A`.
-
-**Du** ist das nicht einfach `A` selber?
-
-**Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
-
-**Du**: Unlogisch.
-
-**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?
-
-**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…
-"
-
-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!"

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."

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
+Statement (A : Set ℕ) : A ⊆ univ := by
+  Hint "**Robo**: `A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert.
 
--- theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
---   tauto
-
-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

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

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