diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index d3d8d7c..52e7a61 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -5,6 +5,8 @@ LemmaDoc not_not as "not_not" in "Logic"
 "
 `not_not {A : Prop} : ¬¬A ↔ A`
 
+## Eigenschaften
+
 * `simp`-Lemma: Ja
 * Namespace: `Classical`
 * Minimal Import: `Std.Logic`
@@ -16,6 +18,8 @@ LemmaDoc not_or_of_imp as "not_or_of_imp" in "Logic"
 "
 `not_or_of_imp {A B : Prop} : (A → B) → ¬A ∨ B`
 
+## Eigenschaften
+
 * `simp`-Lemma: Nein
 * Namespace: `-`
 * Minimal Import: `Mathlib.Logic.Basic`
@@ -27,6 +31,8 @@ LemmaDoc imp_iff_not_or as "imp_iff_not_or" in "Logic"
 "
 `imp_iff_not_or {A B : Prop} : (A → B) ↔ (¬A ∨ B)`
 
+## Eigenschaften
+
 * `simp`-Lemma: Nein
 * Namespace: `-`
 * Minimal Import: `Mathlib.Logic.Basic`
@@ -51,6 +57,8 @@ LemmaDoc Nat.pos_iff_ne_zero as "pos_iff_ne_zero" in "Nat"
 "
 `Nat.pos_iff_ne_zero {n : ℕ} : 0 < n ↔ n ≠ 0`
 
+## Eigenschaften
+
 * `simp`-Lemma: Nein
 * Namespace: `Nat`
 * Minimal Import: `Std.Data.Nat.Lemmas`
@@ -59,8 +67,10 @@ LemmaDoc Nat.pos_iff_ne_zero as "pos_iff_ne_zero" in "Nat"
 
 -- TODO: Not minimal description
 LemmaDoc zero_add as "zero_add" in "Addition"
-"zero_add (a : ℕ) : 0 + a = a`.
+"
+`zero_add (a : ℕ) : 0 + a = a`
 
+## Eigenschaften
 
 * `simp`-Lemma: Ja
 * Namespace: `-`
@@ -69,7 +79,10 @@ LemmaDoc zero_add as "zero_add" in "Addition"
 "
 
 LemmaDoc add_zero as "add_zero" in "Addition"
-"This lemma says `∀ a : ℕ, a + 0 = a`.
+"
+This lemma says `∀ a : ℕ, a + 0 = a`.
+
+## Eigenschaften
 
 * `simp`-Lemma:
 * Namespace: `-`
@@ -79,6 +92,8 @@ LemmaDoc add_zero as "add_zero" in "Addition"
 LemmaDoc add_succ as "add_succ" in "Addition"
 "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`.
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -88,6 +103,8 @@ LemmaDoc not_forall as "not_forall" in "Logic"
 "
 `not_forall {α : Sort _} {P : α → Prop} : ¬(∀ x, → P x) ↔ ∃ x, ¬P x`
 
+## Eigenschaften
+
 * `simp`-Lemma: Ja
 * Namespace: `-`
 * Minimal Import: `Mathlib.Logic.Basic`
@@ -95,82 +112,139 @@ LemmaDoc not_forall as "not_forall" in "Logic"
 "
 
 LemmaDoc not_exists as "not_exists" in "Logic"
