add 1st level to Cantor

.i18n/de/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Tue May 14 11:22:48 2024\n"
+"POT-Creation-Date: Tue May 14 13:40:09 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: de\n"
@@ -5003,52 +5003,68 @@ msgid "Ihr landet auf einem warmen Planeten, und tretet auf eine weite Graslands
 " vereinzelten Bäumen hindurch. Ihr beratet kurz und beschließt, den Spuren zu folgen."
 msgstr ""
 
-#: Game.Levels.Cantor.L01_CantorPowerset
+#: Game.Levels.Cantor.L00_CantorPowerset
 msgid "Cantor's Diagonalargument"
 msgstr ""
 
-#: Game.Levels.Cantor.L01_CantorPowerset
+#: Game.Levels.Cantor.L00_CantorPowerset
 msgid "**Cantor**: Wusstet ihr dass es keine surjektiven Funktionen `f : A → Set A` gibt? Faszinierend\n"
-"oder? Wie das geht? Nehmt doch einmal die Menge `C := { a | a ∉ f a }`. Wenn `f` surjektiv wäre,\n"
-"welches `a : A` würde diese Menge als Bildpunkt haben? Hier, ich gebe euch einfach `C` auch\n"
-"schon mit!\n"
+"oder?\n"
 "\n"
-"[Tipp: `unfold_let` ist wie `unfold` und wird zukünftig in Lean zusammengeführt.\n"
-"Brauche `unfold_let C` wenn eine lokale Definition in deinen Annahmen ist. Alternativ\n"
-"funktionert auch `simp [C]`.]"
+"**Cantor**: Wie das geht? Hier, ist eine kleine Hilfe:"
+msgstr ""
+
+#: Game.Levels.Cantor.L00_CantorPowerset
+msgid ""
+msgstr ""
+
+#: Game.Levels.Cantor.L00_CantorPowerset
+msgid "**Robo**: Denk daran, dass `mem_setOf` aus `Set` irgendwann hilfreich sein wird."
+msgstr ""
+
+#: Game.Levels.Cantor.L00_CantorPowerset
+msgid "**Du**: Ich denke eine Fallunterscheidung auf `«{a}» ∈ «{f}» «{a}»` könnte sinnvoll sein."
+msgstr ""
+
+#: Game.Levels.Cantor.L00_CantorPowerset
+msgid "**Robo**: Das wäre `by_cases h₁ : «{a}» ∈ «{f}» «{a}»`."
+msgstr ""
+
+#: Game.Levels.Cantor.L00_CantorPowerset
+msgid "**Robo**: Mach mal mit `suffices : «{a}» ∉ «{f}» «{a}»` weiter!"
 msgstr ""
 
 #: Game.Levels.Cantor.L01_CantorPowerset
-msgid "**Du**: Uff. Aber ehrlich habe ich die das \"Diagonale\" daran noch nicht\n"
-"ganz gesehen.\n"
-"\n"
-"\n"
-"**Cantor**: Natürlich, das kann ich euch zeigen, aber da muss ich etwas ausholen…"
+msgid "Cantor's Diagonalargument"
 msgstr ""
 
 #: Game.Levels.Cantor.L01_CantorPowerset
-msgid "**Du**: Also ein Widerspruchsbeweis?"
+msgid "**Cantor**: Also und jetzt die eigentliche Aussage!"
 msgstr ""
 
 #: Game.Levels.Cantor.L01_CantorPowerset
-msgid "**Du**: Und jetzt existiert durch Surjektivität ein Urbild von `«{C}»`.\n"
+msgid "**Du**: Uff. Aber ehrlich habe ich die das \"Diagonale\" daran noch nicht\n"
+"ganz gesehen.\n"
+"\n"
 "\n"
-"**Cantor**: Genau! Und dann überlegt euch, ob `b ∈ f b` ist oder nicht für\n"
-"dieses Urbild `b`!"
+"**Cantor**: Natürlich, das kann ich euch zeigen, aber da muss ich etwas ausholen…"
 msgstr ""
 
 #: Game.Levels.Cantor.L01_CantorPowerset
