lemma docs and levels

server/testgame/TestGame/Levels/LinearAlgebra.lean

@@ -25,6 +25,13 @@ Game "TestGame"
 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 "TestGame"
 World "Basis"
 Title "Lineare Abbildungen"

server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean

@@ -3,6 +3,7 @@ import TestGame.Metadata
 import Mathlib.Data.Real.Basic      -- definiert `ℝ`
 import Mathlib.Algebra.Module.Basic -- definiert `module`
 import Mathlib.Tactic.LibrarySearch
+import TestGame.StructInstWithHoles
 
 set_option tactic.hygienic false
 
@@ -14,9 +15,6 @@ Title "Module"
 
 Introduction
 "
-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 auch \"Vektorraum\" genannt.
 Konkret heisst das:
 
 Sei `R` ein Ring. Ein `R`-Modul ist eine kommutative Gruppe `(V, +)` zusammen mit
@@ -29,63 +27,75 @@ Eigenschaften beliebige `(r s : R)` und `(v w : V)`erfüllt:
 - `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.
 "
 
+-- 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
-  refine {
-    smul := fun a r => ↑a * r
-    smul_zero := ?smul_zero
-    zero_smul := ?zero_smul
-    one_smul := ?one_smul
-    smul_add := ?smul_add
-    add_smul := ?add_smul
-    mul_smul := ?mul_smul }
+  Hint "**Robo**: Als erstes willst du die Stuktur `Modul` aufteilen in einzelne Beweise.
+  Der Syntax dafür ist:
 
-  · intro b
+  ```
+  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
-    rw [Rat.cast_one, one_mul]
+    Hint "**Robo**: Den Teil kannst du mit `simp` beweisen."
+    simp
   · intro x y b
+    Hint "**Robo**: Benutze `change` um `•` durch `*` zu ersetzen."
     change (x * y : ℚ) * b = x * (y * b)
-    rw [Rat.cast_mul, mul_assoc]
+    Hint "**Robo**: Mit `simp` und `ring` kannst du den Rest beweisen."
+    simp
+    ring
   · intro a
-    rw [smul_zero]
+    simp
   · intro a x y
     change a * (x + y) = a * x + a * y
-    rw [mul_add]
+    ring
   · intro r s x
     change (r + s : ℚ) * x = r * x + s * x
-    rw [Rat.cast_add, add_mul]
+    simp
+    ring
   · intro a
     change (0 : ℚ) * a = 0
     simp
+
+NewTactic refine exact change