diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index 8bd7a6c..dd5d26b 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -1,300 +1,524 @@
 import GameServer.Commands
-
 import TestGame.Tactics
 
-TacticDoc rfl
+TacticDoc assumption
 "
-## Beschreibung
+`assumption` sucht nach einer Annahme, die genau dem Goal entspricht.
 
-`rfl` beweist ein Goal der Form `X = X`.
+## Beispiel
 
-## Detail
+`assumption` sucht durch die Annahmen und merkt dass `h` genau mit dem Goal übereinstimmt.
+
+```
+Objekte
+  a b c d : ℕ
+  h : a + b = c
+  g : a * b = 16
+  t : c = 12
+Goal
+  a + b = c
+```
+"
+
+TacticDoc apply
+"
+`apply my_lemma` Versucht das Goal mit der Aussage des Lemmas zu unifizieren
+und erstellt ein neues Goal pro Annahme des Lemmas, die noch zu zeigen ist.
 
-`rfl` beweist jedes Goal `A = B` wenn `A` und `B` genau das gleiche sind.
-Wichtig ist nicht, ob diese im Infoview gleich aussehen, sondern ob sie in
-Lean gleich definiert sind.
+## Details
+`apply` funktioniert gleichermassen für Lemmas wie für Implikationen
+wie z.B. `(h : A → B)`.
 
 ## Beispiel
-`rfl` kann folgenes Goal beweisen:
+
+Gegeben folgendes Lemma:
 ```
-Objects
-  a b c : ℕ
-Prove:
-  (a + b) * c = (a + b) * c
+lemma Nat.eq_zero_of_le_zero {n : ℕ} (h : n ≤ 0) : n = 0 := by sorry
 ```
 
-`rfl` kann auch folgendes beweisen:
+Und folgendes Problem:
+
 ```
-Objects
+
+Objekte
   n : ℕ
-Prove:
-  1 + 1 = 2
+  ...
+Goal
+  n = 0
 ```
-denn Lean liest dies intern als `0.succ.succ = 0.succ.succ`.
+
+Hier ändert `apply Nat.eq_zero_of_le_zero` das Goal zu `n ≤ 0` durch Anwendung
+des Lemmas.
 "
 
-TacticDoc assumption
+TacticDoc by_cases
 "
-## Beschreibung
+`by_cases h : P` macht eine Fallunterscheidung. Im ersten Goal wird eine Annahme
+`(h : P)` hinzugefügt, im zweiten `(h : ¬P)`.
 
-`assumption` sucht nach einer Annahme, die genau dem Goal entspricht.
+## Details
+
+`P` kann eine beliegige Aussage sein, die als entweder wahr oder falsch angenommen wird.
 
 ## Beispiel
-Wenn das Goal wie folgt aussieht:
+
 ```
-Objects
-  a b c d : ℕ
-  h : a + b = c
-  g : a * b = 16
-  t : c = 12
-Prove:
-  a + b = c
+example (A : Prop) : A ∨ ¬ A := by
+  by_cases h : A
+  · left
+    assumption
+  · right
+    assumption
 ```
+"
 
-dann findet `assumption` die Annahme `h`und schliesst den Beweis.
+TacticDoc by_contra
 "
+`by_contra h` startet einen Widerspruchsbeweis.
+
+## Details
+Sei `P` das aktuelle Goal. `by_contra h` fügt eine neue Annahme `(h : ¬P)` hinzu
+und setzt das Goal auf `False`.
 
-TacticDoc rewrite
+Oft will man `by_contra` nutzen wenn das Goal von der Form `¬ P` ist.
+
+## Hilfreiche Resultate
+
+* `contradiction` schliesst den Widerspruchsbeweis wenn sich (zwei) Annahmen
+widersprechen.
+* `contrapose` führt einen Beweis durch Kontraposition und ist entsprechend
+in ähnlichen Situationen nutzbar wie `by_contra`
 "
-## Beschreibung
 
-Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
+TacticDoc constructor
 "
+`constructor` teilt ein Goal auf, wenn das Goal eine Struktur ist
 
-TacticDoc induction
+## Detail
+Wenn das Goal eine Struktur ist, wie z.B. `A ∧ B` welches zwei Felder hat `⟨A, B⟩`, dann
+erzeugt `constructor` ein Goal pro Feld der Struktur.
+
+## Hilfreiche Resultate
+
+* Das Gegenteil von `constructor` ist `⟨_, _⟩` (`\\<>`), der *anonyme Konstructor*.
+Dieser enspricht ungefähr der Tupel-Notation in
+\"eine Gruppe ist ein Tupel $(G, 0, +)$, sodass …\".
+
+## Beispiel
+
+```
+example {A B : Prop} (h : A) (g : B) : A ∧ B := by
+  constructor
+  · assumption
+  · assumption
+```
 "
