From 5bf0cd9775c45996e3d30c1a07e87f943b222a2d Mon Sep 17 00:00:00 2001
From: Jon Eugster <Jon.Eugster@hhu.de>
Date: Tue, 29 Nov 2022 17:11:17 +0100
Subject: [PATCH] first_levels

---
 package-lock.json                             |  2 +-
 server/leanserver/GameServer/Commands.lean    |  2 +-
 server/testgame/TestGame.lean                 | 11 ++--
 server/testgame/TestGame/LemmaDocs.lean       | 18 +++---
 .../TestGame/Levels/Logic/003_Assumption.lean | 57 ------------------
 .../Levels/Logic/003b_Assumption.lean         |  0
 .../TestGame/Levels/Logic/005_Apply.lean      | 59 -------------------
 .../Logic/{001_Refl.lean => L01_Rfl.lean}     |  6 +-
 .../Logic/{002_Refl.lean => L02_Rfl.lean}     |  8 +--
 .../TestGame/Levels/Logic/L03_Assumption.lean | 29 +++++++++
 .../Levels/Logic/L03b_Assumption.lean         | 28 +++++++++
 .../{004_Rewrite.lean => L04_Rewrite.lean}    | 35 +++++------
 .../TestGame/Levels/Logic/L05_Apply.lean      | 33 +++++++++++
 .../TestGame/Levels/StatementTest.lean        | 38 ++++++++++++
 server/testgame/TestGame/Metadata.lean        |  9 +--
 server/testgame/TestGame/MyNat.lean           |  3 +-
 server/testgame/TestGame/TacticDocs.lean      |  6 ++
 server/testgame/TestGame/Tactics.lean         |  6 +-
 server/testgame/lakefile.lean                 |  3 +
 19 files changed, 186 insertions(+), 167 deletions(-)
 delete mode 100644 server/testgame/TestGame/Levels/Logic/003_Assumption.lean
 delete mode 100644 server/testgame/TestGame/Levels/Logic/003b_Assumption.lean
 delete mode 100644 server/testgame/TestGame/Levels/Logic/005_Apply.lean
 rename server/testgame/TestGame/Levels/Logic/{001_Refl.lean => L01_Rfl.lean} (92%)
 rename server/testgame/TestGame/Levels/Logic/{002_Refl.lean => L02_Rfl.lean} (73%)
 create mode 100644 server/testgame/TestGame/Levels/Logic/L03_Assumption.lean
 create mode 100644 server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
 rename server/testgame/TestGame/Levels/Logic/{004_Rewrite.lean => L04_Rewrite.lean} (53%)
 create mode 100644 server/testgame/TestGame/Levels/Logic/L05_Apply.lean
 create mode 100644 server/testgame/TestGame/Levels/StatementTest.lean

diff --git a/package-lock.json b/package-lock.json
index 51723c2..3338bc5 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -12297,7 +12297,7 @@
     },
     "lean4web": {
       "version": "git+ssh://git@github.com/hhu-adam/lean4web.git#465694da60e2afbf7d188b41af173998ae75d915",
-      "from": "lean4web@git+https://github.com/hhu-adam/lean4web.git",
+      "from": "lean4web@github:hhu-adam/lean4web",
       "requires": {
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 22732c8..db9628b 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -48,7 +48,7 @@ elab "Introduction" t:str : command => do
   | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
 
 /-- Define the statement of the current level. -/
-elab "Statement" name:ident ? sig:declSig val:declVal : command => do
+elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
   let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String)
   elabCommand (← `(theorem $(mkIdent declName) $sig $val))
diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index ff92164..11936d6 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -1,6 +1,7 @@
 import TestGame.Metadata
-import TestGame.Levels.Level1
-import TestGame.Levels.Level2
-import TestGame.Levels.Level3
-import TestGame.Levels.Level4
-import TestGame.Levels.Level5
\ No newline at end of file
+import TestGame.Levels.Logic.L01_Rfl
+import TestGame.Levels.Logic.L02_Rfl
+import TestGame.Levels.Logic.L03_Assumption
+import TestGame.Levels.Logic.L03b_Assumption
+import TestGame.Levels.Logic.L04_Rewrite
+import TestGame.Levels.Logic.L05_Apply
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index e49db37..b12744f 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -1,14 +1,14 @@
 import GameServer.Commands
-import TestGame.MyNat
+-- import TestGame.MyNat
 
-LemmaDoc zero_add as zero_add in "Addition"
-"This lemma says `∀ a : ℕ, 0 + a = a`."
+-- LemmaDoc zero_add as zero_add in "Addition"
+-- "This lemma says `∀ a : ℕ, 0 + a = a`."
 
-LemmaDoc add_zero as add_zero in "Addition"
-"This lemma says `∀ a : ℕ, a + 0 = a`."
+-- LemmaDoc add_zero as add_zero in "Addition"
+-- "This lemma says `∀ a : ℕ, a + 0 = a`."
 
-LemmaDoc add_succ as add_succ in "Addition"
-"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
+-- LemmaDoc add_succ as add_succ in "Addition"
+-- "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
 
-LemmaSet addition : "Addition lemmas" := 
-zero_add add_zero
\ No newline at end of file
+-- LemmaSet addition : "Addition lemmas" :=
+-- zero_add add_zero
diff --git a/server/testgame/TestGame/Levels/Logic/003_Assumption.lean b/server/testgame/TestGame/Levels/Logic/003_Assumption.lean
deleted file mode 100644
index 540f464..0000000
--- a/server/testgame/TestGame/Levels/Logic/003_Assumption.lean
+++ /dev/null
@@ -1,57 +0,0 @@
-import TestGame.Metadata
-
-Game "Introduction"
-World "Tactic"
-Level 3
-
-Title "Annahmen"
-
-Introduction
-"
-Um Aussagen zu formulieren braucht man Annahmen. Zum einen sind das Objekte, von denen
-eine Aussage handelt, wie zum Beispiel \"sei `n` eine natürliche Zahl\", oder
-\"seien `A`, `B` logische Aussagen\", zum anderen sind dass Annahmen wie \"angenommen
-dass `n` nicht Null ist\" oder \"angenommen `A` ist wahr\".
-
-In Lean schreibt man beides mit der gleichen Notation: `(n : ℕ)` ist eine natürliche Zahl,
-`(A B : Prop)` sind Aussagen, `(h : n ≠ 0)` ist eine Annahme, dass `n` nicht Null ist, und
-`(hA : A)` ist die Annahme, dass `A` wahr ist (`hA` ist ein Beweis von `A`).
-
-Die Annahmen kommen dann vor den Doppelpunkt.
-
-Wenn eine Annahme `h` genau dem Goal entspricht, kannst du `exact h` verwenden.
-"
-
-Statement theorem not_or (n : ℕ) (h : n = 0) : n = 0 := by
-  assumption
-
--- TODO: In Lean3 hatten wir ein Lemma-Text. Können wir den wieder haben?
-
--- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
-Statement (A : Prop) (hA : A) : A := by
-  assumption
-
-@[description "halli hallo"]
-Statement instance hallo : Hallo Nat where
-  mul_eq_add := by
-    $editor {
-    rfl
-    rw }
-  add_comm := by
-    rfl
-    apply
-
-Statement "halli hallo" instance hallo : Hallo Nat where
-  mul_eq_add := by
-    $editor {
-    rfl
-    rw }
-  add_comm := by
-    rfl
-    apply
-
-
-
-Conclusion ""
-
-Tactics assumption
diff --git a/server/testgame/TestGame/Levels/Logic/003b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/003b_Assumption.lean
deleted file mode 100644
index e69de29..0000000
diff --git a/server/testgame/TestGame/Levels/Logic/005_Apply.lean b/server/testgame/TestGame/Levels/Logic/005_Apply.lean
deleted file mode 100644
index 0350e94..0000000
--- a/server/testgame/TestGame/Levels/Logic/005_Apply.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-import TestGame.Metadata
-
-Game "Introduction"
-World "Tactic"
-Level 5
-
-Title "Implikation"
-
-Introduction
-"
-Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und
-die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der
-Aussage `A`.
-
-Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Zeichen dafür:
-`A ↔ B` (`\\iff`) bedeutet \"Genau dann wenn\" und `A → B` (`\\to`) bedeutet \"`A` impliziert `B`\".
-
-Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man
-diese mit `apply h` anwenden.
-Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\".
-"
-
-Statement (A B : Prop) (hA : A) (g : A → B) : B := by
-  apply g
-  assumption
-
--- Gleich am Anfang anzeigen.
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste
-`c` im Goal mit `d` ersetzen."
-
-Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man schreibt diese mit
-`\\1`, `\\2`, `\\3`, …"
-
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
-"Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses
-`(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."
-
--- TODO: Muss ich das wirklich mehrmals auflisten?
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = a =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = b =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : c = c =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : d = d =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-
-Conclusion "Übrigens, mit `rw [h₁] at h₂` kann man auch eine andere Annahme umschreiben
-anstatt dem Goal."
--- TODO: Das macht es doch unmöglich mit den Messages...
-
-Tactics assumption
---Tactics rw
diff --git a/server/testgame/TestGame/Levels/Logic/001_Refl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
similarity index 92%
rename from server/testgame/TestGame/Levels/Logic/001_Refl.lean
rename to server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
index 2e4b851..7894fa6 100644
--- a/server/testgame/TestGame/Levels/Logic/001_Refl.lean
+++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean
@@ -1,7 +1,7 @@
 import TestGame.Metadata
 
-Game "Introduction"
-World "Tactic"
+Game "TestGame"
+World "TestWorld"
 Level 1
 
 Title "Aller Anfang ist... ein Einzeiler?"
@@ -21,7 +21,7 @@ ersten offenen Goal zu machen.
 Wenn der Beweis komplett ist, erscheint \"goals accomplished\".
 "
 
-Statement : 42 = 42 := by
+Statement "Zeige `42 = 42`." : 42 = 42 := by
   rfl
 
 Message : 42 = 42 =>
diff --git a/server/testgame/TestGame/Levels/Logic/002_Refl.lean b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean
similarity index 73%
rename from server/testgame/TestGame/Levels/Logic/002_Refl.lean
rename to server/testgame/TestGame/Levels/Logic/L02_Rfl.lean
index eea5677..8b53a51 100644
--- a/server/testgame/TestGame/Levels/Logic/002_Refl.lean
+++ b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean
@@ -1,14 +1,14 @@
 import TestGame.Metadata
 
-Game "Introduction"
-World "Tactic"
+Game "TestGame"
+World "TestWorld"
 Level 2
 
 Title "Definitionally equal"
 
 Introduction
 "
-Achtung: `refl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich
+Achtung: `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich
 definiert sind, auch wenn diese unterschiedlich dargestellt werden.
 So sind `1 + 1` und `2` per Definition das Gleiche, da sie beide von Lean als `0.succ.succ`
 gelesen werden.
@@ -16,7 +16,7 @@ gelesen werden.
 Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab.
 "
 
-Statement : 1 + 1 = 2 := by
+Statement "Zeige dass eins plus eins zwei ist." : 1 + 1 = 2 := by
   rfl
 
 Conclusion
diff --git a/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean
new file mode 100644
index 0000000..98acf4c
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Logic/L03_Assumption.lean
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 3
+
+Title "Annahmen"
+
+Introduction
+"
+Mathematische Aussagen haben Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine
+natürliche Zahl\", oder auch wahre Aussagen über diese Objekte, wie zum Beispiel
+\"und angenommen, dass `n` strikt grösser als `1` ist\".
+
+In Lean schreibt man beides mit dem gleichen Syntax: `(n : ℕ) (h : 1 < n)` definiert
+zuerst `n` als natürliche Zahl und kreeirt eien Annahme, dass `1 < n`. Dieser Annahme geben wir
+den Namen `h`.
+
+Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
+"
+
+Statement triviale_angelegenheit
+    "Angenommen `1 < n`. dann ist `1 < n`."
+    (n : ℕ) (h : 1 < n) : 1 < n := by
+  assumption
+
+Conclusion ""
+
+Tactics assumption
diff --git a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
new file mode 100644
index 0000000..33afcde
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+import Mathlib.Data.Nat.Basic -- TODO
+
+Game "TestGame"
+World "TestWorld"
+Level 4
+
+Title "Logische Aussagen: `Prop`"
+
+Introduction
+"
+Eine allgemeine logische Aussage definiert man mit `(A : Prop)`. Damit sagt man noch nicht,
+ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man an, dass
+`A` wahr ist: `hA` ist ein Beweis der Aussage `A`.
+"
+
+-- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
+Statement mehr_triviales
+    "
+    Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`.
+    Zeige, dass `A` wahr ist.
+    "
+    (A : Prop) (hA : A) : A := by
+  assumption
+
+Conclusion ""
+
+Tactics assumption
diff --git a/server/testgame/TestGame/Levels/Logic/004_Rewrite.lean b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
similarity index 53%
rename from server/testgame/TestGame/Levels/Logic/004_Rewrite.lean
rename to server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
index 752abd0..6b1329f 100644
--- a/server/testgame/TestGame/Levels/Logic/004_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean
@@ -1,23 +1,29 @@
 import TestGame.Metadata
 
-Game "Introduction"
-World "Tactic"
-Level 4
+Game "TestGame"
+World "TestWorld"
+Level 5
 
 Title "Rewrite"
 
 Introduction
 "
-Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern helfen einem
-nur, dorthin zu kommen.
+Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern man braucht
+mehrere Schritte im Beweis.
 
-Wenn man eine Annahme `(h : X = Y)` hat, die sagt, dass `X` und `Y` gleich sind,
+Wenn man eine Annahme `(h : X = Y)` hat die sagt, dass `X` und `Y` gleich sind,
 kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal
 das eine durch das andere zu ersetzen.
 "
 
-Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
-  rewrite [h₁]
+Statement umschreiben
+    "
+    Angenommen man hat die Gleichheiten
+    `a = b`, `a = d`, `c = d`.
+    Zeige dass `b = c`.
+    "
+    (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rw [h₁]
   rw [←h₂]
   assumption
 
@@ -35,16 +41,7 @@ Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h
 `(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."
 
 -- TODO: Muss ich das wirklich mehrmals auflisten?
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = a =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = b =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : c = c =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : d = d =>
+Message (x : ℕ) : x = x =>
 "Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
 anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
 
@@ -53,4 +50,4 @@ anstatt dem Goal."
 -- TODO: Das macht es doch unmöglich mit den Messages...
 
 Tactics assumption
---Tactics rw
+Tactics rw
diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
new file mode 100644
index 0000000..f97e330
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean
@@ -0,0 +1,33 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 6
+
+Title "Implikation"
+
+Introduction
+"
+Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und
+die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der
+Aussage `A`.
+
+Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Zeichen dafür:
+`A ↔ B` (`\\iff`) bedeutet \"Genau dann wenn\" und `A → B` (`\\to`) bedeutet \"`A` impliziert `B`\".
+
+Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man
+diese mit `apply h` anwenden.
+Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\".
+"
+
+Statement
+    "
+    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist.
+    "
+    (A B : Prop) (hA : A) (g : A → B) : B := by
+  apply g
+  assumption
+
+Tactics apply
+Tactics assumption
diff --git a/server/testgame/TestGame/Levels/StatementTest.lean b/server/testgame/TestGame/Levels/StatementTest.lean
new file mode 100644
index 0000000..3ec654a
--- /dev/null
+++ b/server/testgame/TestGame/Levels/StatementTest.lean
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "TestWorld"
+Level 1
+
+Title "Annahmen"
+
+Introduction "yadaa yadaa"
+
+class MyClass (n : ℕ) where
+
+Statement name
+"Beweise dieses Lemma."
+(n m : ℕ) : CommSemigroup ℕ where
+  mul := fun i j => 0
+  mul_comm := sorry
+  mul_assoc := sorry
+
+--@[exercise]
+instance instTest (n m : ℕ) : CommSemigroup ℕ where
+  mul := fun i j => 0
+  mul_comm := by
+    sorry
+  mul_assoc := by
+    sorry
+
+--@[exercise]
+lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rewrite [h₁]
+  rw [←h₂]
+  assumption
+
+
+Conclusion ""
+
+Tactics assumption
diff --git a/server/testgame/TestGame/Metadata.lean b/server/testgame/TestGame/Metadata.lean
index 6ae4946..ad6fb1c 100644
--- a/server/testgame/TestGame/Metadata.lean
+++ b/server/testgame/TestGame/Metadata.lean
@@ -1,7 +1,8 @@
 import GameServer.Commands
-import TestGame.MyNat
+--import TestGame.MyNat
 import TestGame.TacticDocs
 import TestGame.LemmaDocs
+import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ.
 
 Game "TestGame"
 
@@ -10,10 +11,10 @@ Title "The Natural Number Game"
 Introduction
 "This is a sad day for mathematics. While trying to find glorious new foundations for mathematics,
 someone removed the law of excluded middle and the axiom of choice. Unsurprisingly,
-everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage 
+everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage
 but now we need to rebuild all of mathematics from scratch.
 
-As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from 
+As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from
 the axioms that Giuseppe Peano found under the collapsed tower of number theory. You've been equipped
 with a level 1 spell book. Good luck."
 
@@ -21,4 +22,4 @@ Conclusion
 "There is nothing else so far. Thanks for rescuing natural numbers!"
 
 Path w1 → w2 → w3
-Path w1 → v2 → w3
\ No newline at end of file
+Path w1 → v2 → w3
diff --git a/server/testgame/TestGame/MyNat.lean b/server/testgame/TestGame/MyNat.lean
index d30eff2..3cecede 100644
--- a/server/testgame/TestGame/MyNat.lean
+++ b/server/testgame/TestGame/MyNat.lean
@@ -1,6 +1,6 @@
 axiom MyNat : Type
 
-notation "ℕ" => MyNat
+--notation "ℕ" => MyNat
 
 --axiom zero : ℕ
 
@@ -17,4 +17,3 @@ axiom add_zero : ∀ a : ℕ, a + 0 = a
 axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)
 
 @[elab_as_elim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n
-
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index ef87ba7..f3b051e 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -82,6 +82,12 @@ TODO
 "
 
 
+TacticDoc apply
+"
+## Beschreibung
+
+TODO
+"
 
 
 
diff --git a/server/testgame/TestGame/Tactics.lean b/server/testgame/TestGame/Tactics.lean
index 31016d1..5e95bfc 100644
--- a/server/testgame/TestGame/Tactics.lean
+++ b/server/testgame/TestGame/Tactics.lean
@@ -1,5 +1,5 @@
 import Lean
-import TestGame.MyNat
+-- import TestGame.MyNat
 
 open Lean Elab Tactic
 
@@ -8,5 +8,5 @@ elab "swap" : tactic => do
   | g₁::g₂::t => setGoals (g₂::g₁::t)
   | _ => pure ()
 
--- macro "induction_on" n:ident : tactic => 
--- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
\ No newline at end of file
+-- macro "induction_on" n:ident : tactic =>
+-- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
diff --git a/server/testgame/lakefile.lean b/server/testgame/lakefile.lean
index ff10607..9be3d46 100644
--- a/server/testgame/lakefile.lean
+++ b/server/testgame/lakefile.lean
@@ -3,6 +3,9 @@ open Lake DSL
 
 require GameServer from ".."/"leanserver"
 
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"@"b1cf06cb126ee163a7dc895c1aee17946ff20900"
+
 package TestGame
 
 @[default_target]