diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index f346c35..d3d8d7c 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -3,209 +3,451 @@ import GameServer.Commands
 -- Wird im Level "Implication 11" ohne Beweis angenommen.
 LemmaDoc not_not as "not_not" in "Logic"
 "
-### Aussage
+`not_not {A : Prop} : ¬¬A ↔ A`
 
-`¬¬A ↔ A`
-
-### Annahmen
-
-`(A : Prop)`
+* `simp`-Lemma: Ja
+* Namespace: `Classical`
+* Minimal Import: `Std.Logic`
+* Mathlib Doc: [#not_not](https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#Classical.not_not)
 "
 
 -- Wird im Level "Implication 10" ohne Beweis angenommen.
 LemmaDoc not_or_of_imp as "not_or_of_imp" in "Logic"
 "
-### Aussage
-
-`¬A ∨ B`
-
-### Annahmen
+`not_or_of_imp {A B : Prop} : (A → B) → ¬A ∨ B`
 
-`(A B : Prop)`\\
-`(h : A → B)`
+* `simp`-Lemma: Nein
+* Namespace: `-`
+* Minimal Import: `Mathlib.Logic.Basic`
+* Mathlib Doc: [#not_or_of_imp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#not_or_of_imp)
 "
 
 -- Wird im Level "Implication 12" bewiesen.
 LemmaDoc imp_iff_not_or as "imp_iff_not_or" in "Logic"
 "
-### Aussage
+`imp_iff_not_or {A B : Prop} : (A → B) ↔ (¬A ∨ B)`
 
-`(A → B) ↔ ¬A ∨ B`
-
-### Annahmen
-
-`(A B : Prop)`
+* `simp`-Lemma: Nein
+* Namespace: `-`
+* Minimal Import: `Mathlib.Logic.Basic`
+* Mathlib Doc: [#imp_iff_not_or](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#imp_iff_not_or)
 "
 
-
-LemmaDoc Nat.succ_pos as "Nat.succ_pos" in "Nat"
+LemmaDoc Nat.succ_pos as "succ_pos" in "Nat"
 "
-"
-
-LemmaDoc Nat.pos_iff_ne_zero as "Nat.pos_iff_ne_zero" in "Nat"
-"
-"
-
-LemmaDoc zero_add as "zero_add" in "Addition"
-"This lemma says `∀ a : ℕ, 0 + a = a`."
+`Nat.succ_pos (n : ℕ) : 0 < n.succ`
 
-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)`."
+$n + 1$ ist strikt grösser als Null.
 
-LemmaDoc not_forall as "not_forall" in "Logic"
-"`∀ (A : Prop), ¬(∀ x, A) ↔ ∃x, (¬A)`."
+## Eigenschaften
 
-LemmaDoc not_exists as "not_exists" in "Logic"
-"`∀ (A : Prop), ¬(∃ x, A) ↔ ∀x, (¬A)`."
-
-DefinitionDoc Even as "Even"
-"
-`even n` ist definiert als `∃ r, a = 2 * r`.
-Die Definition kann man mit `unfold even at *` einsetzen.
+* `simp` Lemma: Nein
+* Namespace: `Nat`
+* Minimal Import: `Mathlib.Init.Prelude`
+* Mathlib Doc: [#Nat.succ_pos](https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat.succ_pos)
 "
 
-DefinitionDoc Odd as "Odd"
-"
-`odd n` ist definiert als `∃ r, a = 2 * r + 1`.
-Die Definition kann man mit `unfold odd at *` einsetzen.
+LemmaDoc Nat.pos_iff_ne_zero as "pos_iff_ne_zero" in "Nat"
 "
+`Nat.pos_iff_ne_zero {n : ℕ} : 0 < n ↔ n ≠ 0`
 
-DefinitionDoc Injective as "Injective"
+* `simp`-Lemma: Nein
+* Namespace: `Nat`
+* Minimal Import: `Std.Data.Nat.Lemmas`
+* Mathlib Doc: [#Nat.pos_iff_ne_zero](https://leanprover-community.github.io/mathlib4_docs/Std/Data/Nat/Lemmas.html#Nat.pos_iff_ne_zero)
 "
-`Injective f` ist definiert als
 
-```
-∀ a b, f a = f b → a = b
-```
-definiert.
-"
+-- TODO: Not minimal description
+LemmaDoc zero_add as "zero_add" in "Addition"
+"zero_add (a : ℕ) : 0 + a = a`.
 
-DefinitionDoc Surjective as "Surjective"
-"
-`Surjective f` ist definiert als
 
-```
-∀ a, (∃ b, f a = b)
-```
+* `simp`-Lemma: Ja
+* Namespace: `-`
+* Import: `Mathlib.Nat.Basic`
+* Mathlib Doc: [#zero_add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#zero_add)
 "
 
-DefinitionDoc Bijective as "Bijective"
-"
-"
+LemmaDoc add_zero as "add_zero" in "Addition"
+"This lemma says `∀ a : ℕ, a + 0 = a`.
 
-DefinitionDoc LeftInverse as "LeftInverse"
-"
-"
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc"
 
-DefinitionDoc RightInverse as "RightInverse"
-"
+LemmaDoc add_succ as "add_succ" in "Addition"
+"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`.
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()"
+
+LemmaDoc not_forall as "not_forall" in "Logic"
 "
+`not_forall {α : Sort _} {P : α → Prop} : ¬(∀ x, → P x) ↔ ∃ x, ¬P x`
 
-DefinitionDoc StrictMono as "StrictMono"
+* `simp`-Lemma: Ja
+* Namespace: `-`
+* Minimal Import: `Mathlib.Logic.Basic`
+* Mathlib Doc: [#not_forall](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#not_forall)
 "
-`StrictMono f` ist definiert als
 
-```
-∀ a b, a < b → f a < f b
-```
+LemmaDoc not_exists as "not_exists" in "Logic"
+"`∀ (A : Prop), ¬(∃ x, A) ↔ ∀x, (¬A)`.
 
-"
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()"
 
 LemmaDoc even_iff_not_odd as "even_iff_not_odd" in "Nat"
-"`Even n ↔ ¬ (Odd n)`"
+"`Even n ↔ ¬ (Odd n)`
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()"
 
 LemmaDoc odd_iff_not_even as "odd_iff_not_even" in "Nat"
-"`Odd n ↔ ¬ (Even n)`"
+"`Odd n ↔ ¬ (Even n)`
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()"
 
 LemmaDoc even_square as "even_square" in "Nat"
-"`∀ (n : ℕ), Even n → Even (n ^ 2)`"
+"`∀ (n : ℕ), Even n → Even (n ^ 2)`
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 
 
 
 LemmaDoc mem_univ as "mem_univ" in "Set"
-"x ∈ @univ α"
+"x ∈ @univ α
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc not_mem_empty as "not_mem_empty" in "Set"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc empty_subset as "empty_subset" in "Set"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Subset.antisymm_iff as "Subset.antisymm_iff" in "Set"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 
 
 LemmaDoc Nat.prime_def_lt'' as "Nat.prime_def_lt''" in "Nat"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 
 LemmaDoc Finset.sum_add_distrib as "Finset.sum_add_distrib" in "Sum"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Fin.sum_univ_castSucc as "Fin.sum_univ_castSucc" in "Sum"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Nat.succ_eq_add_one as "Nat.succ_eq_add_one" in "Sum"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Nat.zero_eq as "Nat.succ_eq_add_one" in "Sum"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc add_comm as "add_comm" in "Nat"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc mul_add as "mul_add" in "Nat"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc add_mul as "add_mul" in "Nat"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc arithmetic_sum as "arithmetic_sum" in "Sum"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc add_pow_two as "add_pow_two" in "Nat"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Function.comp_apply as "Function.comp_apply" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc not_le as "not_le" in "Logic"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc if_pos as "if_pos" in "Logic"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc if_neg as "if_neg" in "Logic"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc StrictMono.injective as "StrictMono.injective" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc StrictMono.add as "StrictMono.add" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Odd.strictMono_pow as "Odd.strictMono_pow" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Exists.choose as "Exists.choose" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Exists.choose_spec as "Exists.choose_spec" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 LemmaDoc congrArg as "congrArg" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 LemmaDoc congrFun as "congrFun" in "Function"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
 
 LemmaDoc Iff.symm as "Iff.symm" in "Logic"
-""
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
+
+
+
+/-! ## Definitions -/
+
+DefinitionDoc Even as "Even"
+"
+`even n` ist definiert als `∃ r, a = 2 * r`.
+Die Definition kann man mit `unfold even at *` einsetzen.
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()"
+
+DefinitionDoc Odd as "Odd"
+"
+`odd n` ist definiert als `∃ r, a = 2 * r + 1`.
+Die Definition kann man mit `unfold odd at *` einsetzen.
+"
+
+DefinitionDoc Injective as "Injective"
+"
+`Injective f` ist definiert als
+
+```
+∀ a b, f a = f b → a = b
+```
+definiert.
+"
+
+DefinitionDoc Surjective as "Surjective"
+"
+`Surjective f` ist definiert als
+
+```
+∀ a, (∃ b, f a = b)
+```
+"
+
+DefinitionDoc Bijective as "Bijective"
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
+
+DefinitionDoc LeftInverse as "LeftInverse"
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
+
+DefinitionDoc RightInverse as "RightInverse"
+"
+
+* `simp`-Lemma:
+* Namespace: `-`
+* Minimal Import: `Mathlib.`
+* Mathlib Doc: [#]()
+"
+
+DefinitionDoc StrictMono as "StrictMono"
+"
+`StrictMono f` ist definiert als
+
+```
+∀ a b, a < b → f a < f b
+```
+
+"
+
 
 DefinitionDoc Symbol.Subset as "⊆" "Test"
diff --git a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
index f515bb1..b378431 100644
--- a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
+++ b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
@@ -83,7 +83,7 @@ Statement arithmetic_sum
   ring
 
 NewTactic induction
-NewLemma Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul
+NewLemma Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul Nat.zero_eq
 
 Conclusion "Du schaust dich um und bewunderst das Tal in dem hunderte, wenn nicht tausende,
 Steintürme in allen Formen und Höhen stehen."
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index dd5d26b..63501b5 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -521,4 +521,9 @@ 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.
+
+## Details
+
+`use n` versucht zudem anschliessend `rfl` aufzurufen, und kann das Goal damit manchmal direkt
+schließen.
 "