-## Beschreibung
 
-Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
+TacticDoc contradiction
 "
+`contradiction` schliesst den Beweis wenn es einen Widerspruch in den Annahmen findet.
 
+## Details
+Ein Widerspruch in den Annahmen kann unter anderem folgendermassen aussehen:
 
-TacticDoc linarith
+* `(h : n ≠ n)`
+* `(h : A)` und `(h' : ¬A)`
+* `(h : False)` (i.e. ein Beweis von `False`)
+
+## Beispiel
+
+Folgenes Goal wird von `contradiction` bewiesen
+
+## Hilfreiche Resultate
+
+* Normalerweise wird `contradiction` gebraucht um einen Widerspruchsbeweis zu
+  schliessen, der mit `by_contra` eröffnet wurde.
+* Ein Beweis von `False` representiert in Lean einen Widerspruch.
+
+```
+Objekte:
+  (n m : ℕ)
+  (h : n = m)
+  (g : n ≠ m)
+Goal
+  37 = 60
+```
+nach dem Motto \"ein Widerspruch beweist alles.\"
 "
-## Beschreibung
 
+TacticDoc contrapose
+"
+`contrapose` ändert ein Goal der Form `A → B` zu `¬B → ¬A` und führt damit
+eine Beweis durch Kontraposition.
+
+## Hilfreiche Resultate
+
+* `revert h` kann nützlich sein um eine Annahme als Implikationsprämisse zu schreiben bevor man
+  `contrapose` verwendet.
 "
 
 TacticDoc fin_cases
 "
-## Beschreibung
+`fin_cases i` führt eine Fallunterscheidung wenn `i` ein endlicher Typ ist.
 
+## Details
+`fin_cases i` ist insbesondere nützlich für `(i : Fin n)`, zum Beispiel als Index in
+endlich dimensionalen Vektorräumen.
+
+In diesem Fall bewirkt `fin_cases i` dass man Komponentenweise arbeitet.
 "
 
 TacticDoc funext
 "
-## Beschreibung
+`funext x` wird bei Gleichungen von Funktionen `f = g` gebraucht. Das Goal wird zu
+`f x = g x`.
+
+## Details
+Nach dem Motto `f = g ↔ ∀ x, f x = g x` sind zwei Funktionen dann identisch, wenn sie
+angewendet auf jedes Element identisch sind. `funext x` benützt dieses Argument.
+"
 
+TacticDoc «have»
 "
+`have h : P` führt ein Zwischenresultat ein.
 
+## Details
+Anschliessend muss man zuerst dieses Zwischenresultat beweisen bevor man mit dem Beweis
+weitermachen und das Zwischenresultat verwenden kann.
 
-TacticDoc rw
+## Hilfreiche Resultate
+
+* `suffices h : P` funktioniert genau gleich, aussert das die beiden entstehenden Beweise
+  vertauscht sind.
+* `let h : Prop := A ∧ B` ist verwandt mit `have`, mit Unterschied, dass man mit `let`
+  eine temporäre Definition einführt.
 "
-## Beschreibung
 
-Wenn man eine Annahme `(h : X = Y)` hat, kann man mit
-`rw [h]` alle `X` im Goal durch `Y` ersetzen.
+TacticDoc induction
+"
+`induction n` führt einen Induktionsbeweis über `n`.
 
 ## Detail
-- `rw [←h]` wendet `h` rückwärts an und ersetzt alle `Y` durch `X`.
-- `rw [h, g, ←f]`: Man kann auch mehrere `rw` zusammenfassen.
-- `rw [h] at h₂` ersetzt alle `X` in `h₂` zu `Y` (anstatt im Goal).
 
