levels

server/testgame/TestGame/LemmaDocs.lean

@@ -153,6 +153,9 @@ LemmaDoc Fin.sum_univ_castSucc as "Fin.sum_univ_castSucc" in "Sum"
 LemmaDoc Nat.succ_eq_add_one as "Nat.succ_eq_add_one" in "Sum"
 ""
 
+LemmaDoc Nat.zero_eq as "Nat.succ_eq_add_one" in "Sum"
+""
+
 LemmaDoc add_comm as "add_comm" in "Nat"
 ""
 
@@ -205,4 +208,4 @@ LemmaDoc congrFun as "congrFun" in "Function"
 LemmaDoc Iff.symm as "Iff.symm" in "Logic"
 ""
 
-DefinitionDoc subset as "⊆" "Test"
+DefinitionDoc Symbol.Subset as "⊆" "Test"

server/testgame/TestGame/Levels/Implication/L03_Apply.lean

@@ -11,17 +11,10 @@ Introduction
 "
 Sein Kollege zieht eine Linie unter deinen Beweis, schreibt ein durchgestrichenes ~`revert`~
 hin und gibt dir das Blatt wieder.
-`revert` ist aber nur selten der richtige Weg.
-
-Im vorigen Beispiel würde man besser die Implikation $A \\Rightarrow B$ *anwenden*, also
-sagen \"Es genügt $A$ zu zeigen, denn $A \\Rightarrow B$\" und danach $A$ beweisen.
-
-Wenn man eine Implikation `(g : A → B)` in den Annahmen hat, bei welcher die Konsequenz
-(also $B$) mit dem Goal übereinstimmt, kann man `apply g` genau dies machen.
 "
 
 Statement (A B : Prop) (hA : A) (h : A → B) : B := by
-  Hint "**Robo**: Du hast natürlich recht, normalerweise ist es viel schöner mit
+  Hint "**Robo**: Da hat er natürlich recht, normalerweise ist es viel schöner mit
   `apply {h}` die Implikation anzuwenden."
   apply h
   Hint "**Du**: Und jetzt genügt es also `A` zu zeigen."

server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean

@@ -2,6 +2,7 @@ import TestGame.Metadata
 
 import Mathlib.Init.Set
 import Mathlib.Tactic.Tauto
+import Mathlib
 
 set_option tactic.hygienic false
 
@@ -35,12 +36,16 @@ open Set
 Statement (A : Set ℕ) : A ⊆ univ := by
   Hint "**Robo**: `A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert.
 
-  **Du**: Also kann ich mit `intro` anfangen, wie ich das bei einem `∀`?"
+  **Du**: Also kann ich mit `intro` anfangen, wie ich das bei einem `∀` funktioniert?
+
+  **Robo**: Das ist korrekt."
   intro h hA
+  Hint (hidden := true) "**Robo**: Das dürfte eine Trivialität sein."
   trivial --apply mem_univ -- or `trivial`.
 
-NewTactic intro trivial apply
-NewDefinition subset
--- blocked: tauto simp
+DisabledTactic tauto simp
+NewDefinition Symbol.Subset
+
+Conclusion "Damit drehen sich die beiden Mädchen um und folgen dem Jungen."
 
 end MySet

server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean

@@ -14,10 +14,14 @@ Title "Teilmengen"
 
 Introduction
 "
+Etwas weiter kommt ihr an einem kleinen Gemüsestand vorbei. Da ihr nicht so
+richtig einen Plan habt, fragt ihr den Verkäufer.
+
+**Verkäufer**: Hier ist was ganz wichtiges, was ihr noch oft brauchen werdet:
 Ein zentrales Lemma ist `Subset.antisymm_iff` welches folgendes sagt:
 
 ```
-A = B ↔ A ⊆ B ∧ B ⊆ A
+lemma antisymm_iff {α : Type} {A B : Set α} : A = B ↔ A ⊆ B ∧ B ⊆ A
 ```
 
 Fast immer wenn man Gleichheiten von Mengen zeigen muss, will man diese in zwei Ungleichungen
@@ -26,7 +30,7 @@ aufteilen.
 
 namespace MySet
 
-open Set
+open Set Subset
 
 -- Copied some lemmas from `Matlib.Data.Set.Basic` in order to not import the entire file.
 theorem tmp {α : Type _} {s t : Set α} : s = t → s ⊆ t :=
@@ -39,10 +43,13 @@ theorem Subset.antisymm_iff {α : Type _} {a b : Set α} : a = b ↔ a ⊆ b ∧
 theorem empty_subset {α : Type _} (s : Set α) : ∅ ⊆ s :=
   fun.
 
-Statement subset_empty_iff
-"Die einzige Teilmenge der leeren Menge ist die leere Menge."
-    {A : Type _} (s : Set A) :
+Statement subset_empty_iff {A : Type _} (s : Set A) :
     s ⊆ ∅ ↔ s = ∅ := by
+  Hint "**Du**: Ja, die einzige Teilmenge der leeren Menge ist die leere Menge.
+  Das ist doch eine Tautologie?
+
+  **Robo**: Naja nicht ganz, "
+
   constructor
   intro h
   rw [Subset.antisymm_iff]