-msgid "**Robo**: Das machen wir glaubs am besten mit `by_cases`."
+msgid "**Du**: Also ein Widerspruchsbeweis?"
 msgstr ""
 
 #: Game.Levels.Cantor.L01_CantorPowerset
-msgid "**Du**: Jetzt will ich ja auch noch `«{b}» ∉ «{f}» «{b}»` zeigen für den Widerspruch.\n"
-"\n"
-"**Robo**: Dann sag doch `suffices hn : «{b}» ∉ «{f}» «{b}»`, erinnerst du dich?"
+msgid "**Robo**: als Erinnerung: Wenn du so etwas wie `?f` siehst, bedeutet das, dass\n"
+"noch nicht spezifiziert wurde welche Funktion benützt wird. Du hättest besser\n"
+"`apply cantor_helper f` geschrieben. Aber du kannst auch einfach mal weitermachen, als ob `?f`\n"
+"schon `«{f}»` wäre, und vermutlich wird Lean das irgendwann automatisch einfüllen."
 msgstr ""
 
 #: Game.Levels.Cantor.L01_CantorPowerset
-msgid "**Robo**: Und noch den Fall wenn `«{b}» ∉ «{f}» «{b}»`"
+msgid "**Cantor**: Wendet doch gleich das Resultat von vorhin an!\n"
+"\n"
+"**Robo**: Ich hab das als `cantor_helper f` gespeichert."
 msgstr ""
 
 #: Game.Levels.Cantor.L02_IsFixedPt_abs

Game/Levels/Cantor.lean

@@ -1,12 +1,14 @@
+import Game.Levels.Cantor.L00_CantorPowerset
 import Game.Levels.Cantor.L01_CantorPowerset
 import Game.Levels.Cantor.L02_IsFixedPt_abs
 import Game.Levels.Cantor.L03_fixedPoints_neg
 import Game.Levels.Cantor.L04_IsFixedPt_not
 import Game.Levels.Cantor.L05_IsFixedPt_odd
 import Game.Levels.Cantor.L06_idempotent
-import Game.Levels.Cantor.L07_CantorDiag_IsFixedPt
 import Game.Levels.Cantor.L07_CantorDiag
+import Game.Levels.Cantor.L07_CantorDiag_IsFixedPt
 import Game.Levels.Cantor.L08_CantorPowerset
+-- import Game.Levels.Cantor.L09_SequenceUncountable
 
 World "Cantor"
 Title "Cantor"

Game/Levels/Cantor/L00_CantorPowerset.lean

@@ -0,0 +1,45 @@
+import Game.Metadata
+
+World "Cantor"
+Level 1
+
+Title "Cantor's Diagonalargument"
+
+Introduction
+"
+**Cantor**: Wusstet ihr dass es keine surjektiven Funktionen `f : A → Set A` gibt? Faszinierend
+oder?
+
+**Cantor**: Wie das geht? Hier, ist eine kleine Hilfe:
+"
+
+Conclusion ""
+
+open Set Function
+
+-- the following implies `cantor_power` but not vice versa.
+-- maybe add this before L01_CantorPowerSet
+Statement cantor_helper (f : A → Set A) : ¬ ∃ (a : A), f a = { x | x ∉ f x } := by
+  Hint "**Robo**: Denk daran, dass `mem_setOf` aus `Set` irgendwann hilfreich sein wird."
+  Branch
+    push_neg
+    intro _a
+    by_contra _ha
+
+  by_contra h
+  rcases h with ⟨a, ha⟩
+  Hint (strict := true) "**Du**: Ich denke eine Fallunterscheidung auf `{a} ∈ {f} {a}` könnte sinnvoll sein."
+  Hint (hidden := true) (strict := true) "**Robo**: Das wäre `by_cases h₁ : {a} ∈ {f} {a}`."
+  by_cases h₁ : a ∈ f a
+  · Hint "**Robo**: Mach mal mit `suffices : {a} ∉ {f} {a}` weiter!"
+    suffices : a ∉ f a
+    · contradiction
+    rw [ha] at h₁
+    rw [mem_setOf] at h₁
+    assumption
+  · apply h₁
+    rw [ha]
+    rw [mem_setOf]
+    assumption
+
+TheoremTab "Set"

