From 27532a7688396b2bbee106dd2ab34553bb43e788 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 10 Mar 2023 10:14:51 +0100
Subject: [PATCH] fix errors during merge

---
 server/testgame/TestGame/Levels/Function.lean    | 13 +++++++------
 server/testgame/TestGame/Levels/Sum/L02_Sum.lean |  2 +-
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/server/testgame/TestGame/Levels/Function.lean b/server/testgame/TestGame/Levels/Function.lean
index d502584..0d2770d 100644
--- a/server/testgame/TestGame/Levels/Function.lean
+++ b/server/testgame/TestGame/Levels/Function.lean
@@ -1,11 +1,12 @@
 import TestGame.Levels.Function.L01_Function
 import TestGame.Levels.Function.L02_Let
-import TestGame.Levels.Function.L03_Composition
-import TestGame.Levels.Function.L06_Piecewise
-import TestGame.Levels.Function.L07_Injective
-import TestGame.Levels.Function.L08_Injective
-import TestGame.Levels.Function.L09_Surjective
-import TestGame.Levels.Function.L10_Bijective
+import TestGame.Levels.Function.L03_Piecewise
+import TestGame.Levels.Function.L04_Injective
+import TestGame.Levels.Function.L05_Injective
+import TestGame.Levels.Function.L06_Injective
+import TestGame.Levels.Function.L07_Surjective
+import TestGame.Levels.Function.L08_Bijective
+import TestGame.Levels.Function.L09_Inverse
 import TestGame.Levels.Function.L11_Inverse
 
 Game "TestGame"
diff --git a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
index c7b722f..218187a 100644
--- a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
+++ b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
@@ -38,4 +38,4 @@ Statement
     Alternativ kann man auch mit `rw [add_comm]` dies explizit umordnen."
   ring
 
-NewLemmas Finset.sum_add_distrib add_comm
+NewLemma Finset.sum_add_distrib add_comm