merge necessary as upstream developed while storyline slept

server/adam/Adam/Levels/Contradiction.lean

@@ -0,0 +1,16 @@
+import Adam.Levels.Contradiction.L01_Have
+import Adam.Levels.Contradiction.L02_Suffices
+import Adam.Levels.Contradiction.L03_ByContra
+import Adam.Levels.Contradiction.L04_ByContra
+import Adam.Levels.Contradiction.L05_Contrapose
+import Adam.Levels.Contradiction.L06_Summary
+
+Game "Adam"
+World "Contradiction"
+Title "Widerspruch"
+
+Introduction "
+Ihr begebt euch auf die Suche nach *Oddeus*. Nach etwas rumfragen, kommt ihr tatsächlich an
+eine Dornenfestung und nachdem ihr erklärt habt, wer ihr seit, werdet ihr auf eine Audienz
+gebeten.
+"

server/adam/Adam/Levels/Contradiction/L01_Have.lean

@@ -0,0 +1,60 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Contradiction"
+Level 1
+
+Title "Have"
+
+Introduction
+"
+**Oddeus**: Willkommen Reisende! Ich muss eingestehen ich bin in Gedanken noch
+an etwas, könnt ihr mir bei diesem widersprüchlichen Problem helfen?
+"
+
+-- Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
+-- Zwischenresultat beweisen, welches wir dann benützen können.
+
+-- Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
+-- dass man anschliessen beweisen muss.
+
+-- Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
+-- du mit
+-- ```
+-- have g : ¬ B
+-- apply h
+-- assumption
+-- ```
+-- eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
+-- bevor du dann mit dem Beweis forfährst.
+
+Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
+  Hint "**Du**: Also als erstes Teile ich wohl mal das Und (`∧`) auf."
+  rcases k with ⟨h₁, h₂⟩
+  Hint "**Du**: Aber jetzt…
+
+  **Robo**: Du könntest dir ein passendes Zwischenresultat zurechtlegen, das dir hilft:
+  Mach mal `have g : ¬ B`!"
+  have g : ¬ B
+  · Hint "**Du**: Was und jetzt hab ich einfach angenommen das sei richtig?
+
+    **Robo**: Ne, jetzt musst du das zuerst beweisen bevor du es dann benützen kannst."
+    Hint (hidden := true) "**Robo**: `apply` scheint passend zu sein."
+    apply h
+    assumption
+  · Hint (hidden := true) "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen?
+
+    **Robo**: `contradiction`."
+    contradiction
+
+NewTactic «have»
+DisabledTactic «suffices»
+
+Conclusion "*Oddeus*: Das stimmt wohl."

server/adam/Adam/Levels/Contradiction/L02_Suffices.lean