-"`∀ (A : Prop), ¬(∃ x, A) ↔ ∀x, (¬A)`.
+"
+`not_exists {α : Sort _} {P : α → Prop} : (¬∃ x, P x) ↔ ∀ (x : α), ¬P x.
 
-* `simp`-Lemma:
+## Eigenschaften
+
+* `simp`-Lemma: Ja
 * Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()"
+* Minimal Import: `Std.Logic`
+* Mathlib Doc: [#not_exists](https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#not_exists)"
 
-LemmaDoc even_iff_not_odd as "even_iff_not_odd" in "Nat"
-"`Even n ↔ ¬ (Odd n)`
+LemmaDoc Nat.even_iff_not_odd as "even_iff_not_odd" in "Nat"
+"
+`even_iff_not_odd  {n : ℕ} : Even n ↔ ¬Odd n`
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()"
+## Eigenschaften
 
-LemmaDoc odd_iff_not_even as "odd_iff_not_even" in "Nat"
-"`Odd n ↔ ¬ (Even n)`
+* `simp`-Lemma: Nein
+* Namespace: `Nat`
+* Minimal Import: `Mathlib.Data.Nat.Parity`
+* Mathlib Doc: [#Nat.even_iff_not_odd](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Parity.html#Nat.even_iff_not_odd)"
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()"
+LemmaDoc Nat.odd_iff_not_even as "odd_iff_not_even" in "Nat"
+"
+`Nat.odd_iff_not_even {n : ℕ} : Odd n ↔ ¬Even n`
+
+## Eigenschaften
+
+* `simp`-Lemma: Ja
+* Namespace: `Nat`
+* Minimal Import: `Mathlib.Data.Nat.Parity`
+* Mathlib Doc: [#Nat.odd_iff_not_even](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Parity.html#Nat.odd_iff_not_even)"
 
 LemmaDoc even_square as "even_square" in "Nat"
-"`∀ (n : ℕ), Even n → Even (n ^ 2)`
+"
+`even_square : (n : ℕ), Even n → Even (n ^ 2)`
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+## Eigenschaften
+
+* `simp`-Lemma: Nein
+* *Nicht in Mathlib*
 "
 
 
 
 
-LemmaDoc mem_univ as "mem_univ" in "Set"
-"x ∈ @univ α
+LemmaDoc Set.mem_univ as "mem_univ" in "Set"
+"
+`Set.mem_univ {α : Type _} (x : α) : x ∈ @univ α`
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+Jedes Element ist in `univ`, der Menge aller Elemente eines Typs `α`.
+
+## Eigenschaften
+
+* `simp`-Lemma: Ja
+* Namespace: `Set`
+* Minimal Import: `Mathlib.Data.Set.Basic`
+* Mathlib Doc: [#mem_univ](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.mem_univ)
 "
 
 LemmaDoc not_mem_empty as "not_mem_empty" in "Set"
 "
+`Set.not_mem_empty {α : Type _} (x : α) : x ∉ ∅`
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+Kein Element ist in der leeren Menge.
+
+## Eigenschaften
+
+* `simp`-Lemma: Nein
+* Namespace: `Set`
+* Minimal Import: `Mathlib.Data.Set.Basic`
+* Mathlib Doc: [#not_mem_empty](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.not_mem_empty)
 "
 
 LemmaDoc empty_subset as "empty_subset" in "Set"
 "
+`Set.empty_subset {α : Type u} (s : Set α) : ∅ ⊆ s`
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+## Eigenschaften
+
+* `simp`-Lemma: Ja
+* Namespace: `Set`
+* Minimal Import: `Mathlib.Data.Set.Basic`
+* Mathlib Doc: [#empty_subset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.empty_subset)
 "
 
-LemmaDoc Subset.antisymm_iff as "Subset.antisymm_iff" in "Set"
+LemmaDoc Subset.antisymm as "Subset.antisymm" in "Set"
 "
+`Set.Subset.antisymm {α : Type u} {a : Set α} {b : Set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b`
 
-* `simp`-Lemma:
-* Namespace: `-`
-* Minimal Import: `Mathlib.`
-* Mathlib Doc: [#]()
+Zwei Mengen sind identisch, wenn sowohl $A \\subseteq B$ wie auch $B \\subseteq A$.
+## Details
+
+`apply Subset.antisymm` ist eine Möglichkeit Gleichungen von Mengen zu zeigen.
+eine andere ist `ext i`, welches Elementweise funktiniert.
+Siehe auch
+[`#Subset.antisymm_iff`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm_iff)
+für die Iff-Version.
+
+## Eigenschaften
+
+* `simp`-Lemma: Nein
+* Namespace: `Set.Subset`
+* Minimal Import: `Mathlib.Data.Set.Basic`
+* Mathlib Doc: [#Subset.antisymm](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm)
 "
 
+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.
+eine andere ist `ext i`, welches Elementweise funktiniert.
+Siehe auch
+[`#Subset.antisymm`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm)
+für eine verwandte Version.
+
+## Eigenschaften
+
+* `simp`-Lemma: Nein
+* Namespace: `Set.Subset`
+* Minimal Import: `Mathlib.Data.Set.Basic`
+* Mathlib Doc: [#Subset.antisymm_iff](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm_iff)
+"
 
 
 LemmaDoc Nat.prime_def_lt'' as "Nat.prime_def_lt''" in "Nat"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -181,6 +255,8 @@ LemmaDoc Nat.prime_def_lt'' as "Nat.prime_def_lt''" in "Nat"
 LemmaDoc Finset.sum_add_distrib as "Finset.sum_add_distrib" in "Sum"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -190,6 +266,8 @@ LemmaDoc Finset.sum_add_distrib as "Finset.sum_add_distrib" in "Sum"
 LemmaDoc Fin.sum_univ_castSucc as "Fin.sum_univ_castSucc" in "Sum"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -199,6 +277,8 @@ LemmaDoc Fin.sum_univ_castSucc as "Fin.sum_univ_castSucc" in "Sum"
 LemmaDoc Nat.succ_eq_add_one as "Nat.succ_eq_add_one" in "Sum"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -208,6 +288,8 @@ LemmaDoc Nat.succ_eq_add_one as "Nat.succ_eq_add_one" in "Sum"
 LemmaDoc Nat.zero_eq as "Nat.succ_eq_add_one" in "Sum"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -217,6 +299,8 @@ LemmaDoc Nat.zero_eq as "Nat.succ_eq_add_one" in "Sum"
 LemmaDoc add_comm as "add_comm" in "Nat"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -226,6 +310,8 @@ LemmaDoc add_comm as "add_comm" in "Nat"
 LemmaDoc mul_add as "mul_add" in "Nat"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -235,6 +321,8 @@ LemmaDoc mul_add as "mul_add" in "Nat"
 LemmaDoc add_mul as "add_mul" in "Nat"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -244,6 +332,8 @@ LemmaDoc add_mul as "add_mul" in "Nat"
 LemmaDoc arithmetic_sum as "arithmetic_sum" in "Sum"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -253,6 +343,8 @@ LemmaDoc arithmetic_sum as "arithmetic_sum" in "Sum"
 LemmaDoc add_pow_two as "add_pow_two" in "Nat"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -262,6 +354,8 @@ LemmaDoc add_pow_two as "add_pow_two" in "Nat"
 LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -271,6 +365,8 @@ LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum"
 LemmaDoc Function.comp_apply as "Function.comp_apply" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -280,6 +376,8 @@ LemmaDoc Function.comp_apply as "Function.comp_apply" in "Function"
 LemmaDoc not_le as "not_le" in "Logic"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -289,6 +387,8 @@ LemmaDoc not_le as "not_le" in "Logic"
 LemmaDoc if_pos as "if_pos" in "Logic"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -298,6 +398,8 @@ LemmaDoc if_pos as "if_pos" in "Logic"
 LemmaDoc if_neg as "if_neg" in "Logic"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -307,6 +409,8 @@ LemmaDoc if_neg as "if_neg" in "Logic"
 LemmaDoc StrictMono.injective as "StrictMono.injective" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -316,6 +420,8 @@ LemmaDoc StrictMono.injective as "StrictMono.injective" in "Function"
 LemmaDoc StrictMono.add as "StrictMono.add" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -325,6 +431,8 @@ LemmaDoc StrictMono.add as "StrictMono.add" in "Function"
 LemmaDoc Odd.strictMono_pow as "Odd.strictMono_pow" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -334,6 +442,8 @@ LemmaDoc Odd.strictMono_pow as "Odd.strictMono_pow" in "Function"
 LemmaDoc Exists.choose as "Exists.choose" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -343,6 +453,8 @@ LemmaDoc Exists.choose as "Exists.choose" in "Function"
 LemmaDoc Exists.choose_spec as "Exists.choose_spec" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -351,6 +463,8 @@ LemmaDoc Exists.choose_spec as "Exists.choose_spec" in "Function"
 LemmaDoc congrArg as "congrArg" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -359,6 +473,8 @@ LemmaDoc congrArg as "congrArg" in "Function"
 LemmaDoc congrFun as "congrFun" in "Function"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -368,6 +484,8 @@ LemmaDoc congrFun as "congrFun" in "Function"
 LemmaDoc Iff.symm as "Iff.symm" in "Logic"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -382,6 +500,8 @@ DefinitionDoc Even as "Even"
 "
 `even n` ist definiert als `∃ r, a = 2 * r`.
 Die Definition kann man mit `unfold even at *` einsetzen.
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -415,6 +535,8 @@ DefinitionDoc Surjective as "Surjective"
 DefinitionDoc Bijective as "Bijective"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -424,6 +546,8 @@ DefinitionDoc Bijective as "Bijective"
 DefinitionDoc LeftInverse as "LeftInverse"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
@@ -433,6 +557,8 @@ DefinitionDoc LeftInverse as "LeftInverse"
 DefinitionDoc RightInverse as "RightInverse"
 "
 
+## Eigenschaften
+
 * `simp`-Lemma:
 * Namespace: `-`
 * Minimal Import: `Mathlib.`
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
index 9eeab66..7d5bf80 100644
--- a/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
@@ -106,4 +106,4 @@ ist deine!
 "
 
 NewTactic push_neg
-NewLemma even_iff_not_odd odd_iff_not_even not_exists not_forall
+NewLemma Nat.even_iff_not_odd Nat.odd_iff_not_even not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
index a990e16..57681d9 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
@@ -26,7 +26,7 @@ Statement not_mem_empty "" {A : Type} (x : A) :
   **Robo**: Dann behaupte das doch."
   tauto
 
-NewLemma mem_univ
+NewLemma Set.mem_univ
 
 Conclusion "Der Junge rennt weiter.
 
diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
index 63d3f3b..04a74bf 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
@@ -52,8 +52,7 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
 
   constructor
   intro h
-  rw [Subset.antisymm_iff]
-  constructor
+  apply Subset.antisymm
   assumption
   simp only [empty_subset]
   intro a
@@ -63,6 +62,6 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
 
-NewLemma Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm empty_subset
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
index 15f6394..fc4e714 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
@@ -47,6 +47,4 @@ Statement eq_empty_iff_forall_not_mem
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
 
-NewLemma Subset.antisymm_iff empty_subset
-
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
index bc69079..b3adf6e 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
@@ -31,5 +31,3 @@ Statement nonempty_iff_ne_empty
   rfl
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
index 098ca27..cbb767b 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
@@ -27,5 +27,3 @@ Statement
   simp
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
index 906bac4..8da2a5a 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
@@ -31,5 +31,3 @@ Statement
   rw [univ_union]
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
index f454337..f9481bf 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
@@ -31,5 +31,3 @@ Statement
   exact h4
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
index 6dd11f4..fbcf31c 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
@@ -34,5 +34,3 @@ Statement
   exact hx
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
index 40c786d..23f484f 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
@@ -33,5 +33,3 @@ Statement
   rfl
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
index 50a1e18..f87e21b 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
@@ -33,5 +33,3 @@ Statement
   ring
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
index 7162728..c2fbe30 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
@@ -38,5 +38,3 @@ Statement
 
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
index df5d23e..606947f 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
@@ -37,5 +37,3 @@ Statement
 
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
index 94d3ae8..975846f 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
@@ -35,5 +35,3 @@ Statement
 
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
index 5d81257..d138956 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
@@ -29,5 +29,3 @@ Statement
   library_search
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
index 93569fb..61abddd 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
@@ -24,5 +24,3 @@ Statement
   ring
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
index 7a9d10e..c61c6ab 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
@@ -23,5 +23,3 @@ Statement
 "" : True := sorry
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
index 52d376c..1e45403 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
@@ -24,5 +24,3 @@ Statement
   ring
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
-
-NewLemma Subset.antisymm_iff empty_subset