-`rw` funktioniert gleichermassen mit Annahmen `(h : X = Y)` also auch
-mit Theoremen/Lemmas der Form `X = Y`
+Diese Taktik erstellt zwei Goals:
+* Induktionsanfang, wo `n = 0` ersetzt wird.
+* Induktionsschritt, in dem man die Induktionshypothese `n_ih` zur Verfügung hat.
+
+Der volle Syntax mit Option zum umbenennen der Induktionshypothes und -variable ist
+
+```
+induction n with
+| zero =>
+  sorry
+| succ m m_ih =>
+  sorry
+```
+
+da dieser sich über mehrere Zeilen erstreckt wird er im Spiel nicht eingeführt.
+
+## Hifreiche Resultate
+
+* `Nat.succ_eq_add_one`: schreibt `n.succ = n + 1` um.
+* `Nat.zero_eq`: schreibt `Nat.zero = 0` um.
+
+Beide sind DefEq, aber manche Taktiken können nicht damit umgehen
+
+* Siehe Definition `∑` für Hilfe mit Induktion über Summen.
+* `rcases n` ist sehr ähnlich zu `induction n`. Der Unterschied ist, dass bei
+`rcases` keine Induktionshypothese im Fall `n + 1` zur Verfügung steht.
 
 ## Beispiel
 
-TODO
+```
+example (n : ℕ) : 4 ∣ 5^n + 7 := by
+  induction n
+  sorry      -- Fall `n = 0`
+  sorry      -- Fall `n + 1`
+```
 "
 
-TacticDoc simp_rw
+TacticDoc intro
 "
-## Beschreibung
+`intro x` wird für Goals der Form `A → B` oder `∀ x, P x` verwendet.
+Dadurch wird die Implikationsprämisse (oder das Objekt `x`) den Annahmen hinzugefügt.
 
-TODO
+## Hilfreiche Resultate
+
+* `revert h` macht das Gegenteil von `intro`.
 "
 
-TacticDoc by_cases
+TacticDoc left
 "
-## Beschreibung
+Wenn das Goal von der Form `A ∨ B` ist, enscheidet man mit `left` die linke Seite zu zeigen.
 
-TODO
+## Hilfreiche Resultate
+
+* `right` entscheidet sich für die linke Seite.
 "
 
-TacticDoc apply
+TacticDoc «let»
 "
-## Beschreibung
+`let x : ℕ := 5 ^ 2` führt eine neue temporäre Definition ein.
 
-TODO
+## Hilfreiche Resultate
+
+* `have x : ℕ := 5 ^ 2` führt ebenfalls eine neue natürliche Zahle `x` ein, aber
+  Lean vergisst sofort, wie die Zahl definiert war. D.h. `x = 25` wäre dann nicht
+  beweisbar. Mit `let x : ℕ := 5 ^ 2` ist `x = 25` durch `rfl` beweisbar.
 "
 
-TacticDoc constructor
+TacticDoc linarith
 "
-## Beschreibung
+`linarith` löst Systeme linearer (Un-)Gleichungen.
 
-TODO
+## Detail
+`linarith` kann lineare Gleichungen und Ungleichungen beweisen indem
+es das Gegenteil vom Goal annimmt und versucht einen Widerspruch in den
+Annahmen zu erzeugen (Widerspruchsbeweis). Es braucht ein `≤` definiert um
+zu funktionieren.
+
+## Beispiel
+
+Folgendes kann `linarith` beweisen.
+```
+Objekte
+  x y : ℤ
+  h₁ : 5 * y ≤ 35 - 2 * x
+  h₂ : 2 * y ≤ x + 3
+Goal
+  y ≤ 5
+```
 "
 
-TacticDoc tauto
+TacticDoc push_neg
 "
-## Beschreibung
+`push_neg` schreibt `¬∀ x, _` zu `∃ x, ¬ _` und `¬∃ x, _` zu `∀x, ¬ _` um.
 
-TODO
+## Details
+
+`psuh_neg` schiebt das `¬` soweit nach innen wie möglich.
+
+## Hilfreiche Resultate
+
+* Die beiden Lemmas heissen `not_forall` und `not_exists` und können mit `rw` einzeln angewendet
+  werden.
 "
 
 TacticDoc rcases
 "
-## Beschreibung
+`rcases h` teilt eine Annahme `h` in ihre Einzelteile auf.
 
-TODO
-"
+## Details
+Für Annahmen die Strukturen sind, wie z.B. `h : A ∧ B` (oder `∃x, P x`) kann man die
+Einzelteile mit  `rcases h with ⟨a, b⟩` (oder `rcases h with ⟨x, hx⟩`) benennen.
 
-TacticDoc left
-"
-## Beschreibung
+Für eine Annahme der Form `h : A ∨ B` kann man mit `rcases h with ha | hb` zwei Goals
+erzeugen, einmal unter Annahme der linken Seite, einmal unter Annahme der Rechten.
 
-TODO
-"
+## Hilfreiche Resultate
 