Game/Levels/Cantor/L01_CantorPowerset.lean

@@ -1,20 +1,14 @@
 import Game.Metadata
+import Game.Levels.Cantor.L00_CantorPowerset
 
 World "Cantor"
-Level 1
+Level 2
 
 Title "Cantor's Diagonalargument"
 
 Introduction
 "
-**Cantor**: Wusstet ihr dass es keine surjektiven Funktionen `f : A → Set A` gibt? Faszinierend
-oder? Wie das geht? Nehmt doch einmal die Menge `C := { a | a ∉ f a }`. Wenn `f` surjektiv wäre,
-welches `a : A` würde diese Menge als Bildpunkt haben? Hier, ich gebe euch einfach `C` auch
-schon mit!
-
-[Tipp: `unfold_let` ist wie `unfold` und wird zukünftig in Lean zusammengeführt.
-Brauche `unfold_let C` wenn eine lokale Definition in deinen Annahmen ist. Alternativ
-funktionert auch `simp [C]`.]
+**Cantor**: Also und jetzt die eigentliche Aussage!
 "
 
 Conclusion "**Du**: Uff. Aber ehrlich habe ich die das \"Diagonale\" daran noch nicht
@@ -27,36 +21,49 @@ ganz gesehen.
 open Set Function
 
 Statement {A : Type*} (f : A → Set A) :
-    let C := { a | a ∉ f a }
     ¬ Surjective f := by
   Hint (hidden := true) "**Du**: Also ein Widerspruchsbeweis?"
   by_contra hf
-  Hint (strict := true)
-  "**Du**: Und jetzt existiert durch Surjektivität ein Urbild von `{C}`.
-
-  **Cantor**: Genau! Und dann überlegt euch, ob `b ∈ f b` ist oder nicht für
-  dieses Urbild `b`!"
-  have hsurj := hf C
-  rcases hsurj with ⟨b, hb⟩
-  Hint (hidden := true) "**Robo**: Das machen wir glaubs am besten mit `by_cases`."
-  by_cases b ∈ f b
-  · Branch
-      clear hf C hb
-      Hint "**Du**: Jetzt will ich ja auch noch `{b} ∉ {f} {b}` zeigen für den Widerspruch.
-
-      **Robo**: Dann sag doch `suffices hn : {b} ∉ {f} {b}`, erinnerst du dich?"
-    suffices hn : b ∉ f b
-    · contradiction
-    rw [hb]
-    rw [mem_setOf]
-    simp
-    assumption
-  · Hint "**Robo**: Und noch den Fall wenn `{b} ∉ {f} {b}`"
-    suffices hn : b ∈ f b
-    · contradiction
-    rw [hb]
-    rw [mem_setOf]
-    assumption
-
-NewTactic unfold_let -- TODO: remove
+  -- Branch
+  --   Hint (strict := true)
+  --   "**Du**: Und jetzt existiert durch Surjektivität ein Urbild von `TODO`.
+
+  --   **Cantor**: Genau! Und dann überlegt euch, ob `b ∈ f b` ist oder nicht für
+  --   dieses Urbild `b`!"
+  --   have hsurj := hf { a | a ∉ f a }
+  --   rcases hsurj with ⟨b, hb⟩
+  --   Hint (hidden := true) "**Robo**: Das machen wir glaubs am besten mit `by_cases`."
+  --   by_cases b ∈ f b
+  --   · Branch
+  --       clear hf hb
+  --       Hint "**Du**: Jetzt will ich ja auch noch `{b} ∉ {f} {b}` zeigen für den Widerspruch.
+
+  --       **Robo**: Dann sag doch `suffices hn : {b} ∉ {f} {b}`, erinnerst du dich?"
+  --     suffices hn : b ∉ f b
+  --     · contradiction
+  --     rw [hb]
+  --     rw [mem_setOf]
+  --     simp
+  --     assumption
+  --   · Hint "**Robo**: Und noch den Fall wenn `{b} ∉ {f} {b}`"
+  --     suffices hn : b ∈ f b
+  --     · contradiction
+  --     rw [hb]
+  --     rw [mem_setOf]
+  --     assumption
+  Branch
+    apply cantor_helper
+    -- BUG: This does not trigger
+    Hint "**Robo**: als Erinnerung: Wenn du so etwas wie `?f` siehst, bedeutet das, dass
+    noch nicht spezifiziert wurde welche Funktion benützt wird. Du hättest besser
+    `apply cantor_helper f` geschrieben. Aber du kannst auch einfach mal weitermachen, als ob `?f`
+    schon `{f}` wäre, und vermutlich wird Lean das irgendwann automatisch einfüllen."
+  Hint "**Cantor**: Wendet doch gleich das Resultat von vorhin an!
+
+  **Robo**: Ich hab das als `cantor_helper f` gespeichert."
+  apply cantor_helper f
+  rcases hf { x | x ∉ f x } with ⟨w, hw⟩
+  use w
+
+NewHiddenTactic unfold_let -- TODO: remove
 TheoremTab "Function"

