From 10a12a8e77c59bdfb3f6db3ea34d4fbd14cc6f95 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 22 Mar 2023 15:49:05 +0100
Subject: [PATCH] lemma docs and levels

---
 server/testgame/TestGame.lean                 |   2 +-
 server/testgame/TestGame/LemmaDocs.lean       | 181 ++++++------------
 .../TestGame/Levels/LinearAlgebra.lean        |   7 +
 .../Levels/LinearAlgebra/L01_Module.lean      |  98 +++++-----
 .../TestGame/StructInstWithHolesTest.lean     |   5 +-
 server/testgame/TestGame/TacticDocs.lean      |  37 ++++
 6 files changed, 161 insertions(+), 169 deletions(-)

diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index 1574cc3..ea0d890 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -34,7 +34,7 @@ Path Predicate → Inequality → Sum
 -- Path Inequality → Prime
 -- Path Sum → Inequality -- → Induction
 
-Path Lean → SetTheory → SetTheory2 → SetFunction
+Path Lean → SetTheory → SetTheory2 → SetFunction → Module
 Path Lean → Function → SetFunction
 
 
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index 52e7a61..2166bd9 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -84,9 +84,6 @@ This lemma says `∀ a : ℕ, a + 0 = a`.
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
 * Mathlib Doc"
 
 LemmaDoc add_succ as "add_succ" in "Addition"
@@ -94,9 +91,6 @@ LemmaDoc add_succ as "add_succ" in "Addition"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
 * Mathlib Doc: [#]()"
 
 LemmaDoc not_forall as "not_forall" in "Logic"
@@ -223,6 +217,7 @@ LemmaDoc Subset.antisymm_iff as "Subset.antisymm_iff" in "Set"
 `Set.Subset.antisymm_iff {α : Type u} {a : Set α} {b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a`
 
 Zwei Mengen sind identisch, wenn sowohl $A \\subseteq B$ wie auch $B \\subseteq A$.
+
 ## Details
 
 `rw [Subset.antisymm_iff]` ist eine Möglichkeit Gleichungen von Mengen zu zeigen.
@@ -240,60 +235,57 @@ für eine verwandte Version.
 "
 
 
-LemmaDoc Nat.prime_def_lt'' as "Nat.prime_def_lt''" in "Nat"
+LemmaDoc Nat.prime_def_lt'' as "prime_def_lt''" in "Nat"
 "
+`Nat.prime_def_lt'' {p : ℕ} :
+Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p`
+
+Die bekannte Definition einer Primmzahl in `ℕ`: Eine Zahl (`p ≥ 2`) mit genau zwei Teilern.
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* `simp`-Lemma: Nein
+* Namespace: `Nat`
+* Mathlib Doc: [#Nat.prime_def_lt''](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html#Nat.prime_def_lt'')
 "
 
 
-LemmaDoc Finset.sum_add_distrib as "Finset.sum_add_distrib" in "Sum"
+LemmaDoc Finset.sum_add_distrib as "sum_add_distrib" in "Sum"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* `simp`-Lemma: Nein
+* Namespace: `Finset`
+* Mathlib Doc: [#Finset.sum_add_distrib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Basic.html#Finset.sum_add_distrib)
 "
 
-LemmaDoc Fin.sum_univ_castSucc as "Fin.sum_univ_castSucc" in "Sum"
+LemmaDoc Fin.sum_univ_castSucc as "sum_univ_castSucc" in "Sum"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* `simp`-Lemma: Nein
+* Namespace: `Fin`
+* Mathlib Doc: [#sum_univ_castSucc](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Fin.html#Fin.sum_univ_castSucc)
 "
 
-LemmaDoc Nat.succ_eq_add_one as "Nat.succ_eq_add_one" in "Sum"
+LemmaDoc Nat.succ_eq_add_one as "succ_eq_add_one" in "Sum"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* `simp`-Lemma: Nein
+* Namespace: `Nat`
+* Mathlib Doc: [#succ_eq_add_one](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Basic.html#Nat.succ_eq_add_one)
 "
 
-LemmaDoc Nat.zero_eq as "Nat.succ_eq_add_one" in "Sum"
+LemmaDoc Nat.zero_eq as "zero_eq" in "Sum"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#zero_eq](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Basic.html#Nat.zero_eq)
 "
 
 LemmaDoc add_comm as "add_comm" in "Nat"
@@ -301,10 +293,7 @@ LemmaDoc add_comm as "add_comm" in "Nat"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#add_comm](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#add_comm)
 "
 
 LemmaDoc mul_add as "mul_add" in "Nat"
@@ -312,10 +301,7 @@ LemmaDoc mul_add as "mul_add" in "Nat"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#mul_add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Ring/Defs.html#mul_add)
 "
 
 LemmaDoc add_mul as "add_mul" in "Nat"
@@ -323,10 +309,7 @@ LemmaDoc add_mul as "add_mul" in "Nat"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#add_mul](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Ring/Defs.html#add_mul)
 "
 
 LemmaDoc arithmetic_sum as "arithmetic_sum" in "Sum"
@@ -334,10 +317,7 @@ LemmaDoc arithmetic_sum as "arithmetic_sum" in "Sum"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Not a mathlib lemma.
 "
 
 LemmaDoc add_pow_two as "add_pow_two" in "Nat"
@@ -345,10 +325,7 @@ LemmaDoc add_pow_two as "add_pow_two" in "Nat"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#add_pow_two](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Ring.html#add_pow_two)
 "
 
 LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum"
@@ -356,10 +333,7 @@ LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#sum_comm](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Basic.html#Finset.sum_comm)
 "
 
 LemmaDoc Function.comp_apply as "Function.comp_apply" in "Function"
@@ -367,10 +341,7 @@ LemmaDoc Function.comp_apply as "Function.comp_apply" in "Function"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#comp_apply](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Function.comp_apply)
 "
 
 LemmaDoc not_le as "not_le" in "Logic"
@@ -378,10 +349,7 @@ LemmaDoc not_le as "not_le" in "Logic"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#not_le](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Algebra/Order.html#not_le)
 "
 
 LemmaDoc if_pos as "if_pos" in "Logic"
@@ -389,10 +357,7 @@ LemmaDoc if_pos as "if_pos" in "Logic"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#if_pos](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#if_pos)
 "
 
 LemmaDoc if_neg as "if_neg" in "Logic"
@@ -400,10 +365,7 @@ LemmaDoc if_neg as "if_neg" in "Logic"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#if_neg](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#if_neg)
 "
 
 LemmaDoc StrictMono.injective as "StrictMono.injective" in "Function"
@@ -411,10 +373,7 @@ LemmaDoc StrictMono.injective as "StrictMono.injective" in "Function"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#StrictMono.injective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Basic.html#StrictMono.injective)
 "
 
 LemmaDoc StrictMono.add as "StrictMono.add" in "Function"
@@ -422,10 +381,7 @@ LemmaDoc StrictMono.add as "StrictMono.add" in "Function"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#StrictMono.add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Monoid/Lemmas.html#StrictMono.add)
 "
 
 LemmaDoc Odd.strictMono_pow as "Odd.strictMono_pow" in "Function"
@@ -433,10 +389,7 @@ LemmaDoc Odd.strictMono_pow as "Odd.strictMono_pow" in "Function"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#Odd.strictMono_pow](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Odd.strictMono_pow)
 "
 
 LemmaDoc Exists.choose as "Exists.choose" in "Function"
@@ -444,10 +397,7 @@ LemmaDoc Exists.choose as "Exists.choose" in "Function"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#Exists.choose](https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#Exists.choose)
 "
 
 LemmaDoc Exists.choose_spec as "Exists.choose_spec" in "Function"
@@ -455,30 +405,21 @@ LemmaDoc Exists.choose_spec as "Exists.choose_spec" in "Function"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#Exists.choose_spec](https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#Exists.choose_spec)
 "
 LemmaDoc congrArg as "congrArg" in "Function"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#congrArg](https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#congrArg)
 "
 LemmaDoc congrFun as "congrFun" in "Function"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#congrFun](https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#congrFun)
 "
 
 LemmaDoc Iff.symm as "Iff.symm" in "Logic"
@@ -486,10 +427,7 @@ LemmaDoc Iff.symm as "Iff.symm" in "Logic"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#Iff.symm](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff.symm)
 "
 
 
@@ -502,16 +440,14 @@ DefinitionDoc Even as "Even"
 Die Definition kann man mit `unfold even at *` einsetzen.
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()"
+* Mathlib Doc: [#Even](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Even)"
 
 DefinitionDoc Odd as "Odd"
 "
 `odd n` ist definiert als `∃ r, a = 2 * r + 1`.
 Die Definition kann man mit `unfold odd at *` einsetzen.
-"
+
+* Mathlib Doc: [Odd](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Odd)"
 
 DefinitionDoc Injective as "Injective"
 "
@@ -521,7 +457,8 @@ DefinitionDoc Injective as "Injective"
 ∀ a b, f a = f b → a = b
 ```
 definiert.
-"
+
+* Mathlib Doc: [Injective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Injective)"
 
 DefinitionDoc Surjective as "Surjective"
 "
@@ -530,17 +467,15 @@ DefinitionDoc Surjective as "Surjective"
 ```
 ∀ a, (∃ b, f a = b)
 ```
-"
+
+* Mathlib Doc: [Surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Surjective)"
 
 DefinitionDoc Bijective as "Bijective"
 "
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#Bijective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Bijective)
 "
 
 DefinitionDoc LeftInverse as "LeftInverse"
@@ -548,10 +483,7 @@ DefinitionDoc LeftInverse as "LeftInverse"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#LeftInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.LeftInverse)
 "
 
 DefinitionDoc RightInverse as "RightInverse"
@@ -559,10 +491,7 @@ DefinitionDoc RightInverse as "RightInverse"
 
 ## Eigenschaften
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+* Mathlib Doc: [#RightInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Logic.html#RightInverse)
 "
 
 DefinitionDoc StrictMono as "StrictMono"
@@ -573,7 +502,13 @@ DefinitionDoc StrictMono as "StrictMono"
 ∀ a b, a < b → f a < f b
 ```
 
+## Eigenschaften
+
+* Mathlib Doc: [#StrictMono](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Basic.html#StrictMono)
+
 "
 
+DefinitionDoc Symbol.Subset as "⊆" "
 
-DefinitionDoc Symbol.Subset as "⊆" "Test"
+Auf Mengen (`Set`) ist `A ⊆ B` als `∀x, x ∈ A → x ∈ B` implementiert.
+"
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra.lean b/server/testgame/TestGame/Levels/LinearAlgebra.lean
index 676e2db..6054c79 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra.lean
+++ b/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"
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean b/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
index b471da9..b37f4ae 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
+++ b/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]`
+-- 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:
+-- 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.
-"
+-- ```
+-- 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
diff --git a/server/testgame/TestGame/StructInstWithHolesTest.lean b/server/testgame/TestGame/StructInstWithHolesTest.lean
index b8e07bf..fe0436c 100644
--- a/server/testgame/TestGame/StructInstWithHolesTest.lean
+++ b/server/testgame/TestGame/StructInstWithHolesTest.lean
@@ -3,7 +3,10 @@ import Mathlib
 
 
 example : Module ℚ ℝ := by
-  refine { smul := fun a r => ↑a * r  ?..! }
+  refine { ?..! }
+  exact fun a r => a * r
+  intro b
+  sorry
   sorry
   sorry
   sorry
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index 63501b5..49d56b8 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -90,6 +90,28 @@ widersprechen.
 in ähnlichen Situationen nutzbar wie `by_contra`
 "
 
+TacticDoc change
+"
+`change t` ändert das Goal zu `t`. Voraussetzung ist, dass `t` und das alte Goal defEq sind.
+
+## Details
+
+Dies ist insbesonder hilfreich wenn eine Taktik nicht merkt, dass das Goal defEq ist zu einem
+Term, der eigentlich gebraucht würde.
+
+## Beispiel
+
+Aktuelles Goal:
+
+```
+b: ℝ
+⊢ 1 • b = b
+```
+Wobei die Skalarmultiplikation als `fun (a : ℚ) (r : ℝ) => ↑a * r` definiert war. Dann
+kann man mit `change (1 : ℚ) * b = b` das Goal umschreiben und anschliessend mit Lemmas
+über die Multiplikation beweisen.
+"
+
 TacticDoc constructor
 "
 `constructor` teilt ein Goal auf, wenn das Goal eine Struktur ist
@@ -157,6 +179,11 @@ eine Beweis durch Kontraposition.
   `contrapose` verwendet.
 "
 
+TacticDoc exact
+"
+`exact h` schliesst das Goal wenn der Term `h` mit dem Goal übereinstimmt.
+"
+
 TacticDoc fin_cases
 "
 `fin_cases i` führt eine Fallunterscheidung wenn `i` ein endlicher Typ ist.
@@ -332,6 +359,16 @@ erzeugen, einmal unter Annahme der linken Seite, einmal unter Annahme der Rechte
   freien Variablen
 "
 
+TacticDoc refine
+"
+`refine { ?..! }` wird benötigt um eine Struktur (z.B. ein $R$-Modul) im Taktikmodus in einzelne
+Goals aufzuteilen. Danach hat man ein Goal pro Strukturfeld.
+
+(*Bemerkung*: Es gibt in Lean verschiedenste bessere Varianten dies zu erreichen,
+z.B. \"Term Modus\" oder \"anonyme Konstruktoren\", aber für den Zweck des Spieles bleiben wir
+bei diesem Syntax.)
+"
+
 TacticDoc revert
 "
 `revert h` fügt die Annahme `h` als Implikationsprämisse vorne ans Goal an.