@@ -0,0 +1,63 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Contradiction"
+Level 2
+
+Title "Suffices"
+
+Introduction
+"
+*Oddeus*' Partner meldet sich.
+
+**Partner**: Ich habe letzthin was änliches gesehen, aber irgendwie verdreht.
+"
+
+-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
+-- vertauscht aber die beiden Beweisblöcke:
+
+-- ```
+-- suffices h : [Aussage]
+-- [Beweis des Goals (mithilfe von h)]
+-- [Beweis der Aussage h]
+-- ```
+-- Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
+-- \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
+
+-- Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
+-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
+-- `suffices` schöner gewesen:
+
+Statement
+    "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
+    $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
+    (A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
+  Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
+  brauchen. Das funktioniert genau gleich, aussert dass dann die beiden Goals vertauscht sind.
+
+  **Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
+  abschliesst bevor ich `g` beweise?
+
+  **Robo**: Genau! Verwendende `have` und `suffices` einfach nach gutdünken."
+  suffices g : ¬ B
+  Hint "**Robo**: Also hier beendest du den Beweis angenommen {g} sei wahr."
+  contradiction
+  Hint "**Robo**: Und hier beweist du das Zwischenresultat."
+  apply h
+  assumption
+
+NewTactic «suffices»
+DisabledTactic «have»
+
+Conclusion "*Oddeus* nimmt den Brief, schaut ihn an und, rollt ihn zusammen.
+
+**Oddeus**: Ich verstehe meine Schwester nie. Kommt, vielleicht könnt ihr mir helfen.
+
+Und er führt euch durch seinen Rosengarten."

server/adam/Adam/Levels/Contradiction/L03_ByContra.lean

@@ -0,0 +1,65 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+import Mathlib
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Contradiction"
+Level 3
+
+Title "Per Widerspruch"
+
+Introduction
+"**Oddeus**: Ich verstehe *Evenine* einfach nicht. Ich will euch auch gleich zeigen,
+was sie mir letzthin geschrieben hat, aber zuerst schaut einmal unseren
+wunderschönen Absurda-Tempel an!
+
+Damit kommt ihr vor einen sehr hohen Turm, der ausschliesslich aus Dornenranken gewachsen
+scheint.
+
+**Oddeus**: Versteht ihr, was hier über dem Eingang steht?
+"
+
+--   Eine sehr nützliche Beweismethode ist per Widerspruch.
+
+-- Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
+-- sucht, und damit jegliches beweisen kann.
+
+-- Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
+-- Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
+
+-- Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
+-- steht:
+
+Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
+  Hint "**Robo**: Ein `¬` im Goal heisst häufig, dass du einen Widerspruchsbeweis führen
+  möchtest.
+
+  **Du**: Und wie mach ich das? Mit `contradiction`?
+
+  **Robo**: Mit `by_contra h` fängst du einen an. Mit `contradiction` schliesst du ihn dann
+  später ab."
+  by_contra h
+  Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : ¬ {A}`, und damit musst du einen
+  Widerspruch herbeileiten.
+
+  Ein Methode ist, dass du jetzt mit `suffices` sagts, zu was du denn gerne den Widerspruch
+  haben möchtest, zum Beispiel `suffices k : B`
+  "
+  suffices k : B
+  Hint "**Du**: Ah und jetzt kann ich einfach sagen dass sich die Anahmen `{B}` und `¬{B}`
+  widersprechen."
+  contradiction
+  Hint "**Robo**: Und jetzt kannst du noch das Ergebnis zeigen, das zu einem Widerspruch
+  geführt hat."
+  apply g
+  assumption
+
+NewTactic by_contra
+
+Conclusion "**Oddeus**: Sehr gut, kommt mit hinein!"

server/adam/Adam/Levels/Contradiction/L04_ByContra.lean

@@ -0,0 +1,51 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+import Mathlib
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Contradiction"
+Level 4
+
+Title "Per Widerspruch"
+
+Introduction
+"
+*Oddeus* Geht zu einem Regal mit vielen Dokumenten und beginnt zu suchen.
+
+**Oddeus**: Ich hab's gleich. Hier ist eine Notiz meiner Gelehrter, die mir
+mit solchen kryptischen Nachrichten helfen wollten.
+
+Auf dem Pergament steht das ein Lemma mit dem Namen `not_imp_not`:
+"
+
+Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
+  Hint "**Du**: Ich glaube, dafür kenn ich das meiste schon."
+  Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
+  constructor
+  intro h b
+  by_contra a
+  Hint "**Robo**: Zur Erinnerung, hier würde ich mit `suffices g : B` einen Widerspruch
+  herbeiführen."
+  suffices b : B
+  contradiction
+  apply h
+  assumption
+  intro h a
+  Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruch anfangen."
+  by_contra b
+  Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
+  suffices g : ¬ A
+  contradiction
+  apply h
+  assumption
+
+DisabledTactic rw
+DisabledLemma not_not
+
+Conclusion "**Du**: Und wie hilft uns das jetzt, was steht denn in dem Brief?"

server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean

@@ -0,0 +1,70 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Contradiction"
+Level 5
+
+Title "Kontraposition"
+
+Introduction
+"
+*Oddeus* reicht euch das Papier.
+
+**Du**: Da steht etwas über `contrapose` hier…
+
+**Oddeus**: Das ist doch klar eine Aggression uns gegenüber!
+
+**Robo**: Wartet mal, vielleicht wollte euch eure Schwester einfach von ihren neuen
+Endeckungen zeigen. Schaut, darunter ist eine Aufgabe.
+"
+
+-- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
+
+-- ```
+-- lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
+--   [...]
+-- ```
+
+-- Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
+-- entsprechend umdreht.
+
+-- Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
+-- im Goal erstellt.
+
+-- Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
+-- Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
+-- logisch equivalent sind.
+
+-- Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
+open Nat
+
+Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
+  Hint "**Oddeus**: Wie soll das den gehen?
+
+  **Robo**: `contrapose` benutzt das Lemma eurer Gelehrter, `not_imp_not`. Also es wandelt
+  ein Goal `A → B` zu `¬B → ¬A ` um.
+
+  **Du**: Aber das Goal ist doch gar keine Implikation?
+
+  **Robo**: Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Goal
+  schieben."
+  revert h
+  Hint "*Oddeus*: Ob man jetzt wohl dieses `contrapose` benutzen kann?"
+  contrapose
+  Hint (hidden := true) "**Du**: Warte mal, jetzt kann man wohl `even_iff_not_odd` verwenden…"
+  rw [← even_iff_not_odd]
+  rw [← even_iff_not_odd]
+  Hint "**Robo**: Und den Rest hast du bei *Evenine* als Lemma gezeigt!"
+  apply even_square
+
+NewTactic contrapose
+DisabledTactic by_contra
+
+Conclusion "**Oddeus**: Ah ich sehe, die Aussage ist, dass wir das nur zusammen lösen konnten.
+Ich danke euch, darauf wäre ich nie gekommen."

server/adam/Adam/Levels/Contradiction/L06_Summary.lean

@@ -0,0 +1,56 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Contradiction"
+Level 6
+
+Title "Contradiction"
+
+Introduction
+"
+**Du**: Sag mal Robo, das hätte ich aber auch als Widerspruch anstatt Kontraposition
+beweisen können?
+
+**Robo**: Klar. `contrapose` ist eine Kontraposition, `by_contra` ein Widerspruchsbeweis.
+Probiers doch einfach!
+In diesem Kapitel hast du also folgende Taktiken kennengelernt:
+
+
+Als Vergleich zwischen Beweisen \"per Widerspruch\"
+und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
+du mit `by_contra` einen Widerspruch suchst.
+"
+
+open Nat
+
+Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
+  Hint "**Robo**: Fang diesmal mit `by_contra g` an!"
+  by_contra g
+  Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
+  Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
+  suffices d : ¬ Odd (n ^ 2)
+  contradiction
+  rw [←even_iff_not_odd] at *
+  apply even_square
+  assumption
+
+DisabledTactic contrapose revert
+
+Conclusion "**Robo**: Bravo! Hier nochmals ein Überblick, was wir jetzt alles auf diesem
+Mond gelernt haben:
+
+|       | Taktik          | Beispiel                                               |
+|:------|:----------------|:-------------------------------------------------------|
+| 177   | `have`          | Zwischenresultat annehmen.                             |
+| 18    | `suffices`      | Zwischenresultat annehmen.                             |
+| 19    | `by_contra`     | Widerspruch. (startet einen Widerspruch)               |
+| *3*   | `contradiction` | *(Schliesst einen Widerspruchsbeweis)*                 |
+| 20    | `contrapose`    | Kontraposition.                                        |
+| *9*   | `revert`        | Nützlich um danach `contrapose` anzuwenden.            |
+"

server/adam/Adam/Levels/Function.lean

@@ -0,0 +1,24 @@
+import Adam.Levels.Function.L01_Function
+import Adam.Levels.Function.L02_Let
+import Adam.Levels.Function.L03_Piecewise
+import Adam.Levels.Function.L04_Injective
+import Adam.Levels.Function.L05_Injective
+import Adam.Levels.Function.L06_Injective
+import Adam.Levels.Function.L07_Surjective
+import Adam.Levels.Function.L08_Bijective
+import Adam.Levels.Function.L09_Inverse
+import Adam.Levels.Function.L11_Inverse
+
+Game "Adam"
+World "Function"
+Title "Abbildungen"
+
+Introduction "
+Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf
+eine Insel komplett mit Wasser bedeckt zu sein scheint.
+
+Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,
+vereinzelte aus Lehm.
+
+Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt.
+"

server/adam/Adam/Levels/Function/L01_Function.lean

@@ -0,0 +1,63 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 1
+
+Title "Anonyme Funktionen"
+
+Introduction
+"
+Auf die Frage hin, ob sie von einem Bibliothek wisse, erzählt euch das kleine Mädchen,
+dass es auf der Insel nur einen gäbe, aber sie bedrängt euch so mit einer Frage,
+dass sie euch gar nicht sagt, wo dieser zu finden sei.
+"
+
+Statement "" : ∃ f : ℤ → ℤ, ∀ x, f x < x := by
+  use (fun x ↦ x - 1)
+  simp
+
+Hint : ∃ f : ℤ → ℤ, ∀ x, f x < x =>
+"
+**Robo**: `f : ℤ → ℤ` ist die Notation für eine Funktion und `f x` ist diese Funktion
+angewendet auf ein Element `(x : ℤ)`.
+
+**Du**: War `→` nicht eben noch eine Implikation?
+
+**Robo**: Doch, die brauchen das gleiche Zeichen für beides.
+
+**Du**: Dann ist `f : ℤ → ℤ` also einfach abstrakt irgendeine Funktion,
+wie definier ich aber jetzt konkret eine Abbildungsvorschrift?
+
+**Robo**: Man kennt hier eine Notation für eine anonyme Funktion:
+`fun (x : ℤ) ↦ x ^ 2` ist
+
+$$
+\\begin\{aligned}
+  f : \\mathbb\{ℤ} &\\to \\mathbb\{ℤ} \\\\
+  x &\\mapsto x ^ 2
+\\end\{aligned}
+$$
+
+**Robo**: PS, `↦` ist `\\mapsto`. Aber man kann auch stattdessen `=>` benützen.
+"
+
+HiddenHint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
+"
+**Du**: Ja aber was mach ich damit?
+
+**Robo**: Wie immer gehst du ein `∃` mit `use …` an.
+"
+
+-- TODO: Why does this not show?
+HiddenHint : ∀ (x : ℤ), (fun (y : ℤ) => y - 1) x < x =>
+"**Du**: Zu was sich das wohl vereinfacht?"
+
+HiddenHint (x : ℤ) : (fun y => y - 1) x < x =>
+"**Du**: Zu was sich das wohl vereinfacht?"
+
+Conclusion "Das Mädchen wird kurz ruhig, dann beginnt es zu lächeln und zeigt strahlend
+in eine Richtung. Ihr folgt ihrem Finger und euch fällt in weiter ferne eine pompöse Struktur
+auf einem flachen Hügel auf.
+"

server/adam/Adam/Levels/Function/L02_Let.lean

@@ -0,0 +1,82 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 2
+
+Title "let"
+
+Introduction
+"
+Ihr macht euch auf Richtung Bibliothek entlang kleiner Pfade zwischen verschiedenster Behausungen.
+
+**Du**: Sag mal, ich weiss jetzt dass ich eine Funktion als `fun x ↦ x - 1` definieren kann,
+aber wie kann ich der einen Namen geben?
+
+**Robo**: Wenn jemand hier eine Funktion definiert, werden die dir
+`def f (x : ℤ) : ℤ := x - 1` oder `def f : ℤ → ℤ := (fun x ↦ x - 1)` geben.
+
+**Du**: Und das bedeutet beides das gleiche?
+
+**Robo**: Praktisch, ja. Aber! Wenn du eine Funktion in einer Aufgabe benennen willst,
+schreibst du `let f := fun (x : ℤ) ↦ x - 1`!
+
+**Du**: Und was ist der Unterschied?
+
+**Robo**: Deines mit `let` ist für innerhalb von einem Beweis, das andere mit `def`
+ist für ausserhalb von einem Beweis. Hier, ich geb dir mal eine Aufgabe:
+
+```
+def f (x : ℤ) : ℤ := (x + 4)
+```
+und:
+"
+
+def f (x : ℤ) : ℤ := (x + 4)
+
+Statement "" (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by
+  let g := fun (x : ℤ) ↦ x - 3
+  use g
+  simp
+  unfold f
+  ring
+
+NewTactic «let»
+NewLemma Function.comp_apply
+
+Hint (x : ℤ) : ∃ g, (g ∘ f) x = x + 1 =>
+"**Du**: Ist `g ∘ f` Komposition von Funktionen?
+
+**Robo**: Richtig! Das schreibt man mit `\\comp`.
+
+  **Du** Und hier könnte ich also zuerst
+`let g := fun (x : ℤ) ↦ _` definieren, anstatt direkt
+`use fun (x : ℤ) ↦ _`?
+
+**Robo**: Genau! Das ist zwar praktisch das gleiche, aber kann manchmal nützlich sein.
+"
+
+-- TODO: Make some hints work here
+Hint (x : ℤ) : ((fun (x : ℤ) ↦ x - 3) ∘ f) x = x + 1 =>
+"**Robo**: Manchmal must du nachhelfen und Funktionen mit `unfold f` öffnen, manchmal nicht.
+Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
+
+-- TODO : Make this work
+Hint (x : ℤ) (g := (fun (x : ℤ) ↦ x - 3)) : (g ∘ f) x = x + 1 =>
+"**Robo**: `(g ∘ f) x` ist per Definition `g (f x)`, aber mit
+`rw [Function.comp_apply]` kann man das explizit umschreiben, aber `simp` kennt das
+Lemma auch."
+
+Hint (x : ℤ) : f x - 3 = x + 1 =>
+"**Robo**: Manchmal must du nachhelfen und Definitionen mit `unfold f` öffnen, mamchmal klappts
+ohne.
+Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
+
+-- TODO: Block simp-Lemma
+
+Conclusion "**Du**: Dann verstehst du etwas Mathe?
+
+**Robo**: Ich hatte ja keine Ahnung ob die generierte Aufgabe beweisbar ist…
+
+Und damit erreicht ihr den Hügel mit der Bibliothek."

server/adam/Adam/Levels/Function/L03_Piecewise.lean

@@ -0,0 +1,177 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 3
+
+Title "Komposition"
+
+Introduction
+"
+Endlich kommt ihr zur Bibliothek. Komischerweise stehen an der Tür
+zwei Wächtern. Der eine zeigt euch ein Blatt mit
+
+```
+def f : ℚ → ℚ := fun x ↦ 5 * x
+```
+
+der andere eines mit
+
+```
+def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
+```
+
+und gibt Dir ein Blatt mit einer einzelnen Zeile am oberen Ende.
+"
+
+open Set
+
+namespace LevelFunction4
+
+def f : ℚ → ℚ := fun x ↦ 5 * x
+def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
+
+Statement ""
+    : f ∘ g = g ∘ f := by
+  funext x
+  simp_rw [Function.comp_apply]
+  unfold g
+  by_cases 0 ≤ x
+  have h' : 0 ≤ f x
+  unfold f
+  linarith
+  rw [if_pos h', if_pos h]
+  unfold f
+  ring
+  have h' : ¬ (0 ≤ f x)
+  unfold f
+  linarith
+  rw [if_neg h, if_neg h']
+  unfold f
+  ring
+
+NewTactic funext by_cases simp_rw linarith
+
+NewLemma not_le if_pos if_neg
+
+
+Hint : f ∘ g = g ∘ f =>
+"
+**Robo**: Schau mal, die beiden haben zwei Funktionen, eine davon mit stückweiser Definition.
+
+**Du**: Und ich soll zeigen, dass die beiden vertauschbar sind?
+
+**Robo**: Genau, am besten wählst du mit `funext x` ein beliebiges Element aus, und zeigst das
+dann für dieses.
+"
+
+-- TODO : This does not trigger.
+-- TODO: These 5 hints should be mutually exclusive. i.e. they should not trigger
+-- if a assumption is missing.
+Hint (x : ℚ) : (f ∘ g) x = (g ∘ f) x =>
+"
+**Du**: Ah und jetzt kann ich erst einmal `(g ∘ f) {x}` zu `g (f {x})` umschreiben?
+
+**Robo**: Mit `simp_rw` geht das übrigens schneller.
+
+**Robo**: Und danach willst du eien Fallunterscheidung
+machen, `by_cases h : 0 ≤ {x}`.
+
+**Du**: Damit krieg ich die Fälle `0 ≤ {x}` und `{x} < 0`?
+
+**Robo**: Genau! Oder präziser `0 ≤ {x}` und `¬(0 ≤ {x})`. Das ist nicht ganz das gleiche, und man
+könnte mit dem Lemma `not_le` zwischen `¬(0 ≤ {x})` und `0 < {x}` wechseln.
+"
+
+Hint (x : ℚ) (h : 0 ≤ x) : f (g x) = g (f x) =>
+"
+**Robo**: Um das ausrechnen zu können, brauchst du nicht nur `0 ≤ x` sondern auch noch
+eine neue Annahme `0 ≤ f x`.
+
+**Du**: Also `have h₂ : _`?
+"
+
+Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = g (f x) =>
+"
+**Du**: Mit den beiden Annahmen sagt die Definition von `g` ja z.B.
+`(if 0 ≤ x then _)` wobei ich weiss dass `0 ≤ x` wahr ist,
+kann ich das dann einfach vereinfachen?
+
+**Robo**: Dafür must du zuerst die Definition von `g` öffnen, also `unfold`. Und dann mit
+dem Lemma `if_pos {h}` das umschreiben.
+"
+
+Hint (x : ℚ) (h : ¬ 0 ≤ x) : f (g x) = g (f x) =>
+"
+**Du**: Ich sehe, das ist jetzt der zweite Fall, da brauch ich sicher wieder eine zweite Annahme
+`¬(0 ≤ f x)`…
+"
+
+Hint (x : ℚ) (h : ¬ 0 ≤ x) (h₂ : ¬ 0 ≤ f x) : f (g x) = g (f x) =>
+"
+**Robo**: Jetzt ist der Zeitpunkt wo die Definition von `g` geöffnet sein sollte.
+
+**Robo**: Wenn man ein If-Statement mit wahrer Prämisse mit `if_pos` vereinfacht, dann
+braucht man für eine falsche Prämisse…
+
+**Du**: `if_neg`?
+"
+-- END TODO
+HiddenHint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (2 * x) = g (f x) =>
+"
+**Robo**: Jetzt das Gleiche noch mit `if_pos {h₂}`.
+"
+
+HiddenHint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = 2 * f x =>
+"
+**Robo**: Jetzt das Gleiche noch mit `if_pos {h}`.
+"
+
+Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (2 * x) = 2 * f x =>
+"
+**Robo**: Wenn du jetzt noch die Definition von `f` öffnest, dann kann `ring` den
+Rest ausrechnen.
+"
+
+
+-- TODO: This are also showing in the case of the Hint below
+-- Proof of `0 ≤ f x`.
+Hint (x : ℚ) (h : 0 ≤ x) : 0 ≤ f x =>
+" **Robo**: Wenn du die Definition von `f` öffnest, dann hast du schon das wissen,
+um das zu beweisen."
+HiddenHint (x : ℚ) (h : 0 ≤ x) : 0 ≤ f x =>
+"**Du** *(in Gedanken)*: Was war das nochmals... Ungleichungen... `linarith`!"
+
+HiddenHint (x : ℚ) (h : ¬0 ≤ x) : ¬ 0 ≤ f x =>
+" **Robo**: Das ist das selbe wie vorhin…"
+
+
+-- Hint for modifying `h` wrongly.
+Hint (x : ℚ) (h : x < 0) : f (g x) = g (f x) =>
+"
+**Robo**: Das war nicht so ideal, hier brauchst du die Annahme in der Form `({h} : ¬ 0 ≤ {x})`!
+"
+
+-- TODO: In this case we get to see the Hints above
+Hint (x : ℚ) (h : 0 ≤ x) : 0 ≤ x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_pos]` anstatt `rw [if_pos {h}]`
+geschrieben hast."
+
+Hint (x : ℚ) (h : 0 ≤ f x) : 0 ≤ f x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_pos]` anstatt `rw [if_pos {h}]`
+geschrieben hast."
+
+Hint (x : ℚ) (h : ¬ 0 ≤ x) : ¬ 0 ≤ x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_neg]` anstatt `rw [if_neg {h}]`
+geschrieben hast."
+
+Hint (x : ℚ) (h : ¬ 0 ≤ f x) : ¬ 0 ≤ f x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_neg]` anstatt `rw [if_neg {h}]`
+geschrieben hast."
+
+Conclusion
+"Zufrieden tauschen die beiden Wächter ihren Platz und geben so dabei den
+Durchgang frei."
+
+end LevelFunction4

server/adam/Adam/Levels/Function/L04_Injective.lean

@@ -0,0 +1,38 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 4
+
+Title ""
+
+Introduction
+"
+Ihr läuft durch verschiedenste Gänge der Bibliothek, allesamt mit Büchern entlang der Wände.
+
+**Du**: Wenn wir wüssten, dass nur ein möglicher Weg hierhin führt, könnten wir
+ausschliessen, dass wir im Kreis laufen.
+
+Plötzlich begegnet ihr einem älteren Wesen mit Fakel. Auf die Frage antwortet es mit
+"
+open Set Function
+
+Statement "" : Injective (fun (n : ℤ) ↦ n + 3) := by
+  intro a b
+  simp
+
+NewDefinition Injective
+
+Hint : Injective (fun (n : ℤ) ↦ n + 3) =>
+"**Robo**: `Injective` ist als `∀ \{a b : U}, f a = f b → a = b`
+definiert, also kannst du mit `intro` anfangen.
+"
+
+Hint (a b : ℤ) : (fun n => n + 3) a = (fun n => n + 3) b → a = b =>
+"**Du**: Kann man das wohl vereinfachen?"
+
+Hint (a b : ℤ) (hab : (fun n => n + 3) a = (fun n => n + 3) b) : a = b =>
+"**Robot**: Jetzt musst du wohl `{hab}` vereinfachen."
+
+Conclusion "**Du** Woa das war ja einfach!"

server/adam/Adam/Levels/Function/L05_Injective.lean

@@ -0,0 +1,79 @@
+import Adam.Metadata
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Function"
+Level 5
+
+Title ""
+
+Introduction
+"
+Sofort hackt die ältere Gestalt nach:
+"
+open Set Function
+
+example (f : ℤ → ℤ) (h : StrictMono f) : Injective f := by
+  apply StrictMono.injective
+  assumption
+
+-- Odd.strictMono_pow
+
+Statement "" : Injective (fun (n : ℤ) ↦ n^3 + (n + 3)) := by
+  apply StrictMono.injective
+  apply StrictMono.add
+  apply Odd.strictMono_pow
+  trivial
+  intro a b
+  simp
+
+NewDefinition Injective
+NewLemma StrictMono.injective StrictMono.add Odd.strictMono_pow
+
+
+Hint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
+"**Du**: Hmm, das ist etwas schwieriger…
+
+**Robo**: Aber ich hab einen Trick auf Lager:
+Das Lemma `StrictMono.injective` sagt, dass jede strikt monotone Funktion injektive ist,
+und ich habe das Gefühl Monotonie ist hier einfacher zu zeigen."
+
+HiddenHint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
+"**Robo**: `apply` ist wonach du suchst."
+
+Hint : StrictMono fun (n : ℤ) => n ^ 3 + (n + 3) =>
+"**Du**: Jetzt möchte ich strikte Monotonie von `n ^ 3` und `n + 3` separat zeigen,
+schliesslich scheint es mir als wär das zweite wieder einfach.
+
+**Robo**: Dafür hab ich `StrictMono.add` bereit!"
+
+Hint : StrictMono fun (x : ℤ) => x ^ 3 =>
+"**Du**: Hmm, darauf hab ich jetzt wenig Lust. Gibt's dafür auch was? Das gilt ja nur
+wenn der Exponent ungerade ist.
+
+**Robo**: Du könntest mal `Odd.strictMono_pow` versuchen…"
+
+HiddenHint : Odd 3 =>
+"**Du**: Ist das nicht ne Trivialität? Warte mal!"
+
+Hint : StrictMono fun (x : ℤ) => x + 3 =>
+"**Du**: Ha! Und dieser Teil funktioniert sicher gleich wie Injektivität vorhin!"
+
+
+
+
+
+
+Hint (a b : ℤ) : a ^ 3 + (a + 3) = b ^ 3 + (b + 3) → a = b =>
+"**Robo**: Ich glaube, dieser Weg ist zu steinig. Fang doch nochmals von vorne an!
+"
+
+Hint (a b : ℤ) (h : a ^ 3 + (a + 3) = b ^ 3 + (b + 3)) : a = b =>
+"**Robo**: Ich glaube, dieser Weg ist zu steinig. Fang doch nochmals von vorne an!
+"
+
+Conclusion "**Du**: Danke vielmals!
+
+Und damit lässt das Wesen mitten im Gang stehen, wo es weiter über Injektivität nachdenkt."

server/adam/Adam/Levels/Function/L06_Injective.lean

@@ -0,0 +1,76 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 6
+
+Title "Injektive"
+
+Introduction
+"
+Weiterirrend kommt ihr an eine Verzweigung.
+
+**Robo**: Sieht beides gleich aus.
+
+Ein paar Schritte in den linken Korridor hinein seht ihr auf dem Boden ein Blatt mit Gekritzel:
+
+```
+def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+```
+
+**Du**: Hier haben wir wieder eine stückweise Funktion
+
+$$
+f(n) = \\begin{cases}
+    n^2 & \\text{falls } n \\text{ gerade} \\\\
+    n+1 & \\text{andernfalls.}
+\\end{cases}
+$$
+
+
+Darunter steht in leicht leuchtender Schrift:
+"
+
+namespace FunctionLvl7
+
+open Function
+
+def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+
+Statement "" : ¬ (f + f).Injective := by
+  unfold Injective
+  push_neg
+  use 2
+  use 3
+  simp
+
+Hint : ¬ (Injective (f + f)) =>
+"
+**Robo**: Das ist sicher ein Hinweis.
+
+**Du**: Aber `¬ Injective` sagt mir nichts…
+
+**Robo**: Könntest du etwas mit `¬ ∀` anfangen? Dann könntest du ja `Injektive` zuerst öffnen.
+
+**Du**: Darüber haben wir doch mal was gelernt…
+"
+
+HiddenHint : ¬ (Injective (f + f)) =>
+"
+**Robo**: Das war `push_neg`.
+"
+
+Hint : ∃ a b, (f + f) a = (f + f) b ∧ a ≠ b =>
+"**Du** Jetzt muss ich einfach ein Gegenbeispiel nennen, oder?
+
+**Robo** Genau! Welche beiden Zahlen möchtest du denn verwenden?"
+
+Conclusion
+"
+Als ihr das Problem gelöst habt, erschleicht euch ein starkes
+Gefühl, dass dies der falsche Weg ist.
+Also geht ihr zurück und nehmt die rechte Gabelung.
+"
+
+end FunctionLvl7

server/adam/Adam/Levels/Function/L07_Surjective.lean

@@ -0,0 +1,37 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 7
+
+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:
+"
+
+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/adam/Adam/Levels/Function/L08_Bijective.lean

@@ -0,0 +1,38 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 8
+
+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:
+"
+
+open Function
+
+Statement "" : Bijective (fun (n : ℤ) ↦ n + 1) := by
+  unfold Bijective
+  constructor
+  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 draußen."
+
+NewDefinition Bijective

server/adam/Adam/Levels/Function/L09_Inverse.lean

@@ -0,0 +1,61 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Function"
+Level 9
+
+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
+
+--TODO: This is a really hard proof
+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 der Bibliothek.
+
+**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
+
+**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"

server/adam/Adam/Levels/Function/L11_Inverse.lean

@@ -0,0 +1,93 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+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
+set_option pp.rawOnError true
+Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
+    Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
+  Branch
+    exfalso
+    Hint "Das war eine blöde Idee
+    dd
+
+    ddds
+    "
+  Hint (hidden := true) "constructor"
+  constructor
+  Hint "intro h" -- does not show
+  intro h
+  Hint "rcases h with ⟨h₁, h₂⟩" -- shows too late: 1, 2 after
+  rcases h with ⟨h₁, h₂⟩
+  Hint (strict := true) "let g := fun x => (h₂ x).choose" -- shows correct + 1 after
+  let g := fun x => (h₂ x).choose
+  Hint "use g"
+  use g
+  Hint "constructor" -- does not show
+  constructor
+  Hint "intro x" -- does not show
+  intro x
+  Hint "simp" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
+  simp
+  Hint "apply h₁"
+  apply h₁
+  Hint "apply Exists.choose_spec (h₂ (f x))"
+  apply Exists.choose_spec (h₂ (f x))
+  Hint "intro y" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
+  intro y
+  Hint "simp"
+  simp
+  Hint "apply Exists.choose_spec (h₂ y)"
+  apply Exists.choose_spec (h₂ y)
+  Hint "intro ⟨g, h₁, h₂⟩"
+  intro ⟨g, h₁, h₂⟩
+  Hint "constructor"
+  constructor
+  Hint "intro a b hab"
+  intro a b hab
+  Hint (strict := true) "have h : g (f a) = g (f b)"
+  have h : g (f a) = g (f b)
+  Hint "apply congrArg"
+  apply congrArg
+  Hint "assumption"
+  assumption
+  Hint "rw [h₁, h₁] at h"
+  rw [h₁, h₁] at h
+  Hint "assumption"
+  assumption
+  Hint "intro x"
+  intro x
+  Hint "use g x"
+  use g x
+  Hint "rw [h₂]"
+  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) (h : Bijective f) :
+  (∃ g, LeftInverse g f ∧ RightInverse g f) → Bijective f =>
+  "Test"
+
+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/adam/Adam/Levels/Implication.lean

@@ -0,0 +1,34 @@
+import Adam.Levels.Implication.L01_Intro
+import Adam.Levels.Implication.L02_Revert
+import Adam.Levels.Implication.L03_Apply
+import Adam.Levels.Implication.L04_Apply
+import Adam.Levels.Implication.L05_Apply
+import Adam.Levels.Implication.L06_Iff
+import Adam.Levels.Implication.L07_Rw
+import Adam.Levels.Implication.L08_Iff
+import Adam.Levels.Implication.L09_Iff
+import Adam.Levels.Implication.L10_Apply
+import Adam.Levels.Implication.L11_ByCases
+import Adam.Levels.Implication.L12_Rw
+import Adam.Levels.Implication.L13_Summary
+
+Game "Adam"
+World "Implication"
+Title "Aussagenlogik 2"
+
+Introduction
+"
+Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die ebenfalls
+beide bewohnt zu sein scheinen.
+
+**Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen,
+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…
+
+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 quer.
+
+Das Operationsteam begrüsst euch freundlich und lädt zum Essen im Kommandoturm.
+"

server/adam/Adam/Levels/Implication/L01_Intro.lean

@@ -0,0 +1,34 @@
+import Adam.Metadata
+import Mathlib.Tactic.Tauto
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 1
+
+Title "Intro"
+
+Introduction
+"
+**Operationsleiter**: Sagt mal, könnt ihr mir hier weiterhelfen?
+"
+
+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**: 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,
+  das kennen wir ja schon."
+  constructor
+  assumption
+  assumption
+
+Conclusion "Der Operationsleiter nickt bedacht."
+
+NewTactic intro
+DisabledTactic tauto

server/adam/Adam/Levels/Implication/L02_Revert.lean

@@ -0,0 +1,30 @@
+import Adam.Metadata
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 2
+
+Title "Revert"
+
+Introduction
+"Jemand aus der Gruppe gibt dir ein Blatt Papier mit einer Zeile Text:"
+
+Statement (A B : Prop) (ha : A) (h : A → B) : B := by
+  Hint "**Robo**: Mit `revert {ha}` kann man die Annahme `ha` als
+  Implikationsprämisse vorne ans Goal anhängen, dann ist das Goal `{A} → {B}`.
+
+  **Du**: Das wirkt etwas unnatürlich.
+
+  **Robo**: Schon, ja. Aber als Tool kann das manchmal nützlich sein."
+  revert ha
+  assumption
+
+Conclusion "**Du**: Aber das müsste doch auch anders gehen, ich hätte jetzt intuitiv
+die Implikation $A \\Rightarrow B$ angewendet und behauptet, dass es genügt $A$ zu zeigen…
+
+Daraufhin lächelt der Fragende nur vorahnend."
+
+NewTactic revert
+DisabledTactic tauto

server/adam/Adam/Levels/Implication/L03_Apply.lean

@@ -0,0 +1,35 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Implication"
+Level 3
+
+Title "Apply"
+
+Introduction
+"
+Sein Kollege zieht eine Linie unter deinen Beweis, schreibt ein durchgestrichenes ~`revert`~
+hin und gibt dir das Blatt wieder.
+"
+
+Statement (A B : Prop) (hA : A) (h : A → B) : B := by
+  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."
+  assumption
+
+Conclusion "**Robo** Übrigens mit `apply LEMMA` kannst auch jedes Lemma anwenden, dessen
+Aussage mit dem Goal übereinstimmt.
+
+Die beiden Fragenden schauen das Blatt an und murmeln zustimmend."
+
+NewTactic apply
+DisabledTactic revert tauto
+
+-- Katex notes
+-- `\\(    \\)` or `$   $` for inline
+-- and `$$  $$` block.
+-- align block:
+-- $$\\begin{aligned} 2x - 4 &= 6 \\\\ 2x &= 10 \\\\ x &= 5 \\end{aligned}$$

server/adam/Adam/Levels/Implication/L04_Apply.lean

@@ -0,0 +1,38 @@
+import Adam.Metadata
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 4
+
+Title "Implikation"
+
+Introduction
+"
+**Du** *(zu Robo)*: Testen die uns eigentlich hier?
+
+Ein älteres Gruppenmitglied schiebt ein Tablet über den Tisch und beginnt in leiser
+Stimme zu erklären.
+
+**Mitarbeiterin**: Eines unserer Kontrollelemente ist kaputt und ist verwirrt, wo Sachen hinkommen.
+Gesteuert werden diese über Panels, und hier hab ich das Übungspanel, mit dem wir neue
+Ingeneure ausbilden:
+"
+
+Statement (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+  Hint "**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
+  kombinieren?
+
+  **Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch."
+  intro hA
+  Hint (hidden := true) "**Robo**: Das ist wieder eine Anwendung von `apply`."
+  apply g
+  apply f
+  assumption
+
+Conclusion "**Du**: Ich hab das Konzept verstanden.
+
+Die Mitarbeiterin ist zufrieden und wünscht euch Glück auf der Mission."
+
+DisabledTactic tauto

server/adam/Adam/Levels/Implication/L05_Apply.lean

@@ -0,0 +1,53 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Implication"
+Level 5
+
+Title "Implikation"
+
+Introduction
+"
+Selbstsicher folgt ihr den Anweisungen und geht nach draußen zum
+defekten Kontrollelement. Dieses zeigt ein kompliziertes Diagram:
+$$
+\\begin{CD}
+  A  @>{f}>> B       @<{g}<< C       \\\\
+  @. @V{h}VV @V{m}VV \\\\
+  D  @>{i}>> E       @>{k}>> F       \\\\
+  @A{m}AA @A{n}AA @V{p}VV \\\\
+  G  @<{q}<< H       @>{r}>> I
+\\end{CD}
+$$
+"
+
+Statement
+    (A B C D E F G H I : Prop)
+    (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+    (n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
+  Hint "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
+
+  **Robo**: Und dann fängst du am besten wieder mit `intro` an."
+  intro ha
+  Branch
+    apply r
+    Hint "**Robo**: Das sieht nach einer Sackgasse aus…"
+  Hint (hidden := true) "**Robo**: Na wieder `apply`, was sonst."
+  apply p
+  apply k
+  apply h
+  Branch
+    apply g
+    Hint "**Robo**: Nah, da stimmt doch was nicht…"
+  apply f
+  assumption
+
+Conclusion
+"Mit einem lauten Ratteln springen die Förderbänder wieder an.
+
+**Operationsleiter**: Vielen Dank euch! Kommt ich geb euch eine Führung und stell euch den
+Technikern hier vor."
+
+DisabledTactic tauto
+
+-- https://www.jmilne.org/not/Mamscd.pdf

server/adam/Adam/Levels/Implication/L06_Iff.lean

@@ -0,0 +1,46 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Implication"
+Level 6
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Als erstes kommt ihr in einen kleinen Raum mit ganz vielen Bildschirmen.
+
+Ein junges Wesen dreht sich auf dem Stuhl um, und sagt:
+
+**Mitarbeiter**: Oh hallo! Schaut euch mal das hier an!
+"
+
+Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
+  Hint "**Robo**: Das ist ein genau-dann-wenn Pfeil: `\\iff`. Er besteht aus zwei Teilen:
+  `A ↔ B` ist als `⟨A → B, B → A⟩` definiert.
+
+  **Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
+
+  **Robo**: Genau. Entsprechend kannst du hier auch mit `constructor` anfangen."
+  constructor
+  Hint "**Du**: Ah und die beiden hab ich schon in den Annahmen."
+  assumption
+  assumption
+
+Conclusion
+"
+**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheissen,
+hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`.
+
+**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
+
+**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\" weil's die Rückrichtung ist.
+"
+
+NewTactic constructor
+DisabledTactic tauto rw
+
+-- TODO : `case mpr =>` ist mathematisch noch sinnvoll.