Game/Levels/Cantor/L02_IsFixedPt_abs.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L01_CantorPowerset
 
 World "Cantor"
-Level 2
+Level 3
 
 Title "Fixpunkte"
 

Game/Levels/Cantor/L03_fixedPoints_neg.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L02_IsFixedPt_abs
 
 World "Cantor"
-Level 3
+Level 4
 
 Title "Fixpunkt"
 

Game/Levels/Cantor/L04_IsFixedPt_not.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L03_fixedPoints_neg
 
 World "Cantor"
-Level 4
+Level 5
 
 Title "Keine Fixpunkte"
 

Game/Levels/Cantor/L05_IsFixedPt_odd.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L04_IsFixedPt_not
 
 World "Cantor"
-Level 5
+Level 6
 
 Title "Fixpunkte"
 

Game/Levels/Cantor/L06_idempotent.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L05_IsFixedPt_odd
 
 World "Cantor"
-Level 6
+Level 7
 
 Title "Idempotent"
 

Game/Levels/Cantor/L07_CantorDiag.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L07_CantorDiag_IsFixedPt
 
 World "Cantor"
-Level 8
+Level 9
 
 Title "Diagonalargument"
 

Game/Levels/Cantor/L07_CantorDiag_IsFixedPt.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L06_idempotent
 
 World "Cantor"
-Level 7
+Level 8
 
 Title "Diagonalargument"
 

Game/Levels/Cantor/L08_CantorPowerset.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L07_CantorDiag
 
 World "Cantor"
-Level 9
+Level 10
 
 Title "Diagonalargument"
 
@@ -44,26 +44,4 @@ Statement cantor_power : ∀ (f : A → Set A), ¬ Surjective f := by
   apply not_isFixedPt_not -- Lvl 4
   apply h
 
-
--- the following implies `cantor_power` but not vice versa.
--- maybe add this before L01_CantorPowerSet
-example (f : A → Set A) : ¬ ∃ (a : A), f a = { x | x ∉ f x } := by
-  push_neg
-  intro a
-  intro h
-  by_cases a ∈ f a
-  · suffices : a ∉ f a
-    · contradiction
-    rw [h] at h_1
-    rw [mem_setOf] at h_1
-    assumption
-  sorry
-
-#check Set.preimage
-
-example (f : A → Set A) : f ⁻¹' { { a | a ∉ f a } } = ∅ := by
- sorry
-
-
-
 TheoremTab "Function"

Game/Levels/Cantor/L09_SequenceUncountable.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.Levels.Cantor.L08_CantorPowerset
 
 World "Cantor"
-Level 10
+Level 11
 
 Title "Cantor"