levels

server/testgame/TestGame/LemmaDocs.lean

@@ -75,28 +75,41 @@ Die Definition kann man mit `unfold odd at *` einsetzen.
 
 DefinitionDoc Injective
 "
-`Injective f` ist als
+`Injective f` ist definiert als
 
 ```
-∀ {a b : U}, a < b → f a < f b
+∀ a b, f a = f b → a = b
 ```
 definiert.
 "
 
 DefinitionDoc Surjective
 "
+`Surjective f` ist definiert als
+
+```
+∀ a, (∃ b, f a = b)
+```
 "
 
 DefinitionDoc Bijective
 "
 "
 
+DefinitionDoc LeftInverse
+"
+"
+
+DefinitionDoc RightInverse
+"
+"
+
 DefinitionDoc StrictMono
 "
-`StrictMono`
+`StrictMono f` ist definiert als
 
 ```
-∀ {a b : U}, f a  f b → a = b
+∀ a b, a < b → f a < f b
 ```
 
 "
@@ -178,3 +191,13 @@ LemmaDoc StrictMono.add as StrictMono.add in "Function"
 
 LemmaDoc Odd.strictMono_pow as Odd.strictMono_pow in "Function"
 ""
+
+LemmaDoc Exists.choose as Exists.choose in "Function"
+""
+
+LemmaDoc Exists.choose_spec as Exists.choose_spec in "Function"
+""
+LemmaDoc congrArg as congrArg in "Function"
+""
+LemmaDoc congrFun as congrFun in "Function"
+""

server/testgame/TestGame/Levels/Function/L09_Surjective.lean

@@ -9,11 +9,29 @@ Title "Surjektive"
 
 Introduction
 "
+Endlich kommt ihr in einen große, beleuchteten zentralen Raum.
+Alle Wände sind voll mit Büchern und
+in der Mitte sitzt an einem einsamen
+Tisch ein Gelehrter, der tatsächlich das gesuchte Buch zeigen kann.
+
+Bevor er dieses aushändigt, will er aber folgendes wissen:
 "
 
-Statement
-""
-: (fun (n : ℤ) ↦ n + 1).Surjective := by
+open Function
+
+Statement "" : Surjective (fun (n : ℤ) ↦ n + 1) := by
   intro y
   use y-1
   simp
+
+NewDefinition Surjective
+
+Hint : Surjective (fun (n : ℤ) ↦ n + 1) =>
+"**Robo**: Die Definition von `Surjective f` ist `∀ y, (∃ x, f x = y)`.
+
+**Du**: Dann kann ich das auch einfach wie Quantifier behandeln?
+
+**Robo**: Schieß drauf los!"
+
+Conclusion
+"Der Gelehrte händigt euch schmunzelnd das Buch aus."

server/testgame/TestGame/Levels/Function/L10_Bijective.lean

@@ -9,15 +9,30 @@ Title ""
 
 Introduction
 "
+**Du**: Ehm, und wie kommen wir da wieder raus?
+
+**Gelehrter**: Gerne zeige ich euch den Weg, nachdem ihr mir auch noch folgendes erklärt:
 "
 
-Statement
-""
-  : (fun (n : ℤ) ↦ n + 1).Bijective := by
+open Function
+
+Statement "" : Bijective (fun (n : ℤ) ↦ n + 1) := by
+  unfold Bijective
   constructor
-  intro a b hab
-  simp at hab
-  assumption
+  intro a b
+  simp
   intro y
   use y-1
   simp
+
+Hint : Bijective (fun (n : ℤ) ↦ n + 1) =>
+"**Robo** *(flüsternd)**: `Bijectve f` ist als `Injective f ∧ Surjective f` definiert.
+
+**Du**: Dann ist das ja ganz simpel!
+"
+
+Conclusion
+"Zufrieden drückt euch der Gelehrte eine neue Fackel in die Hand und
+zeigt euch den Weg nach draussen."
+
+NewDefinition Bijective

server/testgame/TestGame/Levels/Function/L11_Inverse.lean

@@ -0,0 +1,60 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 10
+
+Title "Inverse"
+
+Introduction
+"
+Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
+eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
+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.
+"
+
+open Function
+
+Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
+    Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
+  constructor
+  intro h
+  use fun x => (h.2 x).choose
+  constructor
+  · intro x
+    simp
+    apply h.1
+    apply Exists.choose_spec (h.2 (f x))
+  · intro x
+    simp
+    apply Exists.choose_spec (h.2 x)
+  intro ⟨g, h₁, h₂⟩
+  constructor
+  · intro a b hab
+    have h : g (f a) = g (f b)
+    · apply congrArg
+      assumption
+    rw [h₁, h₁] at h
+    assumption
+  · intro x
+    use g x
+    rw [h₂]
+
+NewDefinition LeftInverse RightInverse
+NewLemma Exists.choose Exists.choose_spec congrArg congrFun
+DisabledLemma Function.bijective_iff_has_inverse
+
+Hint {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f =>
+"**Du**: Nah da sagt mir so manches nichts, aber ich kann ja mal mit dem `↔` anfangen, das kenn
+ich ja schon."
+
+Conclusion
+"Endlich entkommt ihr dem Tempel.
+
+**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
+
+**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"

server/testgame/TestGame/Levels/Implication.lean

@@ -21,7 +21,7 @@ Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die
 beide bewohnt zu sein scheinen.
 
 **Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen,
-aber niemand von den Einwohnern...
+aber niemand von den Einwohnern wusste was davon...
 
 **Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr
 erzählen…

server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean

@@ -13,7 +13,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 er kritzelt etwas auf ein Stück Papier:  oben ein paar Annahmen, unten eine Schlussfolgerung.
+Und sie kritzelt etwas auf ein Stück Papier:  oben ein paar Annahmen, unten eine Schlussfolgerung.
 Dazwischen sollst Du offenbar einen Beweis eintragen.
 Du siehst Robo hilflos an.
 "