server/adam/Adam/Levels/Implication/L07_Rw.lean

@@ -0,0 +1,47 @@
+import Adam.Metadata
+
+import Init.Data.ToString
+-- #check List UInt8
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 7
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Als nächstes begenet ihr jemandem im Flur.
+
+Dieser hat schon von euch gehört und will sofort wissen, ob ihr ihm helfen könnt:
+"
+
+Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
+  Hint "**Du**: $B \\iff A \\iff D \\iff C$, die sind doch alle äquivalent…
+
+  **Robo**: Ja aber du musst ihm helfen umzuschreiben. Mit `rw [h₁]` kannst du `C` durch `D`
+  ersetzen."
+  rw [h₁]
+  Hint "**Du** Und wenn ich in die andere Richtung umschreiben möchte?
+
+  **Robo**: Dann schreibst du ein `←` vor den Namen, also `rw [← hₓ]`."
+  Branch
+    rw [← h₃]
+    Hint "**Du**: Ehm, das ist verkehrt.
+
+    **Robo**: Andersrum wär's besser gewesen, aber wenn du jetzt einfach weitermachst bis du
+    sowas wie `A ↔ A` kriegst, kann `rfl` das beweisen.
+
+    **Robo: Da fällt mir ein, `rw` versucht automatisch `rfl` am Ende. Das heisst, du musst
+    das nicht einmal mehr schreiben."
+    rw [h₂]
+  rw [←h₂]
+  assumption
+
+Conclusion "Ihr geht weiter und der Operationsleiter zeigt euch die Küche."
+
+NewTactic rw assumption
+DisabledTactic tauto
+-- NewLemma Iff.symm

server/adam/Adam/Levels/Implication/L08_Iff.lean