-TacticDoc right
+* Für `n : ℕ` hat `rcases n` einen ähnlichen Effekt wie `induction n` mit dem Unterschied,
+  dass im Fall `n + 1` keine Induktionshypothese zur Verfügung steht.
+* In Lean gibt es auch die Taktik `cases`, die gleich funktioniert wie `rcases` aber
+  einen mehrzeiligen Syntax hat:
+  ```
+  cases h with
+  | inl ha =>
+    sorry
+  | inr hb =>
+    sorry
+  ```
+  Hier sind `inl`/`inr` die Namen der Fälle und `ha`/`hb` sind frei gewählte Namen für die
+  freien Variablen
 "
-## Beschreibung
 
-TODO
+TacticDoc revert
 "
+`revert h` fügt die Annahme `h` als Implikationsprämisse vorne ans Goal an.
 
-TacticDoc simp
-"
-## Beschreibung
+## Hilfreiche Resultate
 
-TODO
-"
+* `revert` ist das Gegenteil von `intro`.
+* `revert` kann insbesondere nützlich sein, um anschliessend `contrapose` zu verwenden.
 
-TacticDoc trivial
-"
-## Beschreibung
+## Beispiel
 
-TODO
-"
+```
+Objekte
+  A P : Prop
+  h : P
+Goal
+  A
+```
 
-TacticDoc contradiction
-"
-## Beschreibung
+hier ändert `revert h` den Status zu
 
-TODO
+```
+Objekte
+  A P : Prop
+Goal
+  P → A
+```
 "
 
-TacticDoc push_neg
+TacticDoc rfl
 "
-## Beschreibung
+`rfl` beweist ein Goal der Form `X = X`.
 
-TODO
-"
+## Detail
 
+`rfl` beweist jedes Goal `A = B` wenn `A` und `B` per Definition das gleiche sind (DefEq).
+Andere Taktiken rufen `rfl` oft am Ende versteckt
+automatisch auf um zu versuchen, den Beweis zu schliessen.
 
-TacticDoc contrapose
+
+## Beispiel
+`rfl` kann folgende Goals beweisen:
+
+```
+Objekte
+  a b c : ℕ
+Goal:
+  (a + b) * c = (a + b) * c
+```
+
+```
+Objekte
+  n : ℕ
+Goal
+  1 + 1 = 2
+```
+denn Lean liest dies intern als `0.succ.succ = 0.succ.succ`.
 "
-## Beschreibung
 
-TODO
+TacticDoc right
 "
+Wenn das Goal von der Form `A ∨ B` ist, enscheidet man mit `right` die rechte Seite zu zeigen.
 
-TacticDoc revert
+## Hilfreiche Resultate
+
+* `left` entscheidet sich für die linke Seite.
 "
-## Beschreibung
 
-TODO
+TacticDoc ring
 "
+Löst Gleichungen mit den Operationen `+, -, *, ^`.
 
+## Details
+Insbesondere funktioniert `ring` in Ringen/Semiringen wie z.B. `ℕ, ℤ, ℚ, …`
+(i.e. Typen `R` mit Instanzen `Ring R` oder `Semiring R`).
+Die Taktik ist besonders auf kommutative Ringe (`CommRing R`) ausgelegt.
 
-TacticDoc by_contra
-"
-## Beschreibung
+## Hilfreiche Resultate
 
-TODO
+* `ring` kann nicht wirklich mit Division (`/`) oder Inversen (`⁻¹`) umgehen. Dafür ist die
+  Taktik `field_simp` gedacht, und die typische Sequenz ist
+  ```
+  field_simp
+  ring
+  ```
+* Wenn `ring` nicht abschliesst, sagt es man solle `ring_nf` verwenden. Normalerweise heisst
+  das aber, dass man was falsch gemacht hat und die Seiten der Gleichung noch nicht gleich sind.
 "
 
-TacticDoc ring
+TacticDoc rw
 "
-## Beschreibung
+Wenn man eine Annahme `(h : X = Y)` hat, kann man mit
+`rw [h]` alle `X` im Goal durch `Y` ersetzen.
 
-TODO
+## Details
+
+* `rw [←h]` wendet `h` rückwärts an und ersetzt alle `Y` durch `X`.
+* `rw [h, g, ←f]`: Man kann auch mehrere `rw` zusammenfassen.
+* `rw [h] at h₂` ersetzt alle `X` in `h₂` zu `Y` (anstatt im Goal).
+
+`rw` funktioniert gleichermassen mit Annahmen `(h : X = Y)` also auch
+mit Theoremen/Lemmas der Form `X = Y`
 "
 
