diff --git a/server/testgame/TestGame/Levels/LinearAlgebra.lean b/server/testgame/TestGame/Levels/LinearAlgebra.lean
index 816817f..676e2db 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra.lean
@@ -10,7 +10,6 @@ import TestGame.Levels.LinearAlgebra.L08_GeneratingSet
 import TestGame.Levels.LinearAlgebra.M01_LinearMap
 import TestGame.Levels.LinearAlgebra.M02_LinearIndep
 import TestGame.Levels.LinearAlgebra.M04_Basis
-import TestGame.Levels.LinearAlgebra.M05_Basis
 
 import TestGame.Levels.LinearAlgebra.N01_Span
 import TestGame.Levels.LinearAlgebra.N02_Span
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/M02_LinearIndep.lean b/server/testgame/TestGame/Levels/LinearAlgebra/M02_LinearIndep.lean
index 0114b45..a6d0d4e 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/M02_LinearIndep.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/M02_LinearIndep.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Fin.VecNotation
 -- import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.Algebra.BigOperators.Basic -- default
 -- import Mathlib.LinearAlgebra.LinearIndependent
+import Mathlib
 
 Game "TestGame"
 World "Basis"
@@ -15,7 +16,9 @@ Level 2
 
 Title "Lineare Unabhängigkeit"
 
---notation "ℝ²" => Fin 2 → ℝ
+namespace Ex_LinIndep
+
+scoped notation "ℝ²" => Fin 2 → ℝ
 
 Introduction
 "
@@ -23,18 +26,24 @@ Introduction
 
 Statement
 "Zeige, dass `![1, 0], ![1, 1]` linear unabhängig über `ℝ` sind."
-    : True := by -- linearIndependent ℝ ![(![1, 0] : ℝ²), ![1, 1]] := by
-  trivial
-
--- begin
---   rw fintype.linear_independent_iff,
---   intros c h,
---   simp at h,
---   intros i,
---   fin_cases i,
---   swap,
---   { exact h.2 },
---   { have h' := h.1,
---     rw [h.2, add_zero] at h',
---     exact h'}
--- end
+    : LinearIndependent ℝ ![(![1, 0] : ℝ²), ![1, 1]] := by
+  Hint "`rw [Fintype.linearIndependent_iff]`"
+  rw [Fintype.linearIndependent_iff]
+  Hint "`intros c h`"
+  intros c h
+  Hint "BUG: `simp at h` does not work :("
+  simp at h -- doesn't work
+  sorry
+
+  -- rw [Fintype.linearIndependent_iff]
+  -- intros c h
+  -- simp at h
+  -- intros i
+  -- fin_cases i
+  -- swap
+  -- { exact h.2 }
+  -- { have h' := h.1
+  --   rw [h.2, add_zero] at h'
+  --   exact h'}
+
+end Ex_LinIndep
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/M04_Basis.lean b/server/testgame/TestGame/Levels/LinearAlgebra/M04_Basis.lean
index 66c3304..25b5553 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/M04_Basis.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/M04_Basis.lean
@@ -1,6 +1,7 @@
 import TestGame.Metadata
 
 import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib
 
 Game "TestGame"
 World "Basis"
@@ -8,12 +9,24 @@ Level 4
 
 Title "Basis"
 
+namespace Ex_Basis
+
+scoped notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule
+
 Introduction
 "
 
 "
 
-Statement
-""
-    : True := by -- Basis (Fin 2) ℝ ℝ² := by
-  trivial
+lemma exercise1 : LinearIndependent ℝ ![(![1, 0] : ℝ²), ![1, 1]] := sorry
+
+lemma exercise2 :  ⊤ ≤ span ℝ (Set.range ![(![1, 0] : Fin 2 → ℝ), ![1, 1]]) := sorry
+
+Statement : Basis (Fin 2) ℝ ℝ² := by
+  apply Basis.mk
+  apply exercise1
+  apply exercise2
+
+end Ex_Basis
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/M05_Basis.lean b/server/testgame/TestGame/Levels/LinearAlgebra/M05_Basis.lean
deleted file mode 100644
index ed5be65..0000000
--- a/server/testgame/TestGame/Levels/LinearAlgebra/M05_Basis.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib.Algebra.Module.Submodule.Lattice
-
-Game "TestGame"
-World "Basis"
-Level 5
-
-Title "Lineare Abbildung"
-
-Introduction
-"
-
-"
-
-Statement
-""
-    : True := by
-  trivial
diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
index 04a74bf..431dc1c 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
@@ -62,6 +62,6 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
 
 NewTactic constructor intro rw assumption rcases simp tauto trivial
 
-NewLemma Subset.antisymm empty_subset
+NewLemma Subset.antisymm Subset.antisymm_iff empty_subset
 
 end MySet