diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
index 4a04171..17f9af6 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
@@ -2,7 +2,6 @@ import TestGame.Metadata
 
 import Mathlib.Init.Set
 import Mathlib.Tactic.Tauto
-import Mathlib
 
 set_option tactic.hygienic false
 
diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
index 431dc1c..4ef1bd8 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
@@ -3,6 +3,7 @@ import TestGame.Levels.SetTheory.L03_Subset
 
 import Mathlib.Init.Set
 import Mathlib.Tactic.Tauto
+import Mathlib
 
 set_option tactic.hygienic false
 
@@ -48,10 +49,11 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
   Hint "**Du**: Ja, die einzige Teilmenge der leeren Menge ist die leere Menge.
   Das ist doch eine Tautologie?
 
-  **Robo**: Naja nicht ganz, "
-
+  **Robo**: Ja schon, aber zuerst einmal explizit."
+  Hint (hidden := true) "**Robo**: Fang doch einmal mit `constructor` an."
   constructor
   intro h
+  Hint "**Robo**: "
   apply Subset.antisymm
   assumption
   simp only [empty_subset]
@@ -60,8 +62,7 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
   rcases a with ⟨h₁, h₂⟩
   assumption
 
-NewTactic constructor intro rw assumption rcases simp tauto trivial
-
+DisabledTactic tauto
 NewLemma Subset.antisymm Subset.antisymm_iff empty_subset
 
 end MySet
diff --git a/server/testgame/TestGame/MyNat.lean b/server/testgame/TestGame/MyNat.lean
deleted file mode 100644
index 3cecede..0000000
--- a/server/testgame/TestGame/MyNat.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-axiom MyNat : Type
-
---notation "ℕ" => MyNat
-
---axiom zero : ℕ
-
-axiom succ : ℕ → ℕ
-
-@[instance] axiom MyOfNat (n : Nat) : OfNat ℕ n
-
-@[instance] axiom myAddition : HAdd ℕ ℕ ℕ
-
-@[instance] axiom myMultiplication : HMul ℕ ℕ ℕ
-
-axiom add_zero : ∀ a : ℕ, a + 0 = a
-
-axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)
-
-@[elab_as_elim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n