@@ -0,0 +1,44 @@
+import Adam.Metadata
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 8
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Der Koch kommt erfreut hinter einem grossen Topf hervor.
+
+**Koch**: Sagt mal, gestern hat mir jemand was erzählt und es will einfach nicht aus
+meinem Kopf…
+"
+
+Statement (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+  Hint "**Du**: Naja ich kann wohl immerhin mal mit `intro` anfangen und annehmen,
+  dass `{A}` wahr sei…
+
+  **Robo**: und dann schauen wir weiter!"
+  intro hA
+  Hint "**Robo**: Also eine Implikation wendet man mit apply an…
+
+  **Du**: Weiss ich ja!"
+  apply g
+  Hint "**Robo**: …und du kannst die Implikation `{A} → {B}` genau gleich mit
+  `apply {h}.mp` anwenden.
+
+  **Du**: Aber ich könnte hier auch `rw [← h]` sagen, oder?
+
+  **Robo**: Klar, aber offenbar versteht der Koch das `rw` nicht.
+  "
+  apply h.mp
+  assumption
+
+Conclusion "**Koch**: Danke vielmals! Jetzt muss ich aber schauen dass die Suppe nicht verkocht!
+
+Und er eilt davon."
+
+NewTactic apply assumption
+DisabledTactic tauto rw

server/adam/Adam/Levels/Implication/L09_Iff.lean

@@ -0,0 +1,53 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+
+Game "Adam"
+World "Implication"
+Level 9
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Noch während der Koch wieder zu seiner Suppe geht, kommt sein erster Gehilfe hervor.
+
+**Gehilfe**: Ich hab gestern noch was anderes gehört, könnt ihr mir da auch helfen?
+Aber ich versteh nicht ganz was ihr meinem Chef erklärt habt.
+"
+
+Statement (A B : Prop) : (A ↔ B) → (A → B) := by
+  Hint "**Du**: Hmm, mindestens mit der Implikation kann ich anfangen."
+  Hint (hidden := true) "**Robo**: Genau, das war `intro`."
+  intro h
+  Hint "**Du**: Also ich kenn `rw [h]` und `apply h.mp`, aber das will er wohl nicht hören.
+
+  **Robo**: Was du machen könntest ist mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
+  Teile aufteilen."
+  Branch
+    intro a
+    Hint "**Robo**: Hier müsstest du jetzt `rw [←h]` oder `apply h.mp` benützen, aber der
+    Gehilfe will, dass du zwingend eine dritte Variante benützt. Geh doch einen
+    Schritt zurück so dass das Goal `A → B` ist."
+  rcases h with ⟨mp, mpr⟩
+  Hint (hidden := true) "**Du**: Ah und jetzt ist das Resultat in den Annahmen."
+  assumption
+
+Conclusion
+"
+**Gehilfe**: Ah danke! Und jetzt versteh ich auch die Zusammenhänge!
+"
+OnlyTactic intro rcases assumption
+DisabledTactic rw apply tauto
+
+-- -- TODO: The new `cases` works differntly. There is also `cases'`
+-- example (A B : Prop) : (A ↔ B) → (A → B) := by
+--   intro h
+--   cases h with
+--   | intro a b =>
+--     assumption
+
+-- example (A B : Prop) : (A ↔ B) → (A → B) := by
+--   intro h
+--   cases' h with a b
+--   assumption

server/adam/Adam/Levels/Implication/L10_Apply.lean

@@ -0,0 +1,49 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib
+
+Game "Adam"
+World "Implication"
+Level 10
+
+Title "Lemmas"
+
+Introduction
+"
+Ihr setzt euch hin und der Gehilfe bringt euch allen Suppe. Neben euch sitzt eine Mechanikerin
+über ihre Suppe geneigt.
+
+**Mechanikerin**: Sagt mal, ich hab unten über folgendes tiefgründiges Problem nachgedacht:
+"
+
+Statement (A : Prop) : ¬A ∨ A := by
+  Hint "**Du**: Das scheint ziemlich offensichtlich.
+
+  **Robo**: Ich glaube, sie will eine detailierte Antwort. Ich kenne ein Lemma
+  `not_or_of_imp`, was sagt `(A → B) → ¬ A ∨ B`. Da das Resultat des Lemmas mit
+  deinem Goal übreinstimmt, kannst du es mit `apply not_or_of_imp` anwenden."
+  Branch
+    right
+    Hint "**Du**: Und jetzt?
+
+    **Robo**: `right/left` funktioniert hier nicht, da du nicht weisst ob `A` wahr oder falsch
+    ist."
+  Branch
+    left
+    Hint "**Du**: Und jetzt?
+
+    **Robo**: `right/left` funktioniert hier nicht, da du nicht weisst ob `A` wahr oder falsch
+    ist."
+  apply not_or_of_imp
+  Hint (hidden := true) "**Robo**: Ich würd wieder mit `intro` weitermachen."
+  intro
+  assumption
+
+Conclusion
+"
+**Mechanikerin**: Danke vielmals, jetzt bin ich schon viel ruhiger.
+"
+
+NewLemma not_or_of_imp
+DisabledTactic tauto

server/adam/Adam/Levels/Implication/L11_ByCases.lean

@@ -0,0 +1,38 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib
+
+Game "Adam"
+World "Implication"
+Level 11
+
+Title "by_cases"
+
+Introduction
+"
+**Du**: Sagt mal, hätte ich da nicht auch einfach zwei Fälle anschauen können:
+Wenn `A` wahr ist, beweis ich die rechte Seite, sonst die Linke.
+
+**Robo**: Tatsächlich, `by_cases h : A` würde genau das machen!
+"
+
+Statement (A : Prop) : ¬A ∨ A := by
+  Hint (hidden := true) "**Du**: Wie?
+
+  **Robo**: Also `by_cases h : A` erstellt zwei Goals. Im ersten hast Du `(h : A)` zur
+  Verfügung, im zweiten `(h : ¬ A)`."
+  by_cases h : A
+  Hint "**Du**: "
+  right
+  assumption
+  left
+  assumption
+
+Conclusion
+"
+**Du**: Das kann noch ganz nützlich sein.
+"
+
+NewTactic by_cases
+DisabledTactic tauto

server/adam/Adam/Levels/Implication/L12_Rw.lean

@@ -0,0 +1,50 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib.Logic.Basic
+
+Game "Adam"
+World "Implication"
+Level 12
+
+Title "Lemmas"
+
+Introduction
+"
+Der Arbeitskollegin der Mechanikerin, der die ganze Zeit gespannt zugehört hat, dreht sich zu
+euch.
+
+Er ist offensichtlich interessiert and existierenden Resultaten zu sein, aber offenbar
+kann er nicht viel mit `apply` anfangen.
+
+Er hat aber folgendes Resultat bereit:
+
+```
+lemma not_not (A : Prop) : ¬¬A ↔ A
+```
+
+und stellt euch folgende Frage:
+"
+
+Statement (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
+  Hint "**Robo**: Ein Lemma, das wie `not_not` ein `↔` oder `=` im Statement hat, kann
+  auch mit `rw [not_not]` verwendet werden."
+  rw [not_not]
+  Hint "**Du**: Häh, wieso hat das jetzt 2 von 3 der `¬¬` umgeschrieben?
+
+  **Robo**: `rw` schreibt nur das erste um, das es findet, also `¬¬C`. Aber weil dieses
+  mehrmals vorkommt, werden die alle ersetzt…
+
+  **Du**: Ah, und `¬¬B` ist was anderes, also brauch ich das Lemma nochmals."
+  rw [not_not]
+
+Conclusion
+"
+**Du**: Ah und wir sind fertig…?
+
+**Robo**: Ja, `rw` versucht immer anschliessend `rfl` aufzurufen, und das hat hier
+funktioniert.
+"
+
+DisabledTactic tauto apply
+NewLemma not_not

server/adam/Adam/Levels/Implication/L13_Summary.lean

@@ -0,0 +1,77 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 13
+
+Title "Zusammenfassung"
+
+Introduction
+"
+**Operationsleiter**: Damit endet unsere Führung langsam. Bevor ihr weitergeht
+habe ich noch ein Problem, an dem ich mir die Zähne ausbeisse. Wir haben die
+Herleitung eines unserer Programme `imp_iff_not_or` verloren, und wissen nicht mehr
+ob es einwandfrei funktioniert.
+
+**Du**: Nah gut, mal sehen. Robo, was hab ich denn alles hier gelernt?
+
+**Robo**: Hier ist die Übersicht:
+
+## Notationen / Begriffe
+
+|               | Beschreibung                                             |
+|:--------------|:---------------------------------------------------------|
+| →             | Eine Implikation.                                        |
+| ↔             | Genau-dann-wenn / Äquivalenz.                            |
+
+## Taktiken
+
+|     | Taktik                    | Beispiel                                               |
+|:----|:--------------------------|:-------------------------------------------------------|
+| 8   | `intro`                   | Für eine Implikation im Goal.                          |
+| 9   | `revert`                  | Umkehrung von `intro`.                                 |
+| 10  | `apply`                   | Wendet eine Implikation auf das Goal an.               |
+| 10ᵇ | `apply`                   | Wendet ein Lemma an.                                   |
+| 11  | `by_cases`                | Fallunterscheidung `P` und `¬P`                        |
+| 12  | `rw`                      | Umschreiben zweier äquivalenter Aussagen.              |
+| 12ᵇ | `rw`                      | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
+"
+
+Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
+  constructor
+  Hint "**Du**: Das sieht kompliziert aus…
+
+  **Robo** *(flüsternd)*: Ja, aber die Richtung kennst du ja schon also Lemma,
+  wend doch einfach das an."
+  apply not_or_of_imp
+  Hint "**Du**: Gibt es für die Gegenrichtung auch ein Lemma?
+
+  **Robo**: Leider nicht. Da musst du manuell ran."
+  Hint (hidden := true) "**Robo**: Na Implikationen fangst du immer mit `intro` an."
+  intro h
+  intro ha
+  Hint (hidden := true) "**Robo**: Ich wür mal die Annahme `h` mit `rcases` aufteilen."
+  rcases h with h | h
+  contradiction
+  assumption
+
+DisabledTactic tauto
+
+Conclusion "**Operationsleiter**: Damit gehen unsere Wege auseinander. Da fällt mir ein, seit
+ihr auf dem Weg zu unserem Schwestermond?
+
+**Du**: Könnten wir sein…
+
+**Operationsleiter**: Ich hab hier einen Brief für *Evenine*, könntet ihr diesen mit euch führen?
+
+**Du**: Klar! Robo, halt den mal.
+
+Robo nimmt den Brief und lässt ihn irgendwo in seinem Innern verschwinden. Dabei bemerkt er
+den besorgten Blick des Operationsleiters.
+
+**Robo**: Keine Angst, ich verdaue nichts!"

server/adam/Adam/Levels/Induction.lean

@@ -0,0 +1,5 @@
+import Adam.Levels.Induction.L01_Induction
+
+Game "Adam"
+World "Induction"
+Title "Übungen Induktions"

server/adam/Adam/Levels/Induction/L01_Induction.lean

@@ -0,0 +1,37 @@
+import Adam.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Induction"
+Level 1
+
+Title "Induktion"
+
+Introduction
+"
+Dieses Kapitel enthält noch ein paar Übungen zur Induktion.
+"
+
+Statement
+"Zeige dass $5^n + 7$ durch $4$ teilbar ist."
+    (n : ℕ) : 4 ∣ 5^n + 7 := by
+  induction n
+  simp
+  rcases n_ih
+  rw [Nat.pow_succ, Nat.mul_succ, add_assoc, h, mul_comm, ←mul_add]
+  simp
+
+--NewLemma Nat.pow_succ, Nat.mul_succ, add_assoc, mul_comm, ←mul_add
+
+-- example (n : ℕ) : Even (n^2 + n) := by
+--   induction n
+--   simp
+--   rw [Nat.succ_eq_add_one]
+--   rcases n_ih with ⟨x, h⟩
+--   use x + n_1 + 1
+--   ring_nf at *
+--   rw [←h]
+--   ring

server/adam/Adam/Levels/Inequality.lean

@@ -0,0 +1,16 @@
+import Adam.Levels.Inequality.L01_LE
+import Adam.Levels.Inequality.L02_Pos
+import Adam.Levels.Inequality.L03_Linarith
+import Adam.Levels.Inequality.L04_Linarith
+
+Game "Adam"
+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.
+"

server/adam/Adam/Levels/Inequality/L01_LE.lean

@@ -0,0 +1,34 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Inequality"
+Level 1
+
+Title "Kleinergleich"
+
+Introduction
+"
+*(Gesrpäch)*
+
+**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…
+
+**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
+  (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, könnt ihr mir ein bisschen mehr
+erzählen?"

server/adam/Adam/Levels/Inequality/L02_Pos.lean

@@ -0,0 +1,53 @@
+import Adam.Metadata
+
+import Mathlib.Tactic.LibrarySearch
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Inequality"
+Level 2
+
+Title "Kleinergleich"
+
+Introduction
+"
+*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 (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
+
+Conclusion "**Du**: Oh `simp` ist ja echt nicht schlecht…
+
+Die andere Person scheint beeindruckt, hat aber gleichzeitig auch das Bedürfnis, Dich aus
+der Reserve zu locken."

server/adam/Adam/Levels/Inequality/L03_Linarith.lean

@@ -0,0 +1,26 @@
+import Adam.Metadata
+import Mathlib.Tactic.Linarith
+
+Game "Adam"
+World "Inequality"
+Level 3
+
+Title "Linarith"
+
+Introduction
+"
+**dritte Person**: Nah wenn wir so spielen:
+"
+
+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."

server/adam/Adam/Levels/Inequality/L04_Linarith.lean

@@ -0,0 +1,29 @@
+import Adam.Metadata
+import Mathlib.Tactic.Linarith
+
+Game "Adam"
+World "Inequality"
+Level 4
+
+Title "Linarith"
+
+Introduction
+"
+**Robo**: Die Taktik kann aber noch viel mehr.
+
+**weitere Person**: Hier, probier mal!
+
+$$
+\\begin{aligned}
+  5 * y &\\le 35 - 2 * x \\\\
+  2 * y &\\le x + 3
+\\end{aligned}
+$$
+"
+
+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…"

server/adam/Adam/Levels/Inequality/T_Induction.lean

@@ -0,0 +1,41 @@
+import Adam.Metadata
+
+import Mathlib
+
+Game "Adam"
+World "Inequality"
+Level 1
+
+Title "Induktion"
+
+set_option tactic.hygienic false
+
+
+Introduction
+"
+Hier lernst du Induktion und Ungleichungen kennen. Beides essenziele Grundlagen, die du
+für spätere Aufgaben brauchst.
+
+Die Leantaktik `induction n` führt einen Induktionsbeweis über `(n : ℕ)`. Hier zuerst
+ein abstraktes Beispiel.
+"
+
+Statement
+"Sei $P(n)$ eine logische Aussage über die natürliche Zahl.
+Agenommen $P(0)$ ist wahr und $P(m) \\Rightarrow P(m+1)$ für alle $m$,
+dann gilt $P(n)$ für alle $n \\in \\mathbb{N}.$"
+    (n : ℕ) (P : ℕ → Prop) (h_base : P 0) (h_step : ∀ m, P m → P m.succ) : P n := by
+  induction n
+  assumption
+  apply h_step
+  assumption
+
+Hint (P : ℕ → Prop) : P Nat.zero =>
+"Das ist die Induktionsverankerung, hier musst du $P(0)$ zeigen."
+
+Hint (P : ℕ → Prop) (m : ℕ) (hi : P m) : P (Nat.succ m) =>
+"An der Stelle kommt der Beweis $P(m) \\Rightarrow P(m+1)$.
+
+In diesem Beispiel kannst du `apply` benützen."
+
+NewTactic induction

server/adam/Adam/Levels/Lean.lean

@@ -0,0 +1,26 @@
+import Adam.Levels.Lean.L01_Type
+import Adam.Levels.Lean.L02_Universe
+import Adam.Levels.Lean.L03_ImplicitArguments
+import Adam.Levels.Lean.L04_InstanceArguments
+
+Game "Adam"
+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!"

server/adam/Adam/Levels/Lean/L01_Type.lean

@@ -0,0 +1,41 @@
+import Adam.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "Adam"
+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."

server/adam/Adam/Levels/Lean/L02_Universe.lean

@@ -0,0 +1,44 @@
+import Adam.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "Adam"
+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 =>
+-- ""

server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean

@@ -0,0 +1,71 @@
+import Adam.Metadata
+
+import Mathlib
+import Adam.ToBePorted
+
+set_option tactic.hygienic false
+
+Game "Adam"
+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."

server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean

@@ -0,0 +1,57 @@
+import Adam.Metadata
+
+import Mathlib
+import Adam.ToBePorted
+
+set_option tactic.hygienic false
+
+Game "Adam"
+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 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/adam/Adam/Levels/LeftOvers/L09_Or.lean

@@ -0,0 +1,70 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Implication"
+Level 9
+
+Title "Oder"
+
+Introduction
+"
+Übung macht den Meister... Benutze alle vier Methoden mit UND und ODER
+umzugehen um folgende Aussage zu beweisen.
+
+|         | Und                      | Oder                      |
+|---------|:-------------------------|:--------------------------|
+| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h₁ \\| h₂` |
+| Goal    | `constructor`            | `left`/`right`            |
+"
+
+Statement and_or_imp
+    "Angenommen $(A \\land B) \\lor (A \\Rightarrow C)$ und $A$ sind wahr, zeige dass
+    $B \\lor (C \\land A)$ wahr ist."
+    (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
+  rcases h with h₁ | h₂
+  left
+  rcases h₁ with ⟨x, y⟩
+  assumption
+  right
+  constructor
+  apply h₂
+  assumption
+  assumption
+
+HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) =>
+"Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`."
+
+-- If starting with `left`.
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : B =>
+"Da kommst du nicht mehr weiter..."
+
+-- If starting with `right`.
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : (C ∧ A) =>
+"Da kommst du nicht mehr weiter..."
+
+HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
+"`left` oder `right`?"
+
+HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B) (hA : A) : B ∨ (C ∧ A) =>
+"`left` oder `right`?"
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
+"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen."
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B =>
+"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen."
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C =>
+"Sackgasse."
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
+"Hmmm..."
+
+Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
+"Ein UND im Goal kann mit `constructor` aufgeteilt werden."
+
+NewTactic left right assumption constructor rcases

server/adam/Adam/Levels/LeftOvers/L33_Prime.lean

@@ -0,0 +1,23 @@
+import Adam.Metadata
+import Mathlib.Tactic.Ring
+
+Game "Adam"
+World "Nat2"
+Level 3
+
+Title "Primzahlen"
+
+Introduction
+"
+TODO: Primzahl
+
+"
+
+Statement "" : True := by
+  trivial
+
+Conclusion
+"
+"
+
+NewTactic ring

server/adam/Adam/Levels/LeftOvers/L34_ExistsUnique.lean

@@ -0,0 +1,23 @@
+import Adam.Metadata
+import Mathlib.Tactic.Ring
+
+Game "Adam"
+World "Nat2"
+Level 5
+
+Title "Exists unique"
+
+Introduction
+"
+TODO: Es existiert genau eine gerade Primzahl.
+
+"
+
+Statement "" : True := by
+  trivial
+
+Conclusion
+"
+"
+
+NewTactic ring

server/adam/Adam/Levels/LeftOvers/Lxx_Prime.lean

@@ -0,0 +1,61 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+def even (a : ℕ) : Prop := ∃ r, a = 2 * r
+def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1
+
+lemma not_odd {n : ℕ} : ¬ odd n ↔ even n := by sorry
+
+lemma not_even {n : ℕ} : ¬ even n ↔ odd n := by sorry
+
+lemma even_square (n : ℕ) : even n → even (n ^ 2) := by
+  intro ⟨x, hx⟩
+  unfold even at *
+  use 2 * x ^ 2
+  rw [hx]
+  ring
+
+def prime (n : ℕ) : Prop := (2 ≤ n) ∧ ∀ a b, n = a * b → a = 1 ∨ b = 1
+
+Game "Adam"
+World "Nat"
+Level 4
+
+Title "Für alle"
+
+Introduction
+"
+Eine Primzahl könnte man folgendermassen implementieren:
+```
+def prime (p : ℕ) : Prop := (2 ≤ p) ∧ (∀ a b, p = a * b → a = 1 ∨ b = 1)
+```
+Also, eine Zahl `p` ungleich `0` oder `1`, für die gilt wenn `a * b = p` dann ist
+entweder `a` oder `b` eins.
+
+(Tatsächlich ist eine Primzahl dann etwas genereller definiert, aber dazu mehr später.)
+
+
+
+
+"
+
+Statement
+  "Wenn `n * m` eine Primzahl ist, dann ist einer der beiden Faktoren eins."
+  (p n m : ℕ) (h : prime p) (h₂ : p = m * n) : n = 1 ∨ m = 1 := by
+  unfold prime at h
+  rcases h with ⟨l, r⟩
+  apply r
+  rw [h₂]
+  ring
+
+
+
+Hint (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) =>
+"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
+`(x : ℕ) → `"
+
+NewTactic ring intro unfold

server/adam/Adam/Levels/LeftOvers/Lxx_Tauto.lean

@@ -0,0 +1 @@
+-- tauto is not implemented yet... duper?

server/adam/Adam/Levels/LeftOvers/Lxx_Tfae.lean

@@ -0,0 +1 @@
+-- not implemented yet

server/adam/Adam/Levels/LeftOvers/Playground.lean

@@ -0,0 +1,18 @@
+import Adam.Metadata
+import Mathlib
+
+-- -- INCORPORATED
+-- example (A  B : Prop) : (A → B) ↔ (¬ B → ¬A) := by
+--   constructor
+--   intro h nb
+--   by_contra
+--   have : B
+--   apply h
+--   assumption
+--   contradiction
+--   intro h a
+--   by_contra
+--   have : ¬ A
+--   apply h
+--   assumption
+--   contradiction

server/adam/Adam/Levels/LeftOvers/xx_Functions.lean

@@ -0,0 +1,25 @@
+import Adam.Metadata
+import Mathlib.Tactic.Ring
+
+Game "Adam"
+World "Function"
+Level 1
+
+Title "Funktionen"
+
+Introduction
+"
+Funktionen werden in Lean als `(f : ℕ → ℕ)` geschrieben (`\\to`), also mit dem gleichen
+Pfeil wie Implikationen. Entsprechend kann man Implikationen und Funktionen genau
+gleich behandeln.
+
+"
+
+Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
+  let g := fun (x : ℕ) ↦ 0
+  use g
+  simp
+
+Conclusion ""
+
+NewTactic use simp

server/adam/Adam/Levels/LinearAlgebra.lean

@@ -0,0 +1,41 @@
+import Adam.Levels.LinearAlgebra.L01_Module
+import Adam.Levels.LinearAlgebra.L02_VectorNotation
+import Adam.Levels.LinearAlgebra.L03_VectorNotation
+import Adam.Levels.LinearAlgebra.L04_Submodule
+import Adam.Levels.LinearAlgebra.L05_Submodule
+import Adam.Levels.LinearAlgebra.L06_Span
+import Adam.Levels.LinearAlgebra.L07_Span
+import Adam.Levels.LinearAlgebra.L08_GeneratingSet
+
+import Adam.Levels.LinearAlgebra.M01_LinearMap
+import Adam.Levels.LinearAlgebra.M02_LinearIndep
+import Adam.Levels.LinearAlgebra.M04_Basis
+
+import Adam.Levels.LinearAlgebra.N01_Span
+import Adam.Levels.LinearAlgebra.N02_Span
+import Adam.Levels.LinearAlgebra.N03_Idempotent
+import Adam.Levels.LinearAlgebra.N04_Idempotent
+import Adam.Levels.LinearAlgebra.N05_Sum
+import Adam.Levels.LinearAlgebra.N06_Sum
+import Adam.Levels.LinearAlgebra.N07_Prod
+import Adam.Levels.LinearAlgebra.N08_Prod
+import Adam.Levels.LinearAlgebra.N09_Prod
+
+Game "Adam"
+World "Module"
+Title "Vektorraum"
+
+Introduction "Hier lernst du die Grundlagen zur linearen Algebra.
+
+Vektorräume sind in Lean etwas algemeiner definiert als dies normalerweise in
+einer Einführungsvorlesung antrifft: Man definiert ein \"Modul\" (Plural: Moduln)
+über einem Ring. Ein Modul über einem *Körper* wird dann auch \"Vektorraum\" genannt.
+"
+
+Game "Adam"
+World "Basis"
+Title "Lineare Abbildungen"
+
+Game "Adam"
+World "Module2"
+Title "Mehr Vektorräume"

server/adam/Adam/Levels/LinearAlgebra/L01_Module.lean

@@ -0,0 +1,106 @@
+import Adam.Metadata
+
+import Mathlib.Data.Real.Basic      -- definiert `ℝ`
+import Mathlib.Algebra.Module.Basic -- definiert `module`
+import Mathlib.Tactic.LibrarySearch
+import Adam.StructInstWithHoles
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Module"
+Level 1
+
+Title "Module"
+
+Introduction
+"
+Konkret heisst das:
+
+Sei `R` ein Ring. Ein `R`-Modul ist eine kommutative Gruppe `(V, +)` zusammen mit
+einer Abbildung `• : R × V → V` (Skalarmultiplitation genannt), die folgende
+Eigenschaften beliebige `(r s : R)` und `(v w : V)`erfüllt:
+- `r • (v + w) = r • v + r • w`
+- `(r + s) • v = r • v + s • v`
+- `(r * s) • v = r • s • v`
+- `1 • r = r`
+- `0 • v = 0`
+- `r • 0 = 0`
+
+"
+
+-- Bemerkungen:
+-- 1) Über einem `[field R]` sind die letzten beiden Eigenschaften überflüssig, diese kann
+--    man beweisen, wenn man Cancellation (`a₁ + x = a₂ + x → a₁ = a₂`) hat. In einem generellen
+--    Ring, muss das aber nicht gegeben sein (siehe Nullteiler).
+-- 2) Die nötigen Annahmen um ein Modul in Lean zu erhalten sind tatsächlich noch etwas lockerer,
+--    so muss `R` nicht ganz ein Ring sein (nur `[Semiring R]`) und
+--    `V` muss nicht ganz eine kommutative Gruppe sein (nur `[add_comm_monoid V]`).
+-- Einen abstrakten Vektorraum definiert man wie folgt:
+-- `variables {R V : Type*} [field R] [add_comm_monoid V] [module R V]`
+
+-- Wenn man hingegen konkret zeigen will, dass ein existierendes Objekt ein Vektorraum ist,
+-- kann man eine einsprechende Instanz wie folgt definieren:
+
+-- ```
+-- instance Q_module : Module ℚ ℝ :=
+-- { smul := λa r, ↑a * r
+--   smul_zero := _
+--   zero_smul := _
+--   one_smul := _
+--   smul_add := _
+--   add_smul := _
+--   mul_smul := _ }
+-- ```
+-- Man muss also angeben, welche Skalarmultiplikation man gerne hätte
+-- (`smul`. In unserem Fall sagen wir einfach, diese soll Multiplikation in `ℝ` sein.)
+-- und dazu jegliche Beweise, dass die Skalarmultiplikation sich mit der Ringstruktur verträgt.
+-- Im nachfolgenden beweisen wir die Eigenschaften einzeln.
+
+Statement
+"Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
+    : Module ℚ ℝ := by
+  Hint "**Robo**: Als erstes willst du die Stuktur `Modul` aufteilen in einzelne Beweise.
+  Der Syntax dafür ist:
+
+  ```
+  refine \{ ?..! }
+  ```
+  "
+  refine { ?..! }
+  · Hint "**Robo**: Hier musst du die Skalarmultiplikation angeben.
+    Benutze dafür `exact fun (a : ℚ) (r : ℝ) => ↑a * r`."
+    exact fun (a : ℚ) (r : ℝ) => ↑a * r
+  · Hint "**Robo**: Jetzt musst du alle eigenschaften eines $\\mathbb\{Q}$-Moduls zeigen,
+    das sind also 6 einzelne Goals."
+    intro b
+    Hint "**Robo**: Mit `change (1 : ℚ) * {b} = {b}` kannst du das Goal umschreiben, damit
+    dann andere Taktiken besser damit arbeiten können."
+    change (1 : ℚ) * b = b
+    Hint "**Robo**: Den Teil kannst du mit `simp` beweisen."
+    simp
+  · intro x y b
+    Hint "**Robo**: Benutze `change` um `•` durch `*` zu ersetzen."
+    Hint (hidden := true) "**Robo**: Explizit `change ({x} * {y} : ℚ) * {b} = {x} * ({y} * {b})`"
+    change (x * y : ℚ) * b = x * (y * b)
+    Hint "**Robo**: Mit `simp` und `ring` kannst du den Rest beweisen."
+    simp
+    ring
+  · intro a
+    simp
+  · intro a x y
+    Hint (hidden := true) "**Robo**: Explizit `change {a} * ({x} + {y}) = {a} * {x} + {a} * {y}`"
+    change a * (x + y) = a * x + a * y
+    ring
+  · intro r s x
+    Hint (hidden := true) "**Robo**: Explizit
+    `change ({r} + {s} : ℚ) * {x} = {r} * {x} + {s} * {x}`"
+    change (r + s : ℚ) * x = r * x + s * x
+    simp
+    ring
+  · intro a
+    Hint (hidden := true) "**Robo**: Explizit `change (0 : ℚ) * {a} = 0`"
+    change (0 : ℚ) * a = 0
+    simp
+
+NewTactic refine exact change

server/adam/Adam/Levels/LinearAlgebra/L02_VectorNotation.lean

@@ -0,0 +1,59 @@
+import Adam.Metadata
+
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Algebra.Module.Pi          -- definiert `Module ℚ (fin 2 → ℚ)`
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Tactic.FinCases
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Module"
+Level 2
+
+Title "Konkrete Vektorräume"
+
+Introduction
+"
+Den $\\mathbb{Q}$-Vektorraum $\\mathbb{Q}^3$ definiert man am besten mit
+der lokalen Notation
+
+```
+local notation `ℚ³` := Fin 3 → ℚ
+```
+
+Dabei ist `Fin 3` die Indexmenge $\\{0, 1, 2\\}$.
+
+Die schreibweise für einen Vektor ist `![ _, _ ]`. Zu beachten ist,
+dass man bei Zahlen explizit einen Typ angeben muss, sonst denkt sich
+Lean, man arbeite über `ℕ`.
+
+Um direkt Vektoroperationen über `ℚ` auszurechnen, kann man oft
+`#eval` benützen:
+
+```
+#eval ![ (2 : ℚ), 5 ] + ![ 1/2, -7 ]
+```
+zeigt `![5/2, -2]` an.
+
+Um eine Gleichheit in einem Beweis zu verwenden, muss man andere Taktiken
+benützen.
+
+Am hilfreichsten ist die kombination `funext i, fin_cases i`, die
+Dann eine Vektorgleichung komponentenweise aufteilt.
+
+Für jede Komponente kann man dann mit `simp` und `ring` weiterkommen.
+"
+
+local notation "ℚ³" => Fin 3 → ℚ
+local notation "ℚ^(" n ")" => (Fin n) → ℚ
+
+Statement
+""
+    : ![ (2 : ℚ), 5 ] + ![ 1/2, -7 ] = ![5/2, -2] := by
+  funext i
+  fin_cases i <;>
+  simp <;>
+  ring
+
+NewTactic fin_cases funext

server/adam/Adam/Levels/LinearAlgebra/L03_VectorNotation.lean

@@ -0,0 +1,25 @@
+import Adam.Metadata
+
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Algebra.Module.Pi          -- definiert `Module ℚ (fin 2 → ℚ)`
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Tactic.FinCases
+
+Game "Adam"
+World "Module"
+Level 3
+
+Title "Konkrete Vektorräume"
+
+Introduction
+"
+Beachte dass Skalarmultiplikation mit `•` geschrieben wird, und nicht mit `*`!
+"
+
+Statement
+""
+    : 5 • ![ (2 : ℚ), 5 ] + ![ 1, 0 ] = ![11, 25] := by
+  funext i
+  fin_cases i <;>
+  simp <;>
+  ring

server/adam/Adam/Levels/LinearAlgebra/L04_Submodule.lean

@@ -0,0 +1,46 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+Game "Adam"
+World "Module"
+Level 4
+
+Title "Untervektorräume"
+
+Introduction
+"
+Sei `K` ein Körper und `V` ein `K`-Modul.
+
+```
+variable {K V : Type _} [Field K]
+variable [AddCommMonoid V] [Module K V]
+```
+
+Untermodule/Untervektorräume werden in Lean ein bisschen anders definiert als Module/Vektorräume.
+
+Grob gesagt ist `V` ein Typ (denke z.B. an eine generelle Menge)
+und `[module K V]` eine Instanz, die von Lean automatisc gefunden wird und
+sagt, dass auf `V` eine `K`-Modulstruktur existiert. Hingegen ist `submodule K V` die Menge aller
+Untermodulen
+in `V`. Deshalb definieren wir Untermodule, indem wir Elemente aus dieser Menge auswählen:
+
+```
+variable (U : Submodule K V)
+```
+
+Unter anderem hat dies den Vorteil, dass `submodule K V` eine Lattice ist, also eine `≤`-Operation
+besitzt. Auf dem Papier
+schreibt man normalerweise `U₁ ⊆ U₂` um zu sagen, dass das eine Untermodul eine Teilmenge des
+anderen ist, in Lean braucht
+man dafür immer `≤`.
+
+Ganz `V` als Untermodul von sich selbst betrachtet, schreibt man als `⊤` (`\\top`), also das
+grösste Element in dieser Lattice,
+und das Null-Untermodule `{0}` with als `⊥` geschrieben (`\\bot`), also das kleinste Element.
+"
+
+Statement
+"Jeder Untervektorraum `U ⊆ V` ist eine Teilmenge von `V`."
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (U : Submodule K V) : U ≤ ⊤ := by
+  simp only [le_top]

server/adam/Adam/Levels/LinearAlgebra/L05_Submodule.lean

@@ -0,0 +1,23 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+Game "Adam"
+World "Module"
+Level 5
+
+Title "Untervektorräume"
+
+Introduction
+"
+Elemente aus einem Untervektorraum $U$ wählt man gleich aus, wie Elemente in einer Menge.
+Nämlich man nimmt ein Element `(x : V)` und sagt, dass es in `U` liegt mit `x ∈ U` (`\\in`).
+"
+
+Statement
+"TODO: Spannendere Aufgaben."
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (U : Submodule K V) :
+    ∀ (x : V), x ∈ U ∨ x ∉ U := by
+  intro x
+  rw [or_iff_not_imp_left]
+  tauto

server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean

@@ -0,0 +1,39 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+
+Game "Adam"
+World "Module"
+Level 6
+
+Title "Hülle"
+
+Introduction
+"
+Ein typischer Untervektorraum ist die Hülle `⟨M⟩`, oder `span`, also die Menge aller
+`K`-Linearkombinationen von Elementen aus der Menge `M`.
+
+In Lean ist dies `Submodule.span K M`.
+
+"
+
+local notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule Set Finsupp
+
+Statement mem_span_of_mem
+  "Zeige, dass $x \\in M$ auch Element von der $K$-linearen Hülle
+  \\langle M \\rangle ist."
+    {V K : Type _} [Field K] [AddCommMonoid V]
+    [Module K V] (M : Set V) {x : V} (h : x ∈ M) :
+    x ∈ span K M := by
+  rw [mem_span]
+  intro p hp
+  specialize hp h
+  assumption

server/adam/Adam/Levels/LinearAlgebra/L07_Span.lean

@@ -0,0 +1,48 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+import Mathlib.Tactic.LibrarySearch
+import Mathlib
+
+Game "Adam"
+World "Module"
+Level 7
+
+Title "Hülle"
+
+Introduction
+"
+"
+
+-- notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule Set Finsupp
+
+open BigOperators -- Summen Notation
+
+-- TODO: Why is this not in Mathlib?
+lemma mem_span_of_mem {V K : Type _} [Field K] [AddCommMonoid V]
+    [Module K V] (M : Set V) {x : V} (h : x ∈ M) :
+    x ∈ span K M := by
+  rw [mem_span]
+  intro p hp
+  specialize hp h
+  assumption
+
+Statement
+  "Für $x, y \\in M$, zeige dass $x + 2y$ in der $K$-linearen Hülle $\\langle M \\rangle$ liegt."
+    {V K : Type _} [Field K] [AddCommMonoid V] [Module K V] (M : Set V) {x y : V}
+    (h₁ : x ∈ M) (h₂ : y ∈ M) :
+    x + (2 : K) • y ∈ span K M := by
+  apply add_mem
+  apply mem_span_of_mem
+  assumption
+  apply smul_mem
+  apply mem_span_of_mem
+  assumption

server/adam/Adam/Levels/LinearAlgebra/L08_GeneratingSet.lean

@@ -0,0 +1,43 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+
+Game "Adam"
+World "Module"
+Level 8
+
+Title "Erzeugendensystem"
+
+Introduction
+"
+Dass eine Familie von Vektoren `M` den ganzen Vektorraum
+aufspannt, sagt man in Lean mit `⊤ ≤ span K M`. (Man könnte auch `span K M = ⊤` schreiben,
+aber per Konvention wird `≤` bevorzugt, da `x ≤ ⊤` immer gilt (siehe `le_top`))
+"
+
+-- notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule Set Finsupp
+
+open BigOperators -- Summen Notation
+
+Statement
+  "Zeige, dass `![1, 0], ![1, 1]` den ganzen `ℝ`-Vektorraum `ℝ²` aufspannt."
+    : ⊤ ≤ span ℝ (Set.range ![(![1, 0] : Fin 2 → ℝ), ![1, 1]]) := by
+  --rw [top_le_span_range_iff_forall_exists_fun]
+  sorry
+  --   intro v,
+
+  --   use ![v 0 - v 1, v 1],
+  --   simp,
+  --   funext i,
+  --   fin_cases i;
+  --   simp,
+
+--NewLemma top_le_span_range_iff_forall_exists_fun le_top

server/adam/Adam/Levels/LinearAlgebra/M01_LinearMap.lean

@@ -0,0 +1,91 @@
+import Adam.Metadata
+
+import Mathlib.Data.Real.Basic           -- definiert `ℝ`
+import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ`
+import Mathlib.Tactic.FinCases
+import Mathlib.Data.Fin.VecNotation
+
+Game "Adam"
+World "Basis"
+Level 1
+
+notation "ℝ²" => Fin 2 → ℝ
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Sei `R` ein Ring und `V W` zwei `R`-Moduln. Eine `R`-lineare Abbildung wird in Lean
+folgendermassen geschrieben: `V →ₗ[R] W` (`\\to` + `\\_l`).
+
+Man erstellt eine lineare Abbildung aus einer Funktion `f : V → W` zusammen mit den beweisen,
+dass `f` Addition und Skalarmultiplikation erhält,
+i.e. `f (x + y) = f x + f y` und `f (r • x) = r • f x`.
+
+Hier definieren wir zum Beispiel die Null-Abbildung, die einfach alles auf `0` sendet:
+
+```
+variables {R V W : Type*} [ring R] [add_comm_monoid V] [add_comm_monoid W]
+[module R V] [module R W]
+
+def my_zero_map : V →ₗ[R] W :=
+  { to_fun := λ x, 0,
+    map_add' :=
+    begin
+      intros,
+      simp,
+    end,
+    map_smul' :=
+    begin
+      intros,
+      simp,
+    end }
+```
+
+"
+
+Statement
+"
+Zeige dass die Abbildung
+
+```
+  ℝ² → ℝ²
+  (x, y) ↦ (5x + 2y, x - y)
+```
+
+`ℝ`-linear ist.
+"
+    : ℝ² →ₗ[ℝ] ℝ² :=
+  { toFun := fun v ↦ ![5 * (v 1) + 2 * (v 2), (v 1) - (v 2)]
+    map_add' := by
+      -- Wähle zwei beliebige Vektoren mit `intros` aus.
+      intro x y
+      -- Das Lemma `funext` sagt das zwei Funktionen identisch sind, wenn sie für jeden Wert ereinstimmen:
+      -- `(∀ i, f i = g i) → f = g`. Da Vektoren einfach als Funktionen von einem Indexset codiert sind,
+      -- kannst du mit `apply funext` komponentenweise rechnen.
+      funext i
+      -- Mit `fin_cases i` kannst du pro möglichem Wert von `i` ein Goal auftun. D.h. im ersten gilt dann
+      -- `i = 0`, im zweiten Goal `i = 1`.
+      fin_cases i
+      -- Dies ist der Fall `i = 0`.
+        -- Das Goal hat jetzt Terme der Form `![a, b] 0`, und du weisst was das sein sollte, nämlich
+        -- einfach der erste Komponent `a`. Die Taktik `simp` ist für solche Vereinfachungnen gedacht.
+      · simp
+        -- Einfache Rechenaufgaben hast du ja bereits gemacht.
+        -- `ring` oder `linarith` machen dies automatisch für dich.
+        ring
+      -- Und jetzt noch den Fall `i = 1`.
+      · simp
+        ring
+    map_smul' := by
+      intro r x
+      funext i
+      fin_cases i
+        -- Bemerkung: Wenn du jetzt `simp` brauchst, macht es sogar noch mehr als vorher.
+        -- Skalarmultiplikation ist einfach als komponentenweise Multiplikation definiert.
+        -- Entsprechend braucht `simp` ein Lemma `smul_eq_mul : a • b = a * b`.
+      · simp
+        ring
+      · simp
+        ring
+  }

server/adam/Adam/Levels/LinearAlgebra/M02_LinearIndep.lean

@@ -0,0 +1,49 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic           -- definiert `ℝ`
+import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ`
+import Mathlib.Tactic.FinCases
+import Mathlib.Data.Fin.VecNotation
+-- import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.Algebra.BigOperators.Basic -- default
+-- import Mathlib.LinearAlgebra.LinearIndependent
+import Mathlib
+
+Game "Adam"
+World "Basis"
+Level 2
+
+Title "Lineare Unabhängigkeit"
+
+namespace Ex_LinIndep
+
+scoped notation "ℝ²" => Fin 2 → ℝ
+
+Introduction
+"
+"
+
+Statement
+"Zeige, dass `![1, 0], ![1, 1]` linear unabhängig über `ℝ` sind."
+    : LinearIndependent ℝ ![(![1, 0] : ℝ²), ![1, 1]] := by
+  Hint "`rw [Fintype.linearIndependent_iff]`"
+  rw [Fintype.linearIndependent_iff]
+  Hint "`intros c h`"
+  intros c h
+  Hint "BUG: `simp at h` does not work :("
+  simp at h -- doesn't work
+  sorry
+
+  -- rw [Fintype.linearIndependent_iff]
+  -- intros c h
+  -- simp at h
+  -- intros i
+  -- fin_cases i
+  -- swap
+  -- { exact h.2 }
+  -- { have h' := h.1
+  --   rw [h.2, add_zero] at h'
+  --   exact h'}
+
+end Ex_LinIndep

server/adam/Adam/Levels/LinearAlgebra/M04_Basis.lean

@@ -0,0 +1,32 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib
+
+Game "Adam"
+World "Basis"
+Level 4
+
+Title "Basis"
+
+namespace Ex_Basis
+
+scoped notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule
+
+Introduction
+"
+
+"
+
+lemma exercise1 : LinearIndependent ℝ ![(![1, 0] : ℝ²), ![1, 1]] := sorry
+
+lemma exercise2 :  ⊤ ≤ span ℝ (Set.range ![(![1, 0] : Fin 2 → ℝ), ![1, 1]]) := sorry
+
+Statement : Basis (Fin 2) ℝ ℝ² := by
+  apply Basis.mk
+  apply exercise1
+  apply exercise2
+
+end Ex_Basis

server/adam/Adam/Levels/LinearAlgebra/N01_Span.lean

@@ -0,0 +1,30 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+
+Game "Adam"
+World "Module2"
+Level 1
+
+open Submodule
+
+-- Verpackungswahn 1a)
+Title "Verpackungswahn"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (M : Set V) :
+    span K ↑(span K M) = span K M := by
+  apply Submodule.span_eq
+  -- or : simp

server/adam/Adam/Levels/LinearAlgebra/N02_Span.lean

@@ -0,0 +1,45 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+import Mathlib
+
+open Submodule
+
+Game "Adam"
+World "Module2"
+Level 2
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+  (Verpackungswahn)
+If `f` is a function and `M` a subset of its domain, then
+`f '' M` or `set.image f M` is the notation for the image, which is
+usally denoted `f(M) = {y | ∃ x ∈ M, f(x) = y}` in mathematical texts.
+"
+
+-- TODO: This is blocked by
+-- https://github.com/leanprover/lean4/issues/2074
+
+set_option autoImplicit false
+-- set_option pp.all true
+
+Statement
+"" : True := by
+  sorry
+
+-- example {K V W : Type} [Field K] [AddCommMonoid V] [AddCommMonoid W]
+--     [Module K V] [Module K W] (M : Set V) (f : V →ₗ[K] W) :
+--   f '' span K M = @span K (f '' M) := by
+--   sorry
+
+-- example {K V : Type} [Field K] [AddCommMonoid V]
+--     [Module K V] (M : Set V) (f : V →ₗ[K] V) : f '' M = f '' M =  := by
+--   rfl

server/adam/Adam/Levels/LinearAlgebra/N03_Idempotent.lean

@@ -0,0 +1,34 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Basic
+
+Game "Adam"
+World "Module2"
+Level 3
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    {R V : Type _} [Semiring R] [AddCommGroup V] [Module R V]
+    (p : V →ₗ[R] V) (h : p ∘ p = p) : LinearMap.ker p ⊔ LinearMap.range p = ⊤ := by
+  sorry
+  --   rw eq_top_iff,
+  -- intros v hv,
+
+  -- rw ←sub_add_cancel v (p v),
+
+  -- apply submodule.add_mem_sup,
+  -- { rw [linear_map.mem_ker],
+  --   rw [map_sub],
+  --   change p v - (p ∘ p) v = 0,  -- oder: rw [function.comp, function.funext_iff] at h,
+  --   rw h,
+  --   simp },
+  -- { simp }

server/adam/Adam/Levels/LinearAlgebra/N04_Idempotent.lean

@@ -0,0 +1,33 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Basic
+
+Game "Adam"
+World "Module2"
+Level 4
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    {R V : Type _} [Semiring R] [AddCommGroup V] [Module R V]
+    (p : V →ₗ[R] V)(h : p ∘ p = p) : LinearMap.ker p ⊓ LinearMap.range p = ⊥ := by
+  sorry
+  -- rw eq_bot_iff,
+  -- intros v hv,
+  -- rw submodule.mem_bot,
+  -- rw submodule.mem_inf at hv,
+  -- cases hv.2 with w hw,
+  -- rw ←hw,
+  -- rw ←h,
+  -- change p (p w) = _,
+  -- rw  hw,
+  -- rw ←linear_map.mem_ker,
+  -- exact hv.1,

server/adam/Adam/Levels/LinearAlgebra/N05_Sum.lean

@@ -0,0 +1,26 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.LinearAlgebra.Span
+
+open Submodule
+
+Game "Adam"
+World "Module2"
+Level 5
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Die interne Summe von Untermodulen wird in Lean mit `⊔` (`\\sup`) geschrieben.
+"
+
+Statement
+"
+Zeige, dass `V₁ ⊔ V₂` tatsächlich die interne Summe `⟨V₁ ∪ V₂⟩` ist.
+"
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (V₁ V₂ : Submodule K V) :
+    V₁ ⊔ V₂ = span K ( (V₁ : Set V) ∪ V₂ ) := by
+  rw [span_union]
+  simp

server/adam/Adam/Levels/LinearAlgebra/N06_Sum.lean

@@ -0,0 +1,25 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.LinearAlgebra.Span
+
+open Submodule
+
+Game "Adam"
+World "Module2"
+Level 6
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Eine interne Summe über eine Familie von Untermodulen `(T : ι → submodule K V)`
+wird als `⨆ (i : ι), T i` geschrieben (`\\supr`).
+"
+
+Statement
+""
+    {K V ι : Type _} [Field K] [AddCommMonoid V] [Module K V]
+    (T : ι → Submodule K V) : (⨆ (i : ι), T i) = span K ( ⋃ i, T i) := by
+  rw [Submodule.span_unionᵢ]
+  simp

server/adam/Adam/Levels/LinearAlgebra/N07_Prod.lean

@@ -0,0 +1,41 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Span
+
+Game "Adam"
+World "Module2"
+Level 7
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Die externe Summe von (Unter-) Modulen wird als `V × W` geschrieben
+Das Produkt zweier Module wird mit `×` geschrieben.
+
+Lean weiss dann automatisch, dass das Produkt wieder ein Vektorraum ist.
+-/
+example : module ℝ (ℝ × ℝ) := infer_instance
+
+/-
+Und `ℝ × ℝ` und `fin 2 → ℝ` sind natürlich Isomorph. In Praxis eignet sich
+die Funktionsschreibweise besser, deshalb verwenden wir diese als
+definition für `ℝ²`.
+
+Hier die Äquivalenz als generelle Typen:
+-/
+example : (fin 2 → ℝ) ≃ ℝ × ℝ  :=
+begin
+  apply pi_fin_two_equiv,
+end
+
+/-
+Äquivalenz als Vektorräume schreibt man als `ℝ`-lineare Äquivalenz `≃ₗ[ℝ]`.
+"
+
+Statement
+"Zeige dass das Produkt `ℝ × ℝ` und `ℝ²` isomorph sind als `ℝ`-Vektorräume."
+    : ((Fin 2) → ℝ) ≃ₗ[ℝ] ℝ × ℝ := by
+  sorry

server/adam/Adam/Levels/LinearAlgebra/N08_Prod.lean

@@ -0,0 +1,57 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Span
+
+universe u
+
+Game "Adam"
+World "Module2"
+Level 8
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Eine Familie von Vektorräumen schreibt man erst einmal als Funktion einer Indexmenge `ι`.
+-/
+
+variables {ι : Type u} {V : ι → Type u}
+
+/-
+Für einen einzelnen Vektorraum würde man jetzt Instanzen `[add_comm_monoid V] [module K V]`
+definieren. Lean-Instanzen-Manager versteht hier `∀`-Ausdrücke:
+-/
+
+variables [∀i, add_comm_monoid (V i)] [∀i, module K (V i)]
+
+/-
+Ein externes Produkt von Vektorräumen schreibt man einfach mit `\\Pi`, also `Π i, V i`.
+
+Lean kann aus den Ausdrücken oben dann automatisch herausfinden, dass `Π i, V i`
+ein `K`-Vektorraum ist:
+"
+
+Statement
+"Sei `U` ein `K`-Vektorraum und `fᵢ : U → Vᵢ` eine Familie von `K`-lineare Abbildungen
+in `K`-Vektorräume. Dann gibt es genau eine Abbildung `f : U → (Π i, V i)`, die mit
+allen kommutiert."
+    {K U : Type u} [Field K] {ι : Type u} {V : ι → Type u}
+    [∀ i, AddCommMonoid (V i)] [∀ i, Module K (V i)]
+    [AddCommMonoid U] [Module K U]
+    (f : ∀ i, U →ₗ[K] (V i)) : U →ₗ[K] (∀ i, V i) := by
+  sorry
+-- { to_fun := λv i, f i v,
+--   map_add' :=
+--   begin
+--     intros,
+--     funext,
+--     simp,
+--   end,
+--   map_smul' :=
+--   begin
+--     intros,
+--     funext,
+--     simp,
+--   end }

server/adam/Adam/Levels/LinearAlgebra/N09_Prod.lean

@@ -0,0 +1,78 @@
+import Adam.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Span
+
+Game "Adam"
+World "Module2"
+Level 9
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+universe u
+
+variable {K : Type u} [Field K]
+variable {ι : Type u} {V : ι → Type u}
+variable [∀i, AddCommMonoid (V i)] [∀i, Module K (V i)]
+
+/-
+Ein externes Summe von Vektorräumen schreibt man mit `\Pi\0`, also `Π₀ i, V i`.
+Das Suffix `_₀` wird in Mathlib häufig dafür verwendet "endlichen Support" zu bezeichnen.
+
+-/
+example : Module K (Π₀ i, V i) := inferInstance
+
+variable {U : Type u} [AddCommMonoid U] [Module K U]
+
+Statement
+"" : True := by
+  sorry
+
+-- -- :(
+-- variable [decidable_eq ι]
+-- variable [Π (i : ι) (x : V i), decidable (x ≠ 0)]
+
+-- def my_sum_map (f : Π i, V i →ₗ[K] U) : (Π₀ i, V i) →ₗ[K] U :=
+-- { to_fun := λ x, x.sum (λ i, (f i)),
+--   map_add' :=
+--   begin
+--     intros,
+--     funext,
+--     sorry,
+--   end,
+--   map_smul' :=
+--   begin
+--     intros,
+--     funext,
+--     simp,
+--     sorry
+--   end }
+
+-- Statement
+-- "Sei `U` ein `K`-Vektorraum und `fᵢ : Vᵢ → U` eine Familie von `K`-lineare Abbildungen
+-- in `K`-Vektorräume. Dann gibt es genau eine Abbildung `f : (Π₀ i, V i) → U`, die mit
+-- allen kommutiert."
+--      (f : ∀ i, V i →ₗ[K] U) :
+--   ∃! (g : (Π₀ i, V i) →ₗ[K] U), (∀ i v, f i v = g (dfinsupp.single i v)) :=
+-- by
+--   let g := my_sum_map f,
+--   use g,
+--   constructor,
+--   { simp,
+--     intros,
+--     sorry },
+--   { intros g' h,
+--     apply linear_map.ext,
+--     intro x,
+--     sorry
+--     -- change (λ i, g' x i) = λ i, f i x, -- Wieso?
+--     -- funext,
+--     -- symmetry,
+--     -- apply h,
+--   }

server/adam/Adam/Levels/Notes.txt

@@ -0,0 +1,4 @@
+- `trivial` uses a bunch of other tactics:
+  (contradiction, assumption, rfl, decide, True.intro, And.intro)
+  so it's maybe not a good candidate to introduce at the beginning of the level.
+- Ringschluss (tfae) is not in mathlib4 yet.

server/adam/Adam/Levels/Numbers.lean

@@ -0,0 +1,2 @@
+import Adam.Levels.Numbers.L01_PNat
+import Adam.Levels.Numbers.L02_PNat

server/adam/Adam/Levels/Numbers/L01_PNat.lean

@@ -0,0 +1,82 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Numbers"
+Level 1
+
+Title ""
+
+Introduction
+"
+-- Level name : Positive natürliche Zahlen
+
+import data.pnat.basic
+
+/-
+In diesem Level lernst du neben `ℕ` weitere Arten von
+Zahlen kennen: `ℕ+`,`ℤ`, `ℚ`, `ℝ`, `ℂ`.
+
+Manchmal sieht man in der Literatur Diskussionen, ob die natürlichen Zahlen jetzt bei `0` oder `1`
+anfangen, wobei zumindest in der formalisierten Mathematik (z.B. ZFC-Mengenlehre)
+eigentlich immer `ℕ = {0, 1, 2, 3, …}` definiert wird.
+
+So ist auch in Lean `1` als `0.succ` und `2 = 1.succ = 0.succ.succ` definiert und
+Lean hat eine separate Notation `ℕ+` (oder `pnat`) für alle *positiven* natürlichen Zahlen.
+
+Dies ist als Sub-Typ von `ℕ` definiert:
+`def pnat := {n : ℕ // 0 < n}`
+
+ein Element `(p : ℕ+)` besteht also aus einer natürlichen Zahl `(p.val : ℕ)`
+(oder auch `p.1`, wobei `p.val` bevorzugt ist) sowie einem Beweis, dass diese positiv ist,
+`p.property` (oder `p.2`).
+
+Solche Strukturen mit mehr als einem Feld kann man in Lean mit dem anonymen Konstruktor `⟨_, _⟩`
+erstellen, wie du schon einmal beim `∃` gesehen hast: `(⟨n, h⟩ : ℕ+)`
+"
+
+Statement
+""
+    (a : ℕ+) : (a : ℕ) ≠ 0 := by
+  apply ne_of_gt
+  rcases a with ⟨a, ha⟩
+  assumption
+
+
+-- -/
+
+-- /- Hint : a.property
+-- `have ha := a.property` speichert die `ℕ+`-Eigenschaft dass `0 < a.val`
+-- gilt als neue Variable.
+-- -/
+
+-- /- Hint : ne_of_lt/ne_of_gt
+-- `a < b → a ≠ b`
+-- oder
+-- `a < b → b ≠ a`
+
+-- alternativ kannst du auch mit `symmetry` ein symmetrischen Goal drehen.
+-- -/
+
+-- /- Lemma : no-side-bar
+-- Beweise.
+-- -/
+-- example (a : ℕ+) : (a : ℕ) ≠ 0 :=
+-- begin
+--   have ha := a.property,
+--   symmetry,
+--   apply ne_of_lt,
+--   exact ha,
+-- end
+
+-- /- Axiom : ne_of_lt
+-- `a < b → a ≠ b`.
+-- -/
+
+-- /- Axiom : ne_of_gt
+-- `a < b → b ≠ a`.
+-- -/
+
+-- /- Tactic : symmetry
+-- Dreht ein symmetrisches Goal wie `A = B`, `A ≠ B`, `A ↔ B`, ...
+-- -/

server/adam/Adam/Levels/Numbers/L02_PNat.lean

@@ -0,0 +1,24 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Numbers"
+Level 2
+
+Title ""
+
+Introduction
+"
+  Das Lemma, das du gerade bewiesen hast, findest du als `pnat.ne_zero`
+"
+
+Statement
+""
+    (a b : ℕ+) : (a : ℕ) * b ≠ 0 := by
+  by_contra h
+  rw [Nat.mul_eq_zero] at h
+  cases h
+  have := PNat.ne_zero a
+  contradiction
+  have := PNat.ne_zero b
+  contradiction

server/adam/Adam/Levels/Predicate.lean

@@ -0,0 +1,27 @@
+import Adam.Levels.Predicate.L01_Ring
+import Adam.Levels.Predicate.L02_Rewrite
+import Adam.Levels.Predicate.L03_Rewrite
+import Adam.Levels.Predicate.L04_Ring
+import Adam.Levels.Predicate.L05_Rfl
+import Adam.Levels.Predicate.L06_Exists
+import Adam.Levels.Predicate.L07_Exists
+import Adam.Levels.Predicate.L08_Forall
+import Adam.Levels.Predicate.L09_PushNeg
+
+Game "Adam"
+World "Predicate"
+Title "Prädikate"
+
+Introduction "Eure Reise geht weiter zum zweiten Mond. Dieser ist etwas grösser und
+komplett mit buschartigen Pflanzen überwachsen. Der Landeanflug sit etwas kniffliger,
+aber offenbar kann Robo nicht nur Lean übersetzen, sondern auch mit maschineller Genauigkeit
+navigieren.
+
+Ihr werdet sofort empfangen und man führt euch zur lokalen Machthaberin.
+Ihr kommt an verschiedensten riesigen Büschen vorbei, die offensichtlich innen Ausgehöhlt sind
+und so als Wände für Behausungen der Wesen hier dienen.
+
+Man führt euch in einen der Büsche. Nun entdecksts du dass das Blätterdach künstlich verstärkt ist,
+offensichtlich um Regen abzuweisen.
+
+Vor euch steht eine Frau, die euch als Machthabering *Evenine* vorgestellt wird."

server/adam/Adam/Levels/Predicate/L01_Ring.lean

@@ -0,0 +1,36 @@
+import Adam.Metadata
+import Mathlib.Tactic.Ring
+
+--set_option tactic.hygienic false
+
+Game "Adam"
+World "Predicate"
+Level 1
+
+Title "Natürliche Zahlen"
+
+Introduction
+"
+**Evenine**: Willkommen Reisende! Wir leben hier in Einklang mit der Natur und allem natürlichen,
+so sagt mir, könnt ihr mit natürlichen Zahlen umgehen?
+"
+
+Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
+  Hint "**Du**: Das hab ich in der Schule gelernt, man rechnet das einfach aus,
+  indem man die Terme umsortiert.
+
+  **Robo**: Behaupte doch mit `ring`, dass das so ist.
+
+  **Du**: Aber `ℕ` ist doch gar kein Ring?
+
+  **Robo**: `ring` funktioniert schon für Halbringe, aber sie heisst ring, weil sie auf
+  (kommutativen) Ringen am besten funktioniert.
+  "
+  ring
+
+Conclusion
+"
+*Evenine: Ja das stimmt schon. Und das genügt uns auf diesem Planet auch als Antwort.*
+"
+
+NewTactic ring

server/adam/Adam/Levels/Predicate/L02_Rewrite.lean

@@ -0,0 +1,39 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Predicate"
+Level 2
+
+Title "Rewrite"
+
+Introduction
+"
+Robo spuckt den Brief aus, den er dabei hatte, und gibt ihn *Evenine*.
+
+**Evenine**: Das verstehe ich nicht, wisst ihr was damit gemeint ist?
+
+Und sie händigt Dir den Brief:
+"
+
+Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  Hint "**Du**: Schau mal, das ist ja fast genau, was wir auf *Implis* gemacht haben,
+  nur jetzt mit Gleichheiten von Zahlen anstatt Genau-Dann-Wenn-Aussagen!
+
+  **Robo**: `=` und `↔` kannst du praktisch gleich behandeln wenns um `rw` geht."
+  Hint (hidden := true) "**Du**: Also auch `rw [hₓ]` und `rw [← hₓ]`?
+
+  **Robo**: Probiers doch einfach."
+  rw [h₁]
+  Hint (hidden := true) "**Du**: Wie war das nochmals mit rückwärts umschreiben?
+
+  **Robo**: `←` ist `\\l`. Und dann `rw [← hₓ]`"
+  rw [←h₂]
+  assumption
+
+Conclusion
+"
+**Evenine**: Danke viemals, das hilft uns vermutlich, jetzt Frage ich mich aber…
+"
+
+NewTactic assumption rw

server/adam/Adam/Levels/Predicate/L03_Rewrite.lean

@@ -0,0 +1,36 @@
+import Adam.Metadata
+import Mathlib
+
+Game "Adam"
+World "Predicate"
+Level 3
+
+Title "Rewrite"
+
+Introduction
+"
+**Evenine**: Mit diesem neuen Wissen, könnt ihr mir bei folgendem helfen:
+"
+
+Statement
+"
+$$
+\\begin{aligned}
+  a &= b \\\\
+  a + a ^ 2 &= b + 1 \\\\
+  \\vdash b + b ^ 2 = b + 1
+\\end{aligned}
+$$
+"
+(a b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 := by
+  Hint "**Du**: Ah da ersetzt man ja einfach `{a}` durch `{b}` in der anderen Annahme!
+
+  **Robo**: Genau! Das machst du mit `rw [{h}] at {g}`."
+  rw [h] at g
+  Hint (hidden := true) "**Robo**: Schau mal durch die Annahmen."
+  assumption
+
+Conclusion "
+**Robo**: Noch ein Trick: Mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
+dem Goal umschreiben.
+"

server/adam/Adam/Levels/Predicate/L04_Ring.lean

@@ -0,0 +1,35 @@
+import Adam.Metadata
+import Mathlib.Tactic.Ring
+
+Game "Adam"
+World "Predicate"
+Level 4
+
+Title "Natürliche Zahlen"
+
+Introduction
+"
+*Evenines* Berater meldet sich.
+
+**Berater**: Das stimmt wohl, aber das Problem, das uns eigentlich beschäftigt hat, eure
+Natürlichkeit, war folgendes:
+"
+
+Statement
+    (x y z : ℕ) (h : x = 2 * y + 1) (g : z  = 3 * y + 1): x ^ 2 = 4 * y ^ 2 + z + y := by
+  Hint "**Du**: Ich versteh das Pattern. Wenn ich zuerst alles so umschreibe, dass
+  das Goal nur noch rechnen und umsortieren ist, dann kann `ring` den Rest machen!
+
+  **Robo**: Noch ein Trick: Entweder kannst du zwei Befehle `rw [h₁]` und `rw [h₂]` schreiben,
+  oder du kannst das gleich in einem machen : rw [h₁, h₂]."
+  rw [h, g]
+  ring
+
+
+Conclusion
+"
+*Evenine* bedankt sich nochmals für die Botschaft und ihr werdet zu einem kleineren Busch geführt,
+der ein gemütlich warmes Innenleben an den Tag legt.
+"
+
+NewTactic ring rw

server/adam/Adam/Levels/Predicate/L05_Rfl.lean

@@ -0,0 +1,36 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Predicate"
+Level 5
+
+Title "Definitionally equal"
+
+Introduction
+"
+Müde ruht ihr euch in eurer Bleibe aus. Du schaust doch eine Lücke in den Blättern vielen
+kleinen Vögeln bei der Nahrungssuche zu.
+
+**Du**: Sag mal Robo, ich hab vorhin ein Kind überhört, dass seinem Spielgefährten erklärt hat,
+folgendes sei mit `rfl` zu beweisen:
+"
+
+Statement : 1 + 1 = 2 := by
+  Hint "**Du**: Wieso nicht `ring`?
+
+  **Robo**: Klar, `ring` geht auch und ist intuitiver.
+  Für `rfl` kommt es darauf an, wie die Sachen genau definiert sind: `1 + 1` ist als
+  `(0.succ).succ` definiert und `2` halt ebenfalls.
+  "
+  rfl
+
+OnlyTactic rfl
+
+Conclusion
+"
+**Du**: Dann war das mehr Glück?
+
+**Robo**: Das ist eine Art die Welt zu sehen…
+
+Damit fällst du in einen ruhigen Schlaf.
+"

server/adam/Adam/Levels/Predicate/L06_Exists.lean

@@ -0,0 +1,73 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Mathlib.Algebra.Parity
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Predicate"
+Level 6
+
+Title "Gerade/Ungerade"
+
+Introduction
+"
+Am nächsten Tag erklärt euch *Evenine*, dass es auf dem Mond zwei Gruppierungen gibt,
+ihre und die ihres Halbbruders *Oddeus*. Die Mottos sind
+
+```
+def Even (n : ℕ) : Prop := ∃ r, n = r + r
+```
+
+und
+
+```
+def Odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
+```
+
+**Evenine**: Hier, ich zeige euch mal etwas was man bei uns machen kann:
+"
+
+Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
+  Branch
+    unfold Even
+    Hint "Rob**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst was los ist."
+  Hint "**Robo**: Wie du oben siehst, ist `Even n` dadurch definiert,
+    dass ein `r` existiert so dass `r + r = n`. Am besten
+    öffnest du diese Definition mit `unfold Even at *` einmal, dann siehst du besser, was los ist. "
+  unfold Even at *
+  Hint "**Du**: Also von `{h}` weiss ich jetzt dass ein `r` existiert, so dass `r + r = n`…
+
+  **Robo**: Mit `rcases h with ⟨r, hr⟩` kannst du dieses `r` tatsächlich einführen."
+  rcases h with ⟨r, hr⟩
+  Hint "**Du**: Und jetzt muss ich eine passende Zahl finden, so dass `x + x = n^2`?
+
+  **Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
+  Hint (hidden := true) "**Robo**: Also sowas ähnliches wie `use 4 * r ^ 3`, aber ich kann
+  dir leider nicht sagen, welche Zahl passt.
+  "
+  Branch
+    rw [hr]
+    Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
+    use 2 * r ^ 2
+    ring
+  use 2 * r ^ 2
+  Hint "**Du**: Ah und jetzt `ring`!
+
+  **Robo**: Aber zuerst must du noch mit
+  `rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiss."
+  rw [hr]
+  ring
+
+-- TODO: [Comment] For me the expected behaviour of `(strict := true)` would
+-- be that it distinguishes between the defEq states while `(strict := false)`
+-- would show the hint regardless of a `unfold Even`.
+
+NewTactic unfold use
+NewDefinition Even Odd
+
+Conclusion "**Evenine**: Seht ihr?"

server/adam/Adam/Levels/Predicate/L07_Exists.lean

@@ -0,0 +1,43 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Mathlib.Algebra.Parity
+
+set_option tactic.hygienic false
+
+Game "Adam"
+World "Predicate"
+Level 7
+
+Title "Gerade/Ungerade"
+
+Introduction
+"
+**Du**: Aber, das sagt doch gar nichts aus, genau das gleiche könnte ich für `Odd`
+auch sagen. Hier seht!
+"
+
+Statement odd_square (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by
+  unfold Odd at *
+  rcases h with ⟨r, hr⟩
+  Hint "**Robo**: Ich hab noch einen Trick auf Lager:
+  Wenn du jetzt herausfinden willst, welche Zahl du einsetzen musst, könntest
+  du schon jetzt mit `rw [{hr}]` weitermachen…"
+  rw [hr]
+  Hint "**Robo**: Wenn du jetzt `ring` benötigst, dann schreibt es einfach alles in
+  Normalform um, das hilft beim vergleichen."
+  ring
+  Hint "**Du**: Was bedeutet `ring_nf`?
+
+  **Robo**: Wenn man `ring` nicht am Schluss benützt, sollte man stattdessen `ring_nf`
+  schreiben, aber die funktionieren praktisch gleich."
+  use 2 * (r + r ^ 2)
+  ring
+
+-- TODO: Allow `ring_nf` as part of `ring`.
+
+Conclusion "**Evenine**: Tatsächlich. Vielleicht sind wir gar nich tso unterschiedlich. Könntet
+ihr mal mit ihm reden gehen?"

server/adam/Adam/Levels/Predicate/L08_Forall.lean

@@ -0,0 +1,53 @@
+import Adam.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Mathlib.Algebra.Parity
+import Mathlib
+
+Game "Adam"
+World "Predicate"
+Level 8
+
+Title "Für alle"
+
+Introduction
+"
+Ihr macht euch also auf den Weg. Unterwegs trefft ihr einen Händler und ihr lässt euch von
+ihm den Weg zeigen, sowie einige Tipps zu den beiden Geschwistern geben.
+
+**Händler**: Also seht, die beiden sind gar nicht so verschieden. Ein altes Sprichwort sagt:
+"
+
+--   Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
+
+-- Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
+
+-- Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
+-- auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
+
+-- Also folgende Annahme und Lemma sind genau :
+-- - `(le_square : ∀ (n : ℕ), n ≤ n^2)`
+-- - `lemma le_square (n : ℕ) : n ≤ n^2`
+
+-- Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
+
+
+-- TODO: 1-2 Aufgaben mehr.
+
+Statement : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
+  Hint "**Du**: Das `∀` heisst sicher \"für alle\".
+
+  **Robo**: Und man schreibt `\\forall`. Ein `∀ x, …` im Goal kannst du wie eine
+  Implikation mit `intro x` angehen."
+  intro x h
+  unfold Even at h
+  unfold Odd
+  rcases h with ⟨y, hy⟩
+  use y
+  rw [hy]
+  ring
+
+Conclusion "**Händler**: Sichere Reise!"

server/adam/Adam/Levels/Predicate/L09_PushNeg.lean

@@ -0,0 +1,109 @@
+import Adam.Metadata
+import Mathlib.Tactic.PushNeg
+import Mathlib
+
+import Mathlib.Algebra.Parity
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Predicate"
+Level 9
+
+Title "PushNeg"
+
+Introduction
+"
+Das Dorf von *Oddeus* scheint stärker befestigt zu sein, all jenes von *Evenine*. Ihr kommt
+and eine Wand aus Dornenranken. Beim Eingang steht eine Wache, die auch zuruft:
+
+"
+
+-- Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
+-- mit `push_neg` das `¬` durch den Quantor hindurchschieben.
+
+-- Das braucht intern die Lemmas
+
+-- - `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
+-- - `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
+
+-- (welche man auch mit `rw` explizit benutzen könnte.)
+
+open Nat
+
+Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
+  Hint "**Du**: Also ich kann mal das `¬` durch die Quantifier hindurchschieben.
+
+  **Robo**: `push_neg` macht genau das!
+
+  **Robo**: Intern braucht das zwei Lemmas
+
+  ```
+  not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)
+  not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)
+  ```
+  die du natürlich auch mit `rw` gebrauchen könntest."
+  Branch
+    unfold Odd
+    push_neg
+    Hint "**Robo**: Der Weg ist etwas schwieriger. Ich würde nochmals zurück und schauen,
+    dass du irgendwann `¬Odd` kriegst, was du dann mit `rw [←even_iff_not_odd]`
+    zu `Even` umwandeln.
+    kannst."
+  push_neg
+  intro n
+  Hint "**Robo**: Welche Zahl du jetzt mit `use` brauchst, danach wirst du vermutlich das
+  Lemma `←even_iff_not_odd` brauchen.
+
+  **Du**: Könnte ich jetzt schon `rw [←even_iff_not_odd]` machen?
+
+  **Robo**: Ne, `rw` kann nicht innerhalb von Quantifiern umschreiben.
+
+  **Du**: Aber wie würde ich das machen?
+
+  **Robo**: Zeig ich dir später, die Wache wird schon ganz ungeduldig!
+  Im Moment würde ich zuerst mit `use` eine richtige Zahl angeben, und danach umschreiben."
+  Branch
+    use n + 2
+    Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
+  Branch
+    use n + 4
+    Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
+  use n
+  Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
+  rw [←even_iff_not_odd]
+  unfold Even
+  use n
+  --ring
+
+Conclusion "Damit werdet ihr eingelassen.
+
+**Robo**: Entweder wir suchen direkt diesen *Oddeus*, oder wir schauen uns einmal um. Die Wahl
+ist deine!
+
+**Du**: Kannst du mir nochmals einen Überblick geben, was wir gelernt haben?
+
+**Robo**:
+
+|               | Beschreibung                |
+|:--------------|:----------------------------|
+| `ℕ`           | Die natürlichen Zahlen.     |
+| `∃`           | Existential-Quantifier      |
+| `∀`           | Forall-Quantifier           |
+| `Even n`      | `n` ist gerade              |
+| `Odd n`       | `n` ist ungerade            |
+
+|       | Taktik                    | Beispiel                                               |
+|:------|:--------------------------|:-------------------------------------------------------|
+| *12ᶜ* | `rw`                      | Umschreiben mit Gleichungen.                           |
+| 13    | `ring`                    | Löst Gleichungen mit `+, -, *, ^`.                     |
+| 14    | `unfold`                  | Setzt visuell die Bedeutung einer Definition ein.      |
+| 15    | `use`                     | Um ein `∃` im Goal anzugehen.                          |
+| *7ᶜ*  | `rcases h with ⟨x, hx⟩`   | Um ein `∃` in den Annahmen zu zerlegen.                |
+| *8ᵇ*  | `intro`                   | Um ein `∀` im Goal anzugehen.                          |
+| 16    | `push_neg`                | Für `¬∃` und `¬∀` im Goal.                             |
+
+"
+
+NewTactic push_neg
+NewLemma Nat.even_iff_not_odd Nat.odd_iff_not_even not_exists not_forall

server/adam/Adam/Levels/Prime.lean

@@ -0,0 +1,11 @@
+import Adam.Levels.Prime.L01_Dvd
+-- import Adam.Levels.Prime.L04_Prime
+-- import Adam.Levels.Prime.L05_Prime
+-- import Adam.Levels.Prime.L06_ExistsUnique
+
+Game "Adam"
+World "Prime"
+Title "Teilbarkeit"
+
+Introduction "Ihr schlendert durch die Befestigung ohne direktes Ziel. Und sprecht mit
+verschiedenen Einwohnern."

server/adam/Adam/Levels/Prime/L01_Dvd.lean

@@ -0,0 +1,49 @@
+import Adam.Metadata
+
+import Mathlib.Tactic.Ring
+import Mathlib
+
+Game "Adam"
+World "Prime"
+Level 1
+
+Title "Teilbarkeit"
+
+Introduction
+"
+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.
+
+**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?
+"
+
+-- 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
+
+DisabledLemma dvd_add

server/adam/Adam/Levels/Prime/L02_Prime.lean

@@ -0,0 +1,51 @@
+import Adam.Metadata
+import Mathlib.Data.Nat.Prime
+
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+-- import Data.Nat.Prime
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Prime"
+Level 2
+
+Title "Primzahlen"
+
+Introduction
+"
+Als nächstes Begnet ihr einem Lehrer, der nachdenkend an der Sonne sitzt.
+
+**Lehrer**: Sagt mal, mich hat heute einer meiner Schüler was gefragt,
+und ich glaube einfach, der ist in so jungen Jahren bereits schlauer als ich.
+
+Hier etwas Kontext:
+"
+
+Statement (p : ℕ) (h : Nat.Prime p) : ∀ (x : ℕ), (x ∣ p) → x = 1 ∨ x = p := by
+  Hint "**Du**: Die einzigen Teiler einer Primzahl sind `1` und `p`, ist das
+  nicht eine der möglichen Definitionen über `ℕ`?
+
+  **Robo**: Doch, oder zumindest fast.
+  Du kannst du mit `rw` und `Nat.prime_def_lt''` eine der Definitionen für `Nat.Prime` einsetzen
+
+  **Du** Könnte ich nicht einfach `unfold Nat.Prime` sagen um mir das anzuschauen.
+
+  **Robo**: Bloss nicht. Das ist so eine Definition, in die du besser nicht hineinschaust!
+  `Nat.Prime p` ist als `Irreducible p` definiert, was wiederum anhand von Einheiten
+  definiert ist… Da verlieren wir uns in Definition die wir im Moment gar nicht brauchen."
+  rw [Nat.prime_def_lt''] at h
+  rcases h with ⟨_, h₂⟩
+  assumption
+
+NewLemma Nat.prime_def_lt''
+
+Conclusion "**Du**: Ich sehe, meine \"Definition\" hätte auch `1` als Primzahl deklariert. Gut,
+dass wir das überprüft haben.
+
+**Lehrer**: Und jetzt kommen wir zu dem, was mir Kopfschmerzen bereitet."

server/adam/Adam/Levels/Prime/L03_Prime.lean

@@ -0,0 +1,41 @@
+import Adam.Metadata
+import Mathlib.Data.Nat.Prime
+
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Prime"
+Level 3
+
+Title "Primzahlen"
+
+Introduction
+"
+Der Lehrer erklärt sein Problem.
+
+**Lehrer**: Und dann fragte der Schüler, wie man denn folgendes herleitet.
+Und dabei ist das weit über seiner Altersstufe!
+"
+
+Statement
+  (p : ℕ) (h₂ : 2 ≤ p): Nat.Prime p ↔ ∀ (a b : ℕ), p ∣ a * b → p ∣ a ∨ p ∣ b := by
+  Hint "**Du**: Naja, mal schauen wie weit man mit `intro` und `constructor` kommt…"
+  constructor
+  intro h a b
+  Hint "**Robo**: Stop! Hier helfe ich dir etwas"
+  apply (Nat.Prime.dvd_mul h).mp
+  intro h
+  rw [Nat.prime_iff]
+  unfold Prime
+  rw [Nat.isUnit_iff, ←and_assoc]
+  constructor
+  constructor
+  linarith
+  linarith
+  assumption

server/adam/Adam/Levels/Prime/L06_ExistsUnique.lean

@@ -0,0 +1,34 @@
+import Adam.Metadata
+import Mathlib.Data.Nat.Prime
+
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Adam.ToBePorted
+
+Game "Adam"
+World "Prime"
+Level 4
+
+Title "Existiert eindeutig"
+
+Introduction
+"
+Hier lässt sich noch eine neue Notation einführen: `∃!` bedeutet
+\"es existiert ein eindeutiges\" und ist definiert als
+
+
+"
+
+Statement
+"Zeige dass die einzige gerade Primzahl $2$ ist."
+    : ∃! p, Nat.Prime p ∧ Even p := by
+  use 2
+  constructor
+  simp
+  rintro y ⟨hy, hy'⟩
+  rw [←Nat.Prime.even_iff hy]
+  assumption

server/adam/Adam/Levels/Proposition.lean

@@ -0,0 +1,39 @@
+import Adam.Levels.Proposition.L00_Tauto
+import Adam.Levels.Proposition.L01_Rfl
+import Adam.Levels.Proposition.L02_Assumption
+import Adam.Levels.Proposition.L03_Assumption
+import Adam.Levels.Proposition.L04_True
+import Adam.Levels.Proposition.L05_Not
+import Adam.Levels.Proposition.L06_False
+import Adam.Levels.Proposition.L07_ContraNotEq
+import Adam.Levels.Proposition.L08_Contra
+import Adam.Levels.Proposition.L09_And
+import Adam.Levels.Proposition.L10_And
+import Adam.Levels.Proposition.L11_Or
+import Adam.Levels.Proposition.L12_Or
+import Adam.Levels.Proposition.L13_Summary
+
+Game "Adam"
+World "Proposition"
+Title "Aussagenlogik 1"
+
+Introduction "
+Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
+bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
+Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
+
+Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
+sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
+seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
+herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
+keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
+
+Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
+überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik
+exklusiv in einem Dir fremden Dialekt, den sie Leansch [liːnʃ] nennen.
+
+Zum Glück hat Robo mit Dir das Universum gewechselt.
+Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir
+in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leansch gelernt.
+Und das ist Gold wert.
+"

server/adam/Adam/Levels/Proposition/L00_Tauto.lean

@@ -0,0 +1,46 @@
+import Adam.Metadata
+import Mathlib.Tactic.Tauto
+
+Game "Adam"
+World "Proposition"
+Level 1
+
+Title "Automatisierung"
+
+Introduction
+"
+Gerade seid Ihr auf Königin *Logisindes* Planeten. Sie kommt ohne Umschweife zum Punkt:
+
+**Logisinde**  Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt …
+
+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.
+"
+
+Statement ""
+    (A B C : Prop) :
+    ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
+  Hint "**Robo**  Das ist ganz einfach.  Mit `{A} {B} {C} : Prop` meint sie:
+  `{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
+  Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
+
+  **Du** Ehhm, ja.  Aber da muss ich jetzt trotzdem erst einmal überlegen.
+
+  **Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
+
+  **Du** Ernsthaft?
+
+  **Robo** Ja.  Schreib einfach `tauto`.
+
+  **Robo** Mach schon …"
+  tauto
+
+Conclusion
+"
+**Logisinde** (etwas konsterniert)  Ja, das ist streng genommen richtig.
+Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt!
+Meine Untertanen verstehen `tauto` nicht.  Da müsst Ihr Euch schon etwas mehr anstrengen.
+"
+
+NewTactic tauto

server/adam/Adam/Levels/Proposition/L01_Rfl.lean

@@ -0,0 +1,32 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Proposition"
+Level 2
+
+Title "Aller Anfang ist... ein Einzeiler?"
+
+Introduction
+"
+In der Zwischenzeit hat bereits sich eine lange Schlange Untertanen gebildet, die gern ihren
+Fragen stellen würden. Logisinde winkt den ersten nach vorn. Er räuspert sich.
+
+**Untertan** Warum ist $42 = 42$?
+
+Du schaust ihn fassungslos an.
+Er schreibt es Dir wieder auf.
+"
+
+Statement "" :
+  42 = 42 := by
+  Hint " **Robo** Ist doch klar.  Du musst ihn einfach daran erinnern,
+    dass Gleichheit *reflexiv* ist. Probier mal `rfl`."
+  rfl
+
+Conclusion
+"
+**Untertan** Ah, richtig. Ja, Sie haben ja so recht.  Das vergesse ich immer.  Rfl, rfl, rfl …
+"
+
+NewTactic rfl
+DisabledTactic tauto

server/adam/Adam/Levels/Proposition/L02_Assumption.lean

@@ -0,0 +1,43 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Proposition"
+Level 3
+
+Title "Annahmen"
+
+Introduction
+"
+Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste nach vorne. Es ist schüchtern und schreibt bloß.
+"
+
+Statement ""
+    (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
+  Hint "
+**Robo** `{n} : ℕ` bedeutet, `{n}` ist eine natürliche Zahl.
+
+**Du** Warum schreibt er dann nicht `{n} ∈ ℕ`??
+
+**Robo** Weil das hier alles komische Typen sind …  Ich kann Dir das später mal in Ruhe erklären.
+Jetzt will ich erst einmal die Frage entschlüsseln.
+
+**Robo** Also, `{h₁}`, `{h₂}`, `{h₃}` sind einfach nur Namen für verschiedene Annahmen, und zwar
+für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`.
+
+**Du** Aber das war doch gerade eine der Annahmen.
+
+**Robo** Ja, stimmt.
+
+**Du** ???
+
+**Robo** Du musst ihm das halt explizit sagen.  Probiers mal mit `assumption`."
+  assumption
+
+Conclusion
+"
+**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf
+zerbrochen habe!
+"
+
+NewTactic assumption
+DisabledTactic tauto

server/adam/Adam/Levels/Proposition/L03_Assumption.lean

@@ -0,0 +1,36 @@
+import Adam.Metadata
+import Mathlib.Data.Nat.Basic -- TODO
+
+Game "Adam"
+World "Proposition"
+Level 4
+
+Title "Logische Aussagen"
+
+Introduction
+"
+Ein dritter Untertan kommt mit folgendem Problem.
+"
+
+Statement ""
+  (A : Prop) (hA : A) : A := by
+  Hint "
+**Robo** Hier bedeutet `{A} : Prop` wieder, dass `{A}` irgendeine Aussage ist.
+   Und `{hA}` ist eine Name für die Annahme, dass `{A}` wahr ist.
+
+**Du** Und unter dieser Annahme sollen wir jetzt `{A}` beweisen?
+
+**Robo** Ja.  Da kommst Du jetzt selbst drauf, wie das geht, oder?
+"
+  Hint (hidden := true) "**Robo**: Ist doch genau wie eben:
+die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
+Also wird `assumption` auch wieder funktionieren."
+  assumption
+
+Conclusion
+"
+**Untertan** Das ging ja schnell. Super! Vielen Dank.
+"
+
+NewTactic assumption
+DisabledTactic tauto

server/adam/Adam/Levels/Proposition/L04_True.lean

@@ -0,0 +1,37 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Proposition"
+Level 5
+
+Title "True/False"
+
+Introduction
+"
+Der nächste Untertan in der Reihe ist ein Schelm.
+"
+
+Statement "" : True := by
+  Hint "
+**Robo**  Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und
+bedingungslos wahr ist.
+
+**Du** Und was genau ist dann zu beweisen?
+
+**Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben.
+"
+  trivial
+
+Conclusion
+"
+**Schelm**  Wollte nur mal sehen, dass Ihr nicht auf den Kopf gefallen seid …
+
+**Du** *(zu Robo)*  Können wir nicht einfach immer dieses `trivial` verwenden?
+Wie in einer Mathe-Vorlesung?
+
+**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung.
+Das funktioniert nur in einer Handvoll Situationen.
+"
+
+NewTactic trivial
+DisabledTactic tauto

server/adam/Adam/Levels/Proposition/L05_Not.lean

@@ -0,0 +1,34 @@
+import Adam.Metadata
+
+Game "Adam"
+World "Proposition"
+Level 6
+
+Title "Not"
+
+Introduction
+"
+Der Schelm hat noch eine Schwester dabei.
+"
+
+Statement "" : ¬False := by
+  Hint "
+**Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
+wahr ist, dann ist  `¬A` falsch, und umgekehrt.
+
+**Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
+
+**Robo** Ja, richtig.
+
+**Du** Ist das jetzt nicht doch wieder trivial?
+
+**Robo** Probier mal!"
+  trivial
+
+Conclusion
+"
+Die Schwester lacht und eilt ihrem Bruder hinterher.
+"
+
+NewTactic trivial
+DisabledTactic tauto