-TacticDoc unfold
+TacticDoc simp
 "
-## Beschreibung
+`simp` versucht alle Vereinfachungslemmas anzuwenden, die in der `mathlib` mit `@[simp]`
+gekennzeichnet sind.
 
-TODO
+## Details
+
+* `simp?` zeigt welche Lemmas verwendet wurden.
+* `simp [my_lemma]` fügt zudem `my_lemma` temporär zur Menge der `simp`-Lemmas hinzu.
+* ein `simp`, das nicht am Ende des Beweis steht sollte durch eine entsprechende
+  `simp only [...]` Aussage ersetzt werden, um den Beweis stabiler zu machen.
 "
 
-TacticDoc use
+TacticDoc simp_rw
 "
-## Beschreibung
+`simp_rw [h₁, h₂, h₃]` versucht wie `rw` jedes Lemma der Reihe nach zu Umschreiben zu verwenden,
+verwendet aber jedes Lemma so oft es kann.
 
-TODO
+## Details
+
+Es bestehen aber drei grosse Unterschiede zu `rw`:
+
+* `simp_rw` wendet jedes Lemma so oft an wie es nur kann.
+* `simp_rw` kann besser unter Quantifiern umschreiben als `rw`.
+* `simp_rw` führt nach jedem Schritt ein `simp only []` aus und vereinfacht dadurch grundlegenste
+  Sachen.
 "
 
 TacticDoc «suffices»
 "
-## Beschreibung
+`suffices h : P` führt ein neues Zwischenresultat ein, aus dem das Goal direkt folgen soll.
 
-TODO
-"
+## Details
 
-TacticDoc «have»
-"
-## Beschreibung
+Der einzige Unterschied zu `have h : P` ist, dass die beiden resultierenden Goals vertauscht sind.
 
-TODO
+Mathematisch braucht man diese in ein bisschen unterschiedlichen Fällen:
+
+* `suffices h : P` : \"Es genügt zu zeigen, dass …\". Als erstes folgt die Erklärung wieso
+  das genügt, danach muss man nur noch `P` beweisen.
+* `have h : P` : Ein (kleines) Zwischenresultat. Als erstes folgt dann der Beweis dieses
+Resultats, anschliessend setzt man den Beweis mit Hilfe des Zwischenresultats fort.
 "
 
-TacticDoc «let»
+TacticDoc tauto
 "
 ## Beschreibung
 
 TODO
 "
 
-TacticDoc induction_on
+TacticDoc trivial
 "
-## Summary
+`trivial` versucht durch Kombination von wenigen simplen Taktiken das Goal zu schliessen.
 
-If `n : ℕ` is in our objects list, then `induction_on n`
-attempts to prove the current goal by induction on `n`, with the inductive
-assumption in the `succ` case being `ind_hyp`.
+## Details
+Die Taktiken, die verwendet werden sind:
 
-### Example:
-If your current goal is:
-```
-Objects
-  n : ℕ
-Prove:
-  2 * n = n + n
-```
+* `assumption`
+* `rfl`
+* `contradiction`
+* und noch 3 andere, die hier nicht behandelt werden
+  (`decide`, `apply True.intro`, `apply And.intro`).
+"
 
-then
+TacticDoc unfold
+"
+`unfold myDef` öffnet eine Definition im Goal.
 
-`induction_on n`
+## Details
+Bis auf DefEq (definitinal equality) ändert `unfold` nichts, manche Taktiken
+(z.B. `push_neg`, `rw`) brauchen aber manchmal die Hilfe.
 
-will give us two goals:
+`unfold myDef at h` kann auch Definitionen in Annahmen öffnen
 
-```
-Prove:
-  2 * 0 = 0 + 0
-```
+## Hilfreiche Resultate
 
-and
-```
-Objects
-  n : ℕ,
-Assumptions
-  ind_hyp : 2 * n = n + n
-Prove:
-  2 * succ n = succ n + succ n
-```
+* `change P` ist eine andere Taktik, die das aktuelle Goal in einen DefEq-Ausdruck umschreibt.
+  Diese Taktik braucht man auch manchmal um zu hacken, wenn Lean Mühe hat etwas zu verstehen.
 "
 
-TacticDoc intro
-"Useful to introduce stuff"
+TacticDoc use
+"
+Wenn das Goal von der Form `∃x, P x` ist, kann man mit `use n` ein konkretes Element angeben
+mit dem man das Goal beweisen möchte.
+"