nothin of importance

server/testgame/TestGame/Levels/Prime/L02_Prime.lean

@@ -0,0 +1,51 @@
+import TestGame.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 TestGame.ToBePorted
+
+Game "TestGame"
+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/testgame/TestGame/Levels/Prime/L03_Prime.lean

@@ -0,0 +1,41 @@
+import TestGame.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 TestGame.ToBePorted
+
+Game "TestGame"
+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