storytime

2023-03-15 18:30:35 +01:00
parent b0d9816ce6
commit 32a17ed9e8
33 changed files with 572 additions and 590 deletions
@@ -11,7 +11,7 @@ import TestGame.Levels.Sum
 import TestGame.Levels.Numbers
 import TestGame.Levels.Inequality

-import TestGame.Levels.LeanStuff
+import TestGame.Levels.Lean
 import TestGame.Levels.SetTheory
 import TestGame.Levels.Function
 import TestGame.Levels.SetFunction
@@ -23,23 +23,22 @@ Game "TestGame"
 Title "Lean 4 game"
 Introduction
 "
-TODO
 "

 Conclusion
 "Fertig!"


-Path Proposition → Implication → Predicate
-Path Predicate → Contradiction → Sum → LeanStuff
-Path LeanStuff → SetTheory → SetTheory2 → SetFunction
+Path Proposition → Implication → Predicate → Predicate → Contradiction → Sum → Lean
+Path Predicate → Inequality → Sum
+-- Path Predicate → Prime -- → Induction
+-- Path Sum → Inequality -- → Induction
+
+Path Lean → SetTheory → SetTheory2 → SetFunction
+Path Lean → Function → SetFunction

-Path Predicate → Prime -- → Induction
-Path Sum → Inequality -- → Induction
-Path Inequality → Function

 Path SetTheory2 → Numbers
 Path Module → Basis → Module2
-Path LeanStuff → Function → SetFunction

 MakeGame
@@ -33,6 +33,6 @@ Hint : Bijective (fun (n : ℤ) ↦ n + 1) =>

 Conclusion
 "Zufrieden drückt euch der Gelehrte eine neue Fackel in die Hand und
-zeigt euch den Weg nach draussen."
+zeigt euch den Weg nach draußen."

 NewDefinition Bijective
@@ -28,7 +28,7 @@ aber niemand von den Einwohnern wusste was davon...
 erzählen…

 Und damit leitet Robo den Landeanflug ein. Implis scheint ein riesiger Tagbau zu sein auf
-dem nach allem möglichen gegraben wird. Überall seht ihr Förderbänder kreuz und queer.
+dem nach allem möglichen gegraben wird. Überall seht ihr Förderbänder kreuz und quer.

 Das Operationsteam begrüsst euch freundlich und lädt zum Essen im Kommandoturm.
 "
@@ -18,7 +18,8 @@ Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
  Hint "**Du**: Einen Moment, das ist eine Implikation (`\\to`),
  also `A` impliziert `A und B`, soweit so gut, also eine Tautologie.

-  **Robo**: Die scheinen hier `tauto` auch nicht zu verstehen.
+  **Robo**: Du hast recht, eigentlich könnte man `tauto` sagen,
+  aber das scheinen die hier tauto nicht zu verstehen.
  Implikationen kannst du aber mit `intro h` angehen."
  intro hA
  Hint "**Du**: Jetzt habe ich also angenommen, dass `A` wahr ist und muss `A ∧ B` zeigen,
@@ -8,7 +8,7 @@ Title "Implikation"

 Introduction
 "
-Selbstsicher folgt ihr den Anweisungen und geht nach draussen zum
+Selbstsicher folgt ihr den Anweisungen und geht nach draußen zum
 defekten Kontrollelement. Dieses zeigt ein kompliziertes Diagram:
 $$
 \\begin{CD}
@@ -37,7 +37,7 @@ hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`.
 **Operationsleiter**: \"Modulo Ponens\" ist ein lokaler Begriff hier,
 aber das ist doch nicht wichtig.

-**Robo**: Und das \"r\" in `mpr` stünde für \"reverse\" weils die Rückrichtung ist.
+**Robo**: Und das \"r\" in `mpr` stünde für \"reverse\" weil's die Rückrichtung ist.
 "

 NewTactic constructor
@@ -3,6 +3,8 @@ import TestGame.Metadata
 import Init.Data.ToString
 -- #check List UInt8

+set_option tactic.hygienic false
+
 Game "TestGame"
 World "Implication"
 Level 7
@@ -6,3 +6,11 @@ import TestGame.Levels.Inequality.L04_Linarith
 Game "TestGame"
 World "Inequality"
 Title "Ungleichung"
+
+Introduction "
+Später erinnerst du dich gar nicht mehr wo und wann du diese Unterhaltung hattest, geschweige
+denn mit wem. Vielleicht war es ein Traum, oder eine Erscheinung. Vielleicht war es
+auch nur eines Abends über einer Runde Getränke.
+
+Aber auf jedenfall hast du irgendwo gelernt, was du nun weisst.
+"
@@ -8,17 +8,26 @@ Title "Kleinergleich"

 Introduction
 "
-Ungleichheiten werden in Lean generell immer als Kleinergleich `≤` (`\\le`) oder `<`
-geschrieben.
+*(Gesrpäch)*

-Die Symbole `≥` und `>` gibt es zwar auch, sind aber nur Notation für die gleiche
-Aussage mit `≤` und `<`.
+**Robo** (*lallend*, oder war's fröhlich proklamierend?):
+…und deshalb sind `≥` und `>` eigentlich nur Notationen für `≤`,
+welches man übrigens `\\le` schreibt, was für Less-Equal (also Kleinergleich) steht…

-Zudem sind `<` und `≤` auf `ℕ` so definiert, dass `0 < n` und `1 ≤ n` per Definition
-äquivalent sind. Die folgende Aussage ist also mit `rfl` beweisbar.
+**Du**: Wir haben's verstanden, man benützt also Standartmässig lieber `≤` und `<`,
+aber damit weiß ich eh nichts anzufangen.
+
+**dritte Person**: Komm schon, das kannst du ja sicher:
 "

 Statement
-"$0 < n$ und $1 ≤ n$ sind äquivalente Aussagen."
-    (n m : ℕ) : m < n ↔ m.succ ≤ n := by
+  (n m : ℕ) : m < n ↔ m.succ ≤ n := by
+  Hint "**Robo**: Du Narr! Das ist doch eine Kuriosität, dass `m < n` auf `ℕ` per Definition
+  als `m + 1 ≤ n` definiert ist!
+
+  **dritte Person**: Du verdirbst den Witz! Ich wollte ihn doch nur testen."
  rfl
+
+OnlyTactic rfl
+
+Conclusion "**Du**: Ha. ha… Na aber jetzt mal ehrlich, wie funktioniert das eigentlich?"
@@ -12,67 +12,42 @@ Title "Kleinergleich"

 Introduction
 "
-Es gibt zwei intrinsische Möglichkeiten, zu sagen dass `(n : ℕ)` nicht Null ist:
-`n ≠ 0` oder `0 < n`.
-
-Das folgende Lemma kannst du immer brauchen um zwischen den beiden zu wechseln.
-
-(*Note:* `0 < n` wird in Lemma-Namen oft mit `_pos` beschrieben anstatt `zero_lt`, siehe z.B.
-`Nat.succ_pos`.)
+*weitere Person*: …ich sag dir, eine positive Zahl kann man sowohl mit `0 < n`
+als auch `n ≠ 0` darstellen.

+*Robo*: Und da gibts leider keinen Standard dazu.

+**weitere Person*: Ja und, da kann man ja einfach mit `Nat.pos_iff_ne_zero`
+wechseln. Wart mal, wieso galt das nochmals…
 "

-Statement Nat.pos_iff_ne_zero
-"Benutze Induktion um zu zeigen, dass $0 < n$ und $n \\ne 0$ äquivalent sind."
-    (n : ℕ) : 0 < n ↔ n ≠ 0 := by
-  induction n
+Statement Nat.pos_iff_ne_zero (n : ℕ) : 0 < n ↔ n ≠ 0 := by
+  Hint "**Robo** (*flüsternd*): Wenn du ein bisschen schwere Maschinerie auffahren willst,
+  um in zu beeindrucken, hab ich was. Mach doch eine Fallunterscheidung ob `n` Null ist
+  oder nicht!
+
+  **Du** (*flüsternd*): Und wie geht das?
+
+  **Robo** (*laut und selbstsicher*): Wir fangen mit `rcases n` an!"
+  rcases n
+  Hint "**Du**: Hmm, das muss man doch vereinfachen können.
+
+  **Robo** (*flüsternd*): Zweiter pompöser Auftritt: sag einfach `simp` und lass das alles
+  automatisch geschehen."
  simp
+  Hint "**Du**: Und hier fang ich wohl am besten an wie ich das schon kenne."
  constructor
  intro
  simp
  intro
+  Hint "**Robo**: Warte! Den Rest geb ich dir als Lemma: `Nat.suc_pos`."
  apply Nat.succ_pos

 NewTactic simp
 NewLemma Nat.succ_pos
+DisabledLemma Nat.pos_iff_ne_zero

-Hint : 0 < Nat.zero ↔ Nat.zero ≠ 0 =>
-"Den Induktionsanfang kannst du oft mit `simp` lösen."
+Conclusion "**Du**: Oh `simp` ist ja echt nicht schlecht…

-Hint (n : ℕ) (h : 0 < n ↔ n ≠ 0) : 0 < Nat.succ n ↔ Nat.succ n ≠ 0 =>
-"Jetzt der Induktionsschritt. Fang mal mit `constructor` an."
-
-HiddenHint (n : ℕ) : 0 < Nat.succ n → Nat.succ n ≠ 0 =>
-"Auch das kann `simp`."
-
-Hint (n : ℕ) : n.succ ≠ 0 =>
-"Auch das kann `simp`."
-
-Hint (n : ℕ) : 0 < Nat.succ n =>
-"Hier kannst du das Lemma `Nat.succ_pos` mit `apply` anwenden."
-
-
-
-/- Second, less ideal path -/
-
-Hint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
-"An dieser Stelle fürst du am besten einen Beweis durch Widerspruch."
-
-HiddenHint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
-"Das macht man mit `by_contra`."
-
-Hint (n : ℕ) (h : 0 < n) (g : n = 0) : False =>
-"Brauche `rw [_] at _` um eine Annahme `0 < 0` zu erzeugen."
-
-HiddenHint (h : 0 < 0) : False =>
-"Mit `contradiction` schliesst du den Widerspruchsbeweis."
-
-Hint (n : ℕ) (h : n ≠ 0) : 0 < n =>
-"Diese Richtung beweist du am besten per Induktion."
-
-HiddenHint (n : ℕ) (h : n ≠ 0) : 0 < n =>
-"Starte mit `induction n`."
-
- HiddenHint : 0 < Nat.zero =>
-"Mit `contradiction` kannst du den Induktionsanfang schliessen."
+Die andere Person scheint beeindruckt, hat aber gleichzeitig auch das Bedürfnis, Dich aus
+der Reserve zu locken."
@@ -9,15 +9,18 @@ Title "Linarith"

 Introduction
 "
-Die Taktik `linarith` kann alle Systeme von linearen (Un-)gleichungen über `ℤ`, `ℚ`, etc. lösen.
-Über `ℕ` ist sie etwas schwächer, aber einfache Aussagen kann sie trotzdem beweisen.
+**dritte Person**: Nah wenn wir so spielen:
 "

-Statement
-"Wenn $n \\ge 2$, zeige, dass $n$ nich Null sein kann."
-    (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
+Statement (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
+  Hint "**Du**: `simp` geht hier nicht, was mir ja auch einläuchtet.
+
+  **Robo**: Ist auch keine Vereinfachung, die du machen willst. Stattdessen,
+  `linarith` kann lineare Gleichungen und Ungleichungen lösen. Das ist das Powertool
+  in der hinsicht."
  linarith

 NewTactic linarith
-
 NewLemma Nat.pos_iff_ne_zero
+
+Conclusion "**Du**: Naja so beeindruckend war das jetzt auch noch nicht."
@@ -9,20 +9,21 @@ Title "Linarith"

 Introduction
 "
-Sobald man mit einem Ring arbeitet, der eine lineare Order hat (also z.B. `ℤ` oder `ℚ`),
-ist `linarith` stärker und kann Systeme von Gleichungen und Ungleichungen angehen.
+**Robo**: Die Taktik kann aber noch viel mehr.

-`linarith` kann aber nur mit linearen Ungleichungen umgehen, mit Termen der Form `x ^ 2`
-kann es nicht umgehen.
+**weitere Person**: Hier, probier mal!
+
+$$
+\\begin{aligned}
+  5 * y &\\le 35 - 2 * x \\\\
+  2 * y &\\le x + 3
+\\end{aligned}
+$$
 "

-Statement
-"
-Angenommen man hat für zwei Ganzzahlen $x, y$ folgende Ungleichungen.
-$$
-\\begin{aligned} 5 * y &\\le 35 - 2 * x \\\\ 2 * y &\\le x + 3 \\end{aligned}
-$$
-Zeige, dass $y \\le 5$.
-"
-    (x y : ℤ) (h₂ : 5 * y ≤ 35 - 2 * x) (h₃ : 2 * y ≤ x + 3) : y ≤ 5 := by
+Statement (x y : ℤ) (h₂ : 5 * y ≤ 35 - 2 * x) (h₃ : 2 * y ≤ x + 3) : y ≤ 5 := by
  linarith
+
+Conclusion "**Du**: Boah, das ist schon gar nicht schlecht.
+
+Und damit endet auch Deine Erinnerung und wer weiss was du anschließend gemacht hast…"
@@ -0,0 +1,26 @@
+import TestGame.Levels.Lean.L01_Type
+import TestGame.Levels.Lean.L02_Universe
+import TestGame.Levels.Lean.L03_ImplicitArguments
+import TestGame.Levels.Lean.L04_InstanceArguments
+
+Game "TestGame"
+World "Lean"
+Title "Lean"
+
+Introduction
+"Während ihr weiter durch Täler, über Geröllhalden und zwischen monumentalen Steintürmen
+umherzieht, fragst Du eines Tages Robo.
+
+**Du**: Sag mal, hast du dir je Gedanken dazu gemacht, wie du eigentlich funktionierts?
+
+**Robo**: Was meinst du, wie ich funktioniere? Ich bin halt… ich…
+
+**Du**: Ja schon, aber was woher weisst du denn alles was du weisst?
+
+**Robo**: Das kann ich dir sagen. Früher habe ich viele Datenträger verschlungen,
+und dadurch gelernt.
+
+**Du**: Ob so eine Diskette wohl lecker schmeckt? Egal, ich hab ein paar Fragen zu deinem
+Lean-Modul.
+
+**Robo**: Na dann nur zu!"
@@ -0,0 +1,41 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Lean"
+Level 1
+
+Title "Typen"
+
+Introduction
+"
+**Du**: Also, wieso schreib ich denn sowohl `(n : ℕ)` für eine natürliche Zahl wie
+auch `(h : A ∧ ¬ B)` für eine Aussage?
+
+**Robo**: Alles in Lean sind Objekte von einem *Typen*, man nennt das auch
+\"dependent type theory\". Rechts vom `:` steht immer der Typ der dieses Objekt hat.
+
+**Du**: Verstehe, dann war `ℕ` der Typ der natürlichen Zahlen, `Prop` der Typ
+aller logischen Aussagen, und so weiter. Un wenn `R` einfach irgendein Typ ist, dann…
+
+**Robot: …würdest du das als `(R : Type)` schreiben.
+
+**Du**: Also sind Typen ein bisschen jene Grundlage, die in meinem Studium die
+Mengen eingenommen haben?
+
+**Robo**: Genau. Ein Ring ist dann zum Beispiel als `(R : Type) [Ring R]` definiert,
+also als Typen, auf dem eine Ringstruktur besteht.
+
+**Robo**: Hier ein Beispiel. Die Taktik `ring` funktioniert in jedem Typen, der
+genügend Struktur definiert hat, zum Beispiel in einem kommutativen Ring:
+"
+
+Statement (R : Type) [CommRing R] (a b : R) : a + b = b + a := by
+  ring
+
+Conclusion "**Robo**: `[CommRing R]` nennt man übrigens eine Instanz und die
+eckigen Klammern sagen Lean, dass es automatisch suchen soll, ob es so eine Instanz
+findet, wenn man ein Lemma anwenden will."
@@ -0,0 +1,44 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Lean"
+Level 2
+
+Title "Universen"
+
+Introduction
+"**Du**: Aber wenn alles Typen sind, welcher Typ hat dann `Type`?
+
+**Robo**: `Type 1` und dieser hat Typ `Type 2`, etc.
+
+**Robo**: Die Zahl nennt man *Universum*. Manchmal führt man Universen explizit
+mit `universum u` ein, öfter siehst du `(R : Type _)`, was einfach ein Platzhalter
+für irgend ein Universum ist.
+
+**Du**: Das klingt ein bisschen nach Mengentheoretische Probleme, die man normalerweise
+ignoriert.
+
+**Robo**: Genau! Deshalb schreibt man eigentlich immer einfach `Type _` und ist glücklich.
+Spezifischer muss man erst werden wenn man sowas wie Kategorientheorie anschaut, wo
+man die Universen tatsächlich kontrollieren muss.
+
+**Du**: Oke, hier rein, da raus. Aber hast du mir noch eine Aufgabe?
+"
+
+universe u
+
+Statement
+    (R : Type u) [CommRing R] (a b : R) : a + b = b + a := by
+  Hint "**Robo**: Naja, Aufgaben zu Universen sind nicht so natürlich,
+  aber vorige Aufgabe würde man eigentlich besser so schreiben, da
+  kannst du mindestens das Uniersum beobachten."
+  ring
+
+Conclusion "**Du**: Na dann. Aber gut dass ich's mal gesehen hab."
+
+-- Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
+-- ""
@@ -0,0 +1,71 @@
+import TestGame.Metadata
+
+import Mathlib
+import TestGame.Options.BigOperators
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Lean"
+Level 3
+
+Title "Implizite Argumente"
+
+Introduction
+"
+**Du**: Was mich aber mehr beschäftigt, ist, dass Lemmas manchmal viel mehr Argumente
+haben als ich hinschreiben muss.
+
+**Robo**: Lean kann manche Argumente aus dem Kontext erschliessen. Hast du zum Beispiel
+ein Lemma von vorhin
+
+```
+lemma Fin.sum_univ_castSucc {β : Type _} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
+    ∑ i : Fin (n + 1), f i = ∑ i : Fin n, f (↑Fin.castSucc.toEmbedding i) + f (Fin.last n) := by
+  sorry
+```
+
+dann reicht es ja Lean `f` zu geben und daraus kann es herausfinden, was die anderen
+(`β`, `n`) sein müssen.
+
+**Robo**: Solche *implizite Argumente* markiert man dann mit `{_ : _}` während
+*explizite Arumente* mit `(_ : _)` markiert werden.
+
+**Du**: Dann könnte ich also einfach `Fin.sum_univ_castSucc f` schreiben?
+
+**Robo**: Genau!
+
+**Du**: Und was war dann das `(n := m + 1)` vorhin genau?
+
+**Robo**: Damit kann man im Aussnahmefall die impliziten Argumente doch angeben. Hier haben wir
+gesagt, es soll für das Argument `n` den Term `m + 1` einsetzen. Hier mach das doch noch einmal
+unter weniger Stress:
+"
+
+open BigOperators
+
+Statement (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by
+  Branch
+    rw [Fin.sum_univ_castSucc]
+    Hint "**Robo**: Siehst du, ohne die Hilfe macht es das Falsche. Deshalb muss man hier
+    explizit mit `Fin.sum_univ_castSucc (n := m + 1)` nachhelfen."
+    rw [Fin.sum_univ_castSucc]
+    Hint "**Robo**: Na klar, in dem Beispiel kannst du einfach weiter umschreiben bis es
+    nicht mehr geht, aber das war nicht der Punkt…"
+    rw [Fin.sum_univ_castSucc]
+    Hint "**Robo**: Na klar, in dem Beispiel kannst du einfach weiter umschreiben bis es
+    nicht mehr geht, aber das war nicht der Punkt…"
+    rfl
+  rw [Fin.sum_univ_castSucc (n := m + 1)]
+  rfl
+
+OnlyTactic rw rfl
+
+Conclusion "**Du**: Gibt es auch noch ander Methoden implizite Argumente anzugeben.
+
+**Robo** `@Fin.sum_univ_castSucc` würde *alle* Argumente explizit machen,
+aber das ist unparktischer, weil man dann irgendwie
+`@Fin.sum_univ_castSucc _ _ (m + 1)` schreiben müsste.
+
+**Du**: Ah und ich sehe der `_` ist überall in Lean ein Platzhalter, der automatisch
+gefüllt wird."
@@ -0,0 +1,57 @@
+import TestGame.Metadata
+
+import Mathlib
+import TestGame.Options.BigOperators
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Lean"
+Level 4
+
+Title "Instanz-Argumente"
+
+Introduction
+"**Du**: Also nochmals als Zusammenfassung, dann gibt es 3 Arten von Argumenten,
+explizite mit `()`, implizite mit `{}` und Instanzen mit `[]`?
+
+**Robo**: Korrekt. Instanzen sind damit auch Implizite Argumente. Der Unterschied
+zwischen `{}` und `[]` ist also *wie* Lean diese füllt.
+
+**Du**: Verstehe, bei den ersten sucht es logisch nach einer richtigen Möglichkeit,
+beim zweiten geht's durch alle Instanzen, die es kennt.
+
+
+**Robo**: Funktioniert hier bei mir nicht, aber wenn du ausserhalb eines Beweises
+`#synth Ring ℤ` in ein Dokument schreibt, zeigt dir Lean, ob es eine Instanz finden kann.
+
+**Du**: Ich glaube das macht alles Sinn.
+
+**Robo**: Hier, mach nochmals das Gleiche wie vorhin aber mit @-Syntax um das zu
+verinnerlichen:
+"
+
+open BigOperators
+
+Statement (m : ℕ) :
+      ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by
+  Hint "*Robo*: Schreibe `rw [@Fin.sum_univ_castSucc _ _ (m + 1)]`
+  anstatt `rw [Fin.sum_univ_castSucc (n := m + 1)]`!"
+  rw [@Fin.sum_univ_castSucc _ _ (m + 1)]
+  rfl
+
+OnlyTactic rw rfl
+
+Conclusion "
+**Du**: Danke Robo!
+
+Um zwei weitere Ecken und plötzlich steht ihr wieder vor dem Golem, dem ihr schon begegnet seit.
+Dieser lädt euch zum Abendmahl ein. Ihr erfährt, dass er ganz gerne liest und er zeigt euch
+sein neustes Buch, das er leider nicht lesen kann. Nich tnur ist es der zweite Band einer Serie
+(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
+ersten Band zu suchen.
+"
@@ -1,8 +0,0 @@
-import TestGame.Levels.LeanStuff.L01_Type
-import TestGame.Levels.LeanStuff.L02_Universe
-import TestGame.Levels.LeanStuff.L03_ImplicitArguments
-import TestGame.Levels.LeanStuff.L04_InstanceArguments
-
-Game "TestGame"
-World "LeanStuff"
-Title "Lean"
@@ -1,49 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "LeanStuff"
-Level 1
-
-Title "Typen"
-
-Introduction
-"
-Dieses Kapitel führt ein paar Lean-spezifische Sachen ein, die du wissen solltest.
-
-Mathematisch haben diese Sachen keinen Inhalt, aber es ist wichtig, dass du etwas
-verstehst wie Lean manche Sachen macht.
-
-Als erstes geht es um Typen.
-
-Oft sieht man Argumente von der Form `(U : Type)` was heisst \"sei $U$ ein Typ.\"
-Als Mathematiker kann man sich Typen ein bisschen wie Mengen vorstellen, in dem Sinn
-dass sie die Grundlage der Mathematik bilden: Alles sind Typen.
-
-Zum Beispiel ist `ℕ` der Typ der natürlichen Zahlen, `Prop` der Typ der logischen
-Aussagen, und ein Ring ist ein Typ `(R : Type)` zusammen mit einer Instanz `[Ring R]`,
-die sagt, dass auf diesem Typ eine Ringstruktur besteht.
-
-**Achtung**: Wie du aber gleich sehen wirst sind Typen und Mengen in Lean unterschiedliche
-Sachen.
-
-Hier ein kleines Beispiel zu Typen und Instanzen:
-"
-
-Statement
-""
-    (R : Type) [CommRing R] (a b : R) : a + b = b + a := by
-  ring
-
-Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
-"
-Die Taktik `ring` funktioniert in jedem Typen,
-ist aber stärker, je nach Instanz auf dem Typen.
-
-In Mathlib sind Instanzen `[CommSemiring ℕ]`, [CommRing ℤ]`, `[Field ℚ]`, etc. definiert.
-Die Taktik `ring` muss eine dieser Instanzen finden, die sagen, dass die Addition kommutative ist,
-damit das Lemma `add_comm` angewendet und die Aussage bewiesen werden kann.
-"
@@ -1,51 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "LeanStuff"
-Level 2
-
-Title "Universen"
-
-Introduction
-"
-Ein weitere Syntax, den man in Lean abundzu sieht sind Universen.
-
-Diese sind für Mathematiker erst einmal nicht so wichtig, und es reicht zu wissen,
-dass diese existieren.
-
-Da alle Objekte in Lean einen Typ haben, kann man sich fragen, welchen Typ hat eigentlich `Type`
-selber? Die Anwort darauf ist dass `Type` vom Typ `Type 1` ist und dieses wiederum vom Typ `Type 2`
-usw.
-
-Da Lemmas in Lean gerne so algemein wie möglich formuliert werden, sieht man oft `(R : Type _)`
-anstatt `(R : Type)`, wobei `_` einfach ein Platzhalter für eine Zahl ist.
-
-Alternativ kann man auch explizit Universum-Levels definieren, so sind die folgenden beiden
-Aussdrücke äquivalent:
-
-```
-variable (R : Type _)
-
-universe u
-variable (R : Type u)
-```
-
-In der Praxis kann man immer ohne bedenken `Type _` verwendenen und wenn man auf
-(mengentheoretische)
-Probleme stösst, muss man dan eventuell die Universen spezifizieren.
-
-*Die Normalform ist eigentlich `(R : Type _)` zu schreiben solange man kein Grund hat
-das Universum einzuschränken.*
-"
-
-Statement
-""
-    (R : Type _) [CommRing R] (a b : R) : a + b = b + a := by
-  ring
-
-- Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
-- ""
@@ -1,63 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-import TestGame.Options.BigOperators
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "LeanStuff"
-Level 3
-
-Title "Implizite Argumente"
-
-Introduction
-"
-
-Auch wichtiger Syntax ist der Unterschied zwischen
-impliziten und expliziten Argumenten von Lemmas. **Explizite Argumente**
-schreibt man mit runden Klammern `()`, **impliziete Argumente** mit geschweiften `{}`.
-
-Als implizit werden alle Argumente markiert, die Lean selbständig aus dem Kontext
-erschliessen und einfüllen kann.
-
-Als Beispiel schauen wir uns ein bekanntes Lemma an:
-```
-lemma Fin.sum_univ_castSucc {β : Type _} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
-    ∑ i : Fin (n + 1), f i = ∑ i : Fin n, f (↑Fin.castSucc.toEmbedding i) + f (Fin.last n) := by
-  sorry
-```
-
-Hier ist unter anderem `n` als implizites Argument angegeben, da Lean aus `f` herauslesen kann,
-was `n` sein muss. Falls man trotzdem einmal das implizites Argument angeben muss
-(z.B. um `rw` zu helfen, wenn es mehrere Möglichkeiten gibt),
-kann man dies mit `Fin.sum_univ_castSucc (n := m + 1)` machen.
-"
-
-open BigOperators
-
-Statement
-"Zeige $(\\sum_{i=0}^{m} i) + (m + 1) = \\sum_{i=0}^{m + 1} i$."
-    (m : ℕ) :
-      ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by
-  rw [Fin.sum_univ_castSucc (n := m + 1)]
-  rfl
-
-OnlyTactic rw rfl
-
-NewLemma Fin.sum_univ_castSucc
-
-HiddenHint (m : ℕ) :
-  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
-"Das Lemma `Fin.sum_univ_castSucc` hilft."
-
-Hint (m : ℕ) :
-  ∑ i : Fin m, (Fin.castSucc.toEmbedding i : ℕ) + ↑(Fin.last m) + (m + 1) =
-  ∑ i : Fin (Nat.succ m + 1), ↑i =>
-"Hier hat `rw` die falsche der beiden Summen umgeschrieben. Hilf ihm mit
-`rw [Fin.sum_univ_castSucc (n := m + 1)]`."
-
-Hint (m : ℕ) :
-  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) =
-  ∑ i : Fin (m + 1), ↑i + (m + 1) =>
-"Jetzt sind beide Seiten gleich und das Goal kann mit `rfl` geschlossen werden."
@@ -1,78 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-import TestGame.Options.BigOperators
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "LeanStuff"
-Level 4
-
-Title "Instanz-Argumente"
-
-Introduction
-"
-Bezüglich impliziten Argumente gibt es noch einige weitere Punkte oder Tricks,
-die man wissen sollte.
-
-* Instanz-Argumente wie `[Ring R]` sind auch impilzite Argumente. Der Unterschied ist, dass
-  Lean einen anderen Mechanismus braucht, um diese zu füllen: Es sucht nach einer entsprechenden
-  *Instanz* und, setzt die erste solche Instanz ein.
-  Ausserhalb eines Beweises könnte man auch mit
-  ```
-  #synth Ring ℤ
-  ```
-  testen, ob Lean eine ensprechende Instanz findet. Instanzen werden dafür gebraucht, Typen
-  mit (algebraischer) Stukturen zu versehen.
-* Ein `_` irgendwo im Lean-Code ist immer ein Platzhalter, den Lean versucht aus dem Kontext zu
-  füllen. Das kann praktisch sein, wenn man etwas nicht ausschreiben will, das offensichtlich ist.
-* Mit `@` kann man forcieren, dass alle Argumente explizit sind.
-  Für ein Lemma
-  ```
-  lemma not_or_of_imp {A B : Prop} (h : A → B) :
-      ¬A ∨ B := sorry
-  ```
-  heisst das zum Beispiel dass `not_or_of_imp g` das gleiche ist wie
-  `@not_or_of_imp _ _ g`.
-
-  Und `Fin.sum_univ_castSucc (n := m + 1)` könnte man auch als
-  `@Fin.sum_univ_castSucc _ _ (m + 1)` schreiben.
-"
-
-open BigOperators
-
-Statement
-"Zeige $(\\sum_{i=0}^{m} i) + (m + 1) = \\sum_{i=0}^{m + 1} i$."
-    (m : ℕ) :
-      ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by
-  rw [Fin.sum_univ_castSucc (n := m + 1)]
-  rfl
-
-OnlyTactic rw rfl
-
-NewLemma Fin.sum_univ_castSucc
-
-Hint (m : ℕ) :
-  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
-"
-  Probier nochmals das gleiche, diesmal mit
-```
-rw [@Fin.sum_univ_castSucc _ _ (m + 1)]
-```
-anstatt
-```
-rw [Fin.sum_univ_castSucc (n := m + 1)]
-```
-"
-
-Hint (m : ℕ) :
-  ∑ i : Fin m, (Fin.castSucc.toEmbedding i : ℕ) + ↑(Fin.last m) + (m + 1) =
-  ∑ i : Fin (Nat.succ m + 1), ↑i =>
-"Sackgasse!"
-
-
-Hint (m : ℕ) :
-  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) =
-  ∑ i : Fin (m + 1), ↑i + (m + 1) =>
-"Jetzt sind beide Seiten gleich und das Goal kann mit `rfl` geschlossen werden."
@@ -1,8 +1,11 @@
 import TestGame.Levels.Prime.L01_Dvd
-import TestGame.Levels.Prime.L04_Prime
-import TestGame.Levels.Prime.L05_Prime
-import TestGame.Levels.Prime.L06_ExistsUnique
+-- import TestGame.Levels.Prime.L04_Prime
+-- import TestGame.Levels.Prime.L05_Prime
+-- import TestGame.Levels.Prime.L06_ExistsUnique

 Game "TestGame"
 World "Prime"
 Title "Teilbarkeit"
+
+Introduction "Ihr schlendert durch die Befestigung ohne direktes Ziel. Und sprecht mit
+verschiedenen Einwohnern."
@@ -1,6 +1,7 @@
 import TestGame.Metadata

 import Mathlib.Tactic.Ring
+import Mathlib

 Game "TestGame"
 World "Prime"
@@ -10,43 +11,39 @@ Title "Teilbarkeit"

 Introduction
 "
-Die Aussage \"$m$ teilt $n$.\" wird in Lean als `m | n` (`\\|`) geschrieben.
+Ihr begenet einer Frau, die mit Vorschlaghammer und Schaufel anscheinend an einer Erweiterung
+ihres Hauses baut. Im gespräch erzählt sie euch wie die Dornenwände gezüchtet wurden vor ihrer
+Zeit, und über's Wetter und so.

-**Wichtig:** `∣` (Teilbarkeit) ist ein spezielles Unicode Symbol, das nicht dem
-senkrechten Strich auf der Tastatur (`|`) entspricht. Man erhält es mit `\\|`.
-
-`m ∣ n` bedeutet `∃ c, n = m * c`, das heisst, man kann damit genau gleich umgehen
-wie mit einem `∃`-Quantifier.
+**Handwerkerin**: (*langer Monolog*) …, und dann gestern habe ich zwei Herren überhört,
+wie sie an folgender Aufgabe gesessen sind, könnt ihr mir das erklären?
 "

-Statement dvd_add
-  "Wenn $m$ ein Teiler von $n$ und $k$ ist, dann teilt es die Summe."
-  (n m k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k := by
+-- Die Aussage \"$m$ teilt $n$.\" wird in Lean als `m | n` (`\\|`) geschrieben.
+
+-- **Wichtig:** `∣` (Teilbarkeit) ist ein spezielles Unicode Symbol, das nicht dem
+-- senkrechten Strich auf der Tastatur (`|`) entspricht. Man erhält es mit `\\|`.
+
+-- `m ∣ n` bedeutet `∃ c, n = m * c`, das heisst, man kann damit genau gleich umgehen
+-- wie mit einem `∃`-Quantifier.
+
+Statement dvd_add (n m k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k := by
+  Hint "**Robo**: `n ∣ m` bedeutet \"$n$ teilt $m$\", der senkrechte Strich ist allerdings
+  ein spezieller, den man mit `\\|` schreibt.
+  Definiert ist dieses Symbol als `∃ c, n = m * c`.
+
+  **Du**: Dann kann ich direkt `rcases` und `use` verwenden, wie wenns ein `∃` wäre?
+
+  **Robo**: Genau!"
+  Hint (hidden := true) "**Robo**: Fang doch damit an, mit `rcases _ with ⟨x ,hx⟩`
+  alle Hyptothesen aufzuteilen."
  rcases h with ⟨x, h⟩
  rcases g with ⟨y, g⟩
+  Hint (hidden := true) "**Robo**: Jetzt musst du mit `use _` eine Zahl angeben so dass
+  `{n} + {k} = {m} * _` gilt."
  use x + y
+  Hint (hidden := true) "**Du**: Mit ein bisschen umschreiben kann man sicer `ring` verwenden."
  rw [h, g]
  ring

-HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k =>
-"
-Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
-sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
-"
-
-HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (x : ℕ) (h : n = m * x) (g : m ∣ k) : m ∣ n + k =>
-"
-Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
-sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
-"
-
-HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (y : ℕ)  (h : m ∣ n) (g : k = m * y) : m ∣ n + k =>
-"
-Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
-sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
-"
-
-HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (x : ℕ) (y : ℕ) (h : n = m * x) (g : k = m * y) : m ∣ n + k =>
-"
-Jetzt kannst du mit `use` eine Zahl angeben, so dass $m * X = n + k$.
-"
+DisabledLemma dvd_add
@@ -22,9 +22,9 @@ Statement ""

 **Robo** Ja.  Da kommst Du jetzt selbst drauf, wie das geht, oder?
 "
-  Hint (hidden := true) "Ist doch genau wie eben:
+  Hint (hidden := true) "**Robo**: Ist doch genau wie eben:
 die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
-Also wird `asumption` auch wieder funktionieren."
+Also wird `assumption` auch wieder funktionieren."
  assumption

 Conclusion
@@ -12,12 +12,12 @@ Title "Und"
 Introduction
 "
 Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht.
-Er legt sie uns vor, setzt sich hin, und häkelt.
+Er legt sie uns vor, setzt sich hin und häkelt.
 "
 Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
  Hint
 "
-**Du**:  Also, wir haben zwei Annahmen: `{A}` gilt, und `{B}` gilt. Auch. Und beweisen sollen wir
+**Du**:  Also, wir haben zwei Annahmen: `{A}` gilt, und `{B}` gilt auch. Und beweisen sollen wir
 dass `{A} und {B}` gilt.  Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung.
 Kann ich nicht wieder `trivial` sagen?

@@ -8,3 +8,13 @@ import TestGame.Levels.Sum.L06_Summary
 Game "TestGame"
 World "Sum"
 Title "Endliche Summe"
+
+Introduction "Mit dem Gefühl, dass sich *Evenine* und *Oddeus* in Zukunft wieder
+besser verstehen werden, steigt ihr in eurer Raumschiff und setzt eure Reise fort.
+
+Bald erreicht ihr einen neuen Planet. Die oberfläche scheint steinig zu sein, aber nicht etwa
+geröll oder Chaos. Stattdessen, scheinen unzählige Steinplatten zu bizzaren hohen Türme
+gestapelt und die ganze Landschaft wirkt wie ein grosses Puzzle in dem jede Platte
+feinsäuberlich auf den darunterliegenden Platten aufbaut.
+
+Bald trefft ihr auch die Bewohner dieses Planeten an."
@@ -12,36 +12,55 @@ Title "Simp"

 Introduction
 "
+**Unbekannte**: Willkommen auf *Indu*, unserem Planeten! Bevor ich euch herumzeigen will,
+sagt mir, ob ihr unsere Lebensweise zu verstehen und schätzen wisst:
 In diesem Kapitel lernen wir endliche Summen und mehr Übungen zur Induktion.

-Eine endliche Summe läuft erstmal immer über einen endlichen Index
-`Fin n`, welcher $n$ Elemente
-$\\{0, 1, \\ldots, n-1\\}$ beinhaltet.
-
-Der Syntax für  $\\sum_{i=0}^n a_i$ ist `∑ i : Fin n, _` (\\sum)
-
-Als erstes kann die Taktik `simp` (für \"simplification\") ganz viel Triviales vereinfachen.
-`simp` ist eine der stärksten Taktiken in Lean und verwendet
-ganz viele markierte Lemmas um das Goal zu vereinfachen.
-
-Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
-
-```
-@[simp]
-lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
-  sorry
-```
-
-Die Taktik `simp` benützt alle Lemmas, die mit `@[simp]` markiert sind.
-
-(Tipp: `simp?` zeigt an, welche Lemmas `simp` benutzen würde.)
 "

+-- Eine endliche Summe läuft erstmal immer über einen endlichen Index
+-- `Fin n`, welcher $n$ Elemente
+-- $\\{0, 1, \\ldots, n-1\\}$ beinhaltet.
+
+-- Der Syntax für  $\\sum_{i=0}^n a_i$ ist `∑ i : Fin n, _` (\\sum)
+
+-- Als erstes kann die Taktik `simp` (für \"simplification\") ganz viel Triviales vereinfachen.
+-- `simp` ist eine der stärksten Taktiken in Lean und verwendet
+-- ganz viele markierte Lemmas um das Goal zu vereinfachen.
+
+-- Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
+
+-- ```
+-- @[simp]
+-- lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
+--   sorry
+-- ```
+
+-- Die Taktik `simp` benützt alle Lemmas, die mit `@[simp]` markiert sind.
+
+-- (Tipp: `simp?` zeigt an, welche Lemmas `simp` benutzen würde.)
+
 open BigOperators

-Statement
-"Zeige $\\sum_{i = 0} ^ {n-1} (0 + 0) = 0$."
-    (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
+Statement (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
+  Hint "BUG"
+
+  -- TODO (Bug): Invalid escape sequence:
+  -- "**Du**: Oh das ist ganz schön viel neues… Mal sehen, das sagt wohl
+  -- $( \\sum_i 0 + 0 ) = 0$. Dann ist das vielleicht doch nicht so komplex.
+
+  -- **Robo**: Genau! Man schreibt `\\sum`. Beachte den Index:
+  -- $( \\sum_\{i=0}^\{n-1} 0 + 0 ) = 0$, also `Fin n` ist ein Typ mit den Elementen
+  -- $\\{0, \\ldots, n-1\\}$.
+
+  -- **Du**: Oke, also `Fin n` hat `n` Elemente. Und was mach ich jetzt?
+
+  -- **Robo**: `simp` ist eine ganz starke Taktik, die viele Terme vereinfacht, wir
+  -- fangen besser an, diese zu benützen.
+
+  -- Irgendwie hast du das Gefühl ein Déjà-vue zu haben…"
  simp

-NewTactic simp
+OnlyTactic simp
+
+Conclusion "**Unbekannte**: Sehr gut, folgt mir!"
@@ -13,29 +13,42 @@ Title "endliche Summe"

 Introduction
 "
-Generell sind aber nur solche Lemmas `@[simp]` markiert, klar eine Vereinfachung darstellen.
-
-So ist ein Lemma wie `Finset.sum_add_distrib` kein `simp`-Lemma, da beide Seiten je
-nach Situation bevorzugt sein könnte:
-
-$$
-  \\sum_{i = 0}^n a_i + b_i = \\sum_{i = 0}^n a_i + \\sum_{j = 0}^n b_j
-$$
-
-Dieses Lemma kann aber mit `rw` angewendet werden.
+Während euch die Person zu einem besonders herausragenden Steinturm führt, löchert
+sie euch noch weiter mit Fragen.
 "

 open BigOperators

 Statement
-"Zeige dass $\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$."
+    "$\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$."
    (n : ℕ) : ∑ i : Fin n, ((i : ℕ) + 1) = n + (∑ i : Fin n, (i : ℕ)) := by
-  rw [Finset.sum_add_distrib]
-  Hint "Die zweite Summe `∑ x : Fin n, 1` kann `simp` zu `n` vereinfacht werden."
-  simp
-  Hint "Bis auf Umordnung sind jetzt beide Seiten gleich, darum kann `ring` das Goal schließen.
+  -- Hint "**Du**: Hmm, wieder `simp`?

-    Alternativ kann man auch mit `rw [add_comm]` dies explizit umordnen."
+  -- **Robo**: Nicht ganz. `simp` benützt nur Lemmas, die klar eine Vereinfachung darstellen,
+  -- und in deiner Bibliothek mit `@[simp]` markiert wird. Hier brauchen wir eine andere
+  -- Umformung:
+
+  -- $$
+  -- \\sum_\{i = 0}^n a_i + b_i = \\sum_\{i = 0}^n a_i + \\sum_\{j = 0}^n b_j
+  -- $$
+
+  -- **Robo*: Da unklar ist, welche Seite \"einfacher\" ist, wird so ein Lemma nicht mit
+  -- `@[simp]` markiert. Das heisst du musst `Finset.sum_add_distrib` mit `rw`
+  -- explizit anwenden.
+  -- "
+  rw [Finset.sum_add_distrib]
+  Hint "**Robo**: Die zweite Summe `∑ x : Fin n, 1` kann jetzt aber mit
+  `simp` zu `n` vereinfacht werden."
+  simp
+  Hint "**Robo**: Bis auf Umordnung sind jetzt beide Seiten gleich!
+
+  **Du**: Dann greift jetzt wohl `ring`!
+
+  **Robo**: Genau! Und alternativ könntest du mit `rw [add_comm]` die Arbeit von `ring`
+  auch manuell machen."
  ring

 NewLemma Finset.sum_add_distrib add_comm
+
+Conclusion "Eure Begleitung scheint mit der Antwort zu frieden zu sein und zeigt
+freudig an dem Turm empor, den ihr soeben erreicht habt."
@@ -15,78 +15,75 @@ Title "Arithmetische Summe"

 Introduction
 "
-Oft beweist man Aussagen über Summen am besten per Induktion.
+**Du**: Wie werden solche Meisterwerke eigentlich gebaut?

-Mit `induction n` startet man einen Induktionsbeweis. Dies erstellt 2 neue Goals:
+Da zeigt eure Begleitung auf eine kleine Steinplatte neben dem Eingang,
+auf der eien Beschreibung gekritzelt ist.

-* **Induktionsanfang**: `n = 0`. Dieser kann ganz oft direkt mit `simp` bewiesen werden.
-* **Induktionsschritt**: Man kriegt eine Annahme `(n_ih : P n)` und muss `P (n + 1)`
-  beweisen. Für endliche Summen will man normalerweise danach zuerst
-  `rw [Fin.sum_univ_castSucc]` brauchen, welches
-  $$\\sum_{i=0}^{n} a_i = \\sum_{i=0}^{n-1} a_i + a_n$$
-  umschreibt.
-
-**Bemerkung:**
-
-Eine technische Sonderheit bezüglich endlichen Summen
-ist der kleine Pfeil `↑` in `∑ i : Fin (n + 1), ↑i`.
-Da `i : Fin n` technisch keine natürliche Zahl ist (sondern vom Typ `Fin n`), muss man
-dieses zuerst mit `↑i` oder `(i : ℕ)` in eine natürliche Zahl umwandeln. Diese nennt man
-*Coersion*.
-
-Gleichermassen, kommen hier im Induktionsschritt die Terme `↑(↑Fin.castSucc.toEmbedding i)`
-und `↑(Fin.last (n + 1))` vor. Diese Terme können mit `simp` vereinfacht werden.
+**Robo**: Das ist wohl der bekannte arithmetische Turm von Indu, über den hab ich schon
+einmal Daten verarbeitet. Und die antwort auf deine Frage: Vermutlich ein Stein nach
+dem anderen.
 "

 open BigOperators

 Statement arithmetic_sum
-"Zeige $2 \\cdot \\sum_{i = 0}^n i = n \\cdot (n + 1)$."
+    "$2 \\cdot \\sum_{i = 0}^n i = n \\cdot (n + 1)$."
    (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
+  Hint "**Du**: Klar, die werden ja nicht oben anfangen mit bauen. Sag mal,
+  wie zeige ich denn die arithmetische Summe, die hier gekritzelt steht?
+  Ich würde gerne Induktion über $n$ anwenden.
+
+  **Robo**: Ja dann ist's einfach `induction n`, ist doch logisch!"
  induction n
+  Hint "**Du**: Zuerst den Induktionsanfang…
+
+  **Robo**: Diesen kannst du oft mit `simp` abkürzen!"
  simp
+  Hint "**Robo**: Jetzt im Induktionsschritt: Bei Induktion über endlichen Summen willst du
+  immer mit `rw [Fin.sum_univ_castSucc]` anfangen" -- :
+
+  -- $$\\sum_\{i=0}^n a_i = \\sum_{i=0}^\{n-1} a_i + a_n$$"
  rw [Fin.sum_univ_castSucc]
-  rw [mul_add]
+  -- TODO: Bug. Dieser Hint wird nicht angezeigt.
+  Hint "**Du**: Oh das sieht jetz aber kompliziert aus…
+
+  **Robo**: Da musst du etwas drüber hinweg lesen. Am besten machst du kurz `simp`,
+  dann sieht's schon wieder besser aus."
  simp
+  Hint "**Du**: Was bedeutet eigentlich der kleine Pfeil `↑`?
+
+  **Robo**: Das ist eine *Coersion*. Sowas wie wenn man eine natürliche Zahl als Integer anschaut,
+  also die natürliche Abbildung `ℕ ↪ ℤ`. Oder hier, wenn ein Element `x : Fin n` stattdessen als
+  Element in `(↑x : ℕ)` angeschaut wird.
+
+  **Robo**: Übrigens, um die Induktionshypothese anzuwenden brauchst du zuerst das Lemma
+  `mul_add`."
+  rw [mul_add]
+  Hint "**Du**: Und wie wende ich jetzt die Induktionshypothese an?
+
+  **Robo mit `rw` wie jede andere Annahme auch."
  rw [n_ih]
+  Hint "**Robo**: Jetzt musst du noch kurz `rw [Nat.succ_eq_add_one]` anwenden.
+
+  **Du**: Aber wieso?
+
+  **Robo**: Naja, `ring` ist jetzt auch noch nicht so stark, und erkennt nicht dass `n.succ`
+  und `n + 1` das gleiche sind.
+
+  **Du**: Aber das könnte man doch ändern, oder?
+
+  **Robo**: Vielleicht wenn wir einmal einem Techniker begegnen, der mir ein Update
+  einspielen kann…"
+  Branch
+    ring_nf
+    Hint "**Robo**: Wie gesagt, brauch doch `rw [Nat.succ_eq_add_one]` als Fix für meine
+    kleinen Maken."
  rw [Nat.succ_eq_add_one]
  ring

 NewTactic induction
 NewLemma Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul

-Hint (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) =>
-"Als Erinnerung, einen Induktionsbeweis startet man mit `induction n`."
-
-Hint : 2 * ∑ i : Fin (Nat.zero + 1), ↑i = Nat.zero * (Nat.zero + 1) =>
-"Den Induktionsanker $n = 0$ kann `simp` oft beweisen."
-
-Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
-  2 * ∑ i : Fin (Nat.succ n + 1), ↑i = Nat.succ n * (Nat.succ n + 1) =>
-"Den Induktionsschritt beginnt man oft mit `rw [Fin.sum_univ_castSucc]`."
-
-- Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
--   2 * (∑ i : Fin (n + 1), ↑(Fin.castSucc.toEmbedding i) +
--   ↑(Fin.last (n + 1))) = Nat.succ n * (Nat.succ n + 1) =>
-- "Die Taktik `simp` vereinfacht `↑(↑Fin.castSucc.toEmbedding i)`. "
-
-Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
-  2 * (∑ x : Fin (n + 1), ↑x + (n + 1)) = Nat.succ n * (Nat.succ n + 1) =>
-"Um Die Induktionshypothese anzuwenden muss man noch
-$$2 \\cdot ((\\sum_\{x=0}^n x) + (n + 1)) = 2 \\cdot \\sum_\{x=0}^n x + 2 \\cdot (n + 1))$$
-umschreiben. Dazu kannst du `mul_add` benützen.
-"
-
-Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
-  2 * ∑ x : Fin (n + 1), ↑x + 2 * (n + 1) = Nat.succ n * (Nat.succ n + 1) =>
-"`simp` vereinfacht `↑(↑Fin.castSucc.toEmbedding i)` zu `↑i`.
-Danach kann die Induktionshypothese mit `rw` angewendet werden."
-
-Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
-  n * (n + 1) + 2 * (n + 1) = Nat.succ n * (Nat.succ n + 1) =>
-"
-Im Moment muss man hier `ring` noch helfen,
-indem man mit `rw [Nat.succ_eq_add_one]` zuerst `Nat.succ n = n + 1` umschreibt.
-
-(Dies wird irgendwann noch gefixt)
-"
+Conclusion "Du schaust dich um und bewunderst das Tal in dem hunderte, wenn nicht tausende,
+Steintürme in allen Formen und Höhen stehen."
@@ -12,47 +12,22 @@ Title "Summe aller ungeraden Zahlen"

 Introduction
 "
-Hier nochmals eine Übung zur Induktion.
+**Du**: Haben eigentlich alle Türme hier so kryptische Beschreibungen am Eingang?
+
+Du gehst zu einem etwas kleineren Nachbarsturm.
 "
 set_option tactic.hygienic false

 open BigOperators

 Statement odd_arithmetic_sum
-"Zeige folgende Gleichung zur Summe aller ungeraden Zahlen:
-
-$\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
+    "$\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
    (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 := by
-  induction' n with n hn
+  Hint "**Robo**: Das funktioniert genau gleich wie zuvor, viel Glück."
+  induction n
  simp
  rw [Fin.sum_univ_castSucc]
  simp
-  rw [hn]
+  rw [n_ih]
  rw [Nat.succ_eq_add_one]
  ring
-
-HiddenHint (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 =>
-"
-Fange wieder mit `induction {n}` an.
-"
-
-HiddenHint : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 =>
-"
-Den Induktionsanfang kannst du wieder mit `simp` beweisen.
-"
-
-HiddenHint (n : ℕ) : ∑ i : Fin (Nat.succ n), ((2 : ℕ) * i + 1) = Nat.succ n ^ 2 =>
-"
-Den Induktionsschritt startest du mit `rw [Fin.sum_univ_castSucc]`.
-"
-
-HiddenHint (n : ℕ) (hn : ∑ i : Fin n, (2 * (i : ℕ) + 1) = n ^ 2) :
-  ∑ x : Fin n, (2 * (x : ℕ) + 1) + (2 * n + 1) = Nat.succ n ^ 2 =>
-"
-Hier kommt die Induktionshypothese {hn} ins Spiel.
-"
-
-HiddenHint (n : ℕ) : n ^ 2 + (2 * n + 1) = Nat.succ n ^ 2 =>
-"
-Mit `rw [Nat.succ_eq_add_one]` und `ring` kannst du hier abschliessen.
-"
@@ -18,19 +18,32 @@ Title "Summe vertauschen"

 Introduction
 "
-Verschachtelte endliche Summen kann man beliebig tauschen.
+Nun aber zeigt euch eure Begleiterin zwei weitere Türme mit einer kleinen Brücke, die
+zwischen den beiden verläuft. Die Tafel am Eingang wurde von einem herunterfallenden Stein
+zerstört. Auf der oberen Hälfte steht nur folgendes:

 $$\\sum_{i=0}^n\\sum_{j=0}^m a_{ij} = \\sum_{j=0}^m\\sum_{i=0}^n a_{ij}$$

-Dieses Lemma heisst `Finset.sum_comm`
+**Du**: Ich glaube, ich kann das in eurem Dialekt formulieren und euch damit helfen!
 "


 Statement
-"Zeige dass
-$\\sum_{i=0}^n\\sum_{j=0}^m  2^i (1 + j) = \\sum_{j=0}^m\\sum_{i=0}^n  2^i (1 + j)$."
-    (n m : ℕ) : ∑ i : Fin n, ∑ j : Fin m, ( 2^i * (1 + j) : ℕ) =
+(n m : ℕ) : ∑ i : Fin n, ∑ j : Fin m, ( 2^i * (1 + j) : ℕ) =
    ∑ j : Fin m, ∑ i : Fin n, ( 2^i * (1 + j) : ℕ) := by
+  Hint "**Robo**: Das sieht gut aus, aber du solltest das kurz beweisen, um sicher zu sein.
+
+  **Du**: Hast du nicht ein Lemma dafür?
+
+  **Robo**: Doch, probier mal `Finset.sum_comm`."
  rw [Finset.sum_comm]

 NewLemma Finset.sum_comm
+
+Conclusion "
+  Euer Begleiter ist ganz begeistert als er dir das Stück Papier aus den Händen nimmt,
+  auf dem du die Aussage gekritzelt hast. Gleich zückt sie einen Meißel und beginnt eine
+  neue Platte zu erstellen.
+
+  Ihr winkt ihr noch zum Abschied und geht weiter.
+"
@@ -17,109 +17,76 @@ Title "Zusammenfassung"

 Introduction
 "
-Zusammenfassung aus diesem Kapitel
+**Du**: Robo gib mir nochmals eine Übersicht, bitte.

-## Notationen / Begriffe
+**Robo**: Aber klar:

 |                      | Beschreibung                              |
 |:---------------------|:------------------------------------------|
 | `Fin n`              | Ist ein Typ mit Zahlen $0, \\ldots, n-1$. |
 | `∑ (i : Fin n), a i` | $\\sum_{i=0}^{n-1} a_i$                   |
+| `↑i`                 | Eine Coersion, z.B. `Fin n → ℕ`.          |

-## Taktiken
+und

 |    | Taktik                    | Beispiel                             |
 |:---|:--------------------------|:-------------------------------------|
-| 20 | `simp`                    | Simplifikation.                      |
-| 21 | `induction n`             | Induktion über $n$                   |
+| 21 | `simp`                    | Simplifikation.                      |
+| 22 | `induction n`             | Induktion über $n$                   |

-Und hier noch eine etwas schwierigere Übung.
-
-Das Resultat aus Level 3 kannst du als `arithmetic_sum` wiederverwenden:
-$$
-2 \\cdot \\sum_{i = 0}^n i = n \\cdot (n + 1)
-$$
+Da löst sich aus der Steinlandschaft plötzlich ein grosser Steingolem. Er schaut euch
+bedrohlich an und fragt in tiefer Stimme:
 "

 open BigOperators

-Statement
-"Zeige $\\sum_{i = 0}^m i^3 = (\\sum_{i = 0}^m i)^2$."
-  (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), (i : ℕ))^2 := by
-  induction' m with m hm
+Statement (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), (i : ℕ))^2 := by
+  Hint "**Du**: Gulp. Naja das wird schon klappen. Also man fängt wieder mit Induktion an…"
+  induction m
+  Hint "**Du**: Also den Induktionsanfang kann man einfach zeigen…"
  simp
+  Hint "**Robo**: Und jetzt wieder `rw [Fin.sum_univ_castSucc]` und `simp` um vorwärts zu
+  kommen!"
  rw [Fin.sum_univ_castSucc]
  simp
-  rw [hm]
-  rw [Fin.sum_univ_castSucc (n := m + 1)]
+  Hint "**Robo**: Siehst du die Induktionshypothese hier drin?"
+  rw [n_ih]
+  Hint "**Du**: Ok, damit habe ich die linke Seite der Gleichung ziemlich gut bearbeitet.
+  Aber, ehm, mit der Rechten komme ich nicht weiter…
+
+  Der Golem schaut dich finster an.
+
+  **Robo**: Du willst `Fin.sum_univ_castSucc` auf der rechten Seite anwenden, aber es
+  gibt mehrere Orte, wo das Lemma passen würde.
+  Deshalb musst du mit `rw [Fin.sum_univ_castSucc (n := {n} + 1)]` angeben, wo genau.
+
+  **Du**: Was bedeutet das?
+
+  **Robo** Das Lemma hat eine Annahme `n` und du sagst ihm explizit, was es für dieses `n`
+  einsetzen muss, nämlich `{n} + 1`"
+  Branch
+    rw [Fin.sum_univ_castSucc]
+    Hint "**Robo**: Das hat jetzt einfach `Fin.sum_univ_castSucc` am ersten Ort angewendet,
+    wo das möglich war. Das ist nicht so ideal, die like Seite war schon okay.
+
+    **Robo**: Geh doch zurück und bring `rw` dazu am anderen Ort umzuschreiben."
+  rw [Fin.sum_univ_castSucc (n := n + 1)]
  simp
+  Hint "**Robo**: `add_pow_two` ist auch noch nützlich!"
  rw [add_pow_two]
+  Hint "**Du**: Ich glaube, ich sehe hier ne arithmetische Summe drin!!
+
+  **Robo**: Ich habe dir das dies von vorhin temporär als `arithmetic_sum` gespeichert,
+  damit du diese brauchen kannst."
  rw [arithmetic_sum]
+  Hint "**Du**: Jetzt sollten es eigentlich nur noch arithmetische Operationen sein."
  ring

 NewLemma arithmetic_sum add_pow_two

-HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (m + 1), ↑i) ^ 2 =>
-"Führe auch hier einen Induktionsbeweis."
+Conclusion "Der Golem denkt ganz lange nach, und ihr bekommt das Gefühl, dass er gar nie
+aggressive war, sondern nur eine sehr tiefe Stimme hat.

-HiddenHint : ∑ i : Fin (Nat.zero + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.zero + 1), ↑i) ^ 2 =>
-"`simp` kann den Induktionsanfang beweisen."
+Mit einem kleinen Erdbeben setzt er sich hin und winkt euch dankend zu.

-Hint (m : ℕ) : ∑ i : Fin (Nat.succ m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
-"Im Induktionsschritt willst du das Goal so umformen, dass du folgende Therme
-ersetzen kannst:
-
-* `∑ i : Fin (m + 1), ↑i ^ 3` (Induktionshypothese)
-* `2 * (∑ i : Fin (m + 1), ↑i)` (arithmetische Summe)
-"
-
-HiddenHint (m : ℕ) : ∑ i :
-    Fin (Nat.succ m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
-"
-Als erstes kannst du mal mit dem bekannten `rw [Fin.sum_univ_castSucc]` anfangen.
-"
-
-HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), (Fin.castSucc.toEmbedding i : ℕ) ^ 3 +
-    ↑(Fin.last (m + 1)) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
-"Mit `simp` kriegst du das `↑(Fin.castSucc.toEmbedding i)` weg"
-
-Hint (m : ℕ) : ∑ x : Fin (m + 1), (x : ℕ) ^ 3 + (m + 1) ^ 3 =
-    (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
-"Jetzt kannst du die Induktionshypothese benützen."
-
-Hint (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
-"Die linke Seite ist jetzt erst mal gut. Um auf der rechten Seite `Fin.sum_univ_castSucc`
-anzuwenden, haben wir ein Problem: Lean schreibt immer die erste Instanz um, also würde gerne
-auf der linken Seite `(∑ i : Fin (m + 1), ↑i) ^ 2` umschreiben.
-
-Wir können Lean hier weiterhelfen, indem wir manche Argemente von `Fin.sum_univ_castSucc`
-explizit angeben. Die Funktion hat ein Argument mit dem Namen `n`, welches wir z.B. explizit
-angeben können:
-
-```
-rw [Fin.sum_univ_castSucc (n := m + 1)]
-```
-"
-
-HiddenHint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
-    (∑ i : Fin (m + 1), ↑(Fin.castSucc.toEmbedding i) + ↑(Fin.last (m + 1))) ^ 2 =>
-"Wenn du noch einen AUsdruck `↑(Fin.castSucc.toEmbedding i)` hast, solltest du mal
-`simp` aufrufen."
-
-Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (m + 1), ↑i + (m + 1)) ^ 2 =>
-"Die rechte Seite hat die Form $(a + b)^2$ welche mit `add_pow_two` zu $a^2 + 2ab + b^2$
-umgeschrieben werden kann."
-
-HiddenHint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
-    (∑ i : Fin (m + 1), ↑i) ^ 2 + (2 * ∑ i : Fin (m + 1), ↑i) * (m + 1) + (m + 1) ^ 2 =>
-"Wenn du noch einen AUsdruck `↑(Fin.castSucc.toEmbedding i)` hast, solltest du mal
-`simp` aufrufen."
-
-Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
-    (∑ i : Fin (m + 1), ↑i) ^ 2 + (2 * ∑ i : Fin (m + 1), ↑i) * (m + 1) + (m + 1) ^ 2 =>
-"Jetzt hast du in der Mitte `2 * ∑ i : Fin (m + 1), ↑i)`, welches du mit der
-arithmetischen Summe `arithmetic_sum` umschreiben kannst."
-
-Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
-    (∑ i : Fin (m + 1), ↑i) ^ 2 + m * (m + 1) * (m + 1) + (m + 1) ^ 2 =>
-"Den Rest sollte `ring` für dich übernehmen."
+Damit zieht ihr weiter durch die karge Landschaft auf diesem Planet."