From f2a8ca3785912cf26a1b3df34852aca995bc37fc Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 5 Sep 2024 10:37:43 +0200
Subject: [PATCH] add Image/Preimage planet

---
 .i18n/de/Game.pot                             | 160 ++++++++++--------
 Game.lean                                     |   1 +
 Game/Levels/FunctionBij.lean                  |   1 -
 Game/Levels/FunctionImage.lean                |   9 +
 .../FunctionImage/L01_ImagePreimage.lean      |  34 ++++
 .../FunctionImage/L02_ImagePreimage.lean      |  22 +++
 .../L03_InjectiveRange.lean                   |   5 +-
 .../L04_LeftInvPreimage.lean}                 |   4 +-
 .../L05_Preimage_Injective.lean}              |   4 +-
 .../L06_SurjectiveRange.lean}                 |   4 +-
 Game/Levels/FunctionImage/LXX_Set6.lean       |  15 ++
 Game/Levels/FunctionInj.lean                  |   2 -
 Game/Levels/FunctionInj/L04_Injective.lean    |   2 +-
 Game/Levels/FunctionInj/L05_Injective.lean    |   2 +-
 .../FunctionInj/L06_SuccHasLeftInv.lean       |   2 +-
 Game/Levels/FunctionInj/L07_Extend.lean       |   2 +-
 .../FunctionInj/L09_InjOfHasLeftInv.lean      |   2 +-
 .../FunctionInj/L10_RightInvOfLeftInv.lean    |   2 +-
 .../Levels/FunctionInj/L11_InjHasLeftInv.lean |  11 +-
 Game/Levels/FunctionSurj.lean                 |   1 -
 Game/Levels/FunctionSurj/L14_choose.lean      |   2 +-
 .../FunctionSurj/L15_SurjectiveTFAE.lean      |   2 +-
 22 files changed, 195 insertions(+), 94 deletions(-)
 create mode 100644 Game/Levels/FunctionImage.lean
 create mode 100644 Game/Levels/FunctionImage/L01_ImagePreimage.lean
 create mode 100644 Game/Levels/FunctionImage/L02_ImagePreimage.lean
 rename Game/Levels/{FunctionInj => FunctionImage}/L03_InjectiveRange.lean (92%)
 rename Game/Levels/{FunctionInj/L08_LeftInvPreimage.lean => FunctionImage/L04_LeftInvPreimage.lean} (97%)
 rename Game/Levels/{FunctionBij/L09_Preimage_Injective.lean => FunctionImage/L05_Preimage_Injective.lean} (97%)
 rename Game/Levels/{FunctionSurj/L13_SurjectiveRange.lean => FunctionImage/L06_SurjectiveRange.lean} (97%)
 create mode 100644 Game/Levels/FunctionImage/LXX_Set6.lean

diff --git a/.i18n/de/Game.pot b/.i18n/de/Game.pot
index 445cc78..c4f8099 100644
--- a/.i18n/de/Game.pot
+++ b/.i18n/de/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Tue Sep  3 15:32:52 2024\n"
+"POT-Creation-Date: Thu Sep  5 10:36:56 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: de\n"
@@ -5017,31 +5017,6 @@ msgid "**Robo**: Siehst du die Annahme `«{hs}» : f ∘ g = succ ∘ f`?\n"
 "`f₁ = f₂` in `∀ x, f₁ x = f₂ x` um."
 msgstr ""
 
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "Range of Surjection"
-msgstr ""
-
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "The range of a function is the set of all outputs.\n"
-"\n"
-"In this level you show that a function is surjective if and only if the range of\n"
-"the function is equal to the universal subset of the codomain. For `f : A → B`,\n"
-"the range of `f` is defined as\n"
-"\n"
-"```\n"
-"range f : Set B := {b | ∃ a, f a = b}\n"
-"```"
-msgstr ""
-
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "**Du**: Wie zeigt man denn schon wieder Gleichheit von Mengen?"
-msgstr ""
-
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "**Robo**: Ich habe ein relevantes Resultat gefunden: `mem_range`.\n"
-"Such das mal in denem Inventar!"
-msgstr ""
-
 #: Game.Levels.FunctionSurj.L14_choose
 msgid "Every function with nonempty fibres has a right inverse."
 msgstr ""
@@ -5176,15 +5151,6 @@ msgid "Als ihr das Problem gelöst habt, erschleicht euch ein starkes\n"
 "Also geht ihr zurück und nehmt die rechte Gabelung."
 msgstr ""
 
-#: Game.Levels.FunctionInj.L03_InjectiveRange
-msgid "Range of Injective"
-msgstr ""
-
-#: Game.Levels.FunctionInj.L03_InjectiveRange
-msgid "For an injective function `f : A → B` the fibres of the elements in the range\n"
-"are singletons."
-msgstr ""
-
 #: Game.Levels.FunctionInj.L04_Injective
 msgid "Monotone Funktionen"
 msgstr ""
@@ -5286,26 +5252,6 @@ msgstr ""
 msgid ""
 msgstr ""
 
-#: Game.Levels.FunctionInj.L08_LeftInvPreimage
-msgid "Preimage of the inverse"
-msgstr ""
-
-#: Game.Levels.FunctionInj.L08_LeftInvPreimage
-msgid "The image of a set `S : Set A` along a  function `f : A → B` is the set of all elements\n"
-"`b : B` that are the image of some element `a : A` in `S`. We denote it by `f '' S` and\n"
-"define it as below.\n"
-"```\n"
-"f '' S = {b : B | ∃ a : A, a ∈ S ∧ f a = b}\n"
-"```\n"
-"\n"
-"Note that an element of the image is a triple `⟨b, a, h⟩` where `b` is the image of `a` and `h`\n"
-"is the proof that `a` is in `S` and `f a = b`.\n"
-"\n"
-"The image of function with a left in\n"
-"verse is a subset of the preimage of the inverse of\n"
-"the same subset."
-msgstr ""
-
 #: Game.Levels.FunctionInj.L09_InjOfHasLeftInv
 msgid "Functions with left inverses are injective."
 msgstr ""
@@ -5323,11 +5269,11 @@ msgid ""
 msgstr ""
 
 #: Game.Levels.FunctionInj.L11_InjHasLeftInv
-msgid "Injections with nonempty domain have retract."
+msgid "Injections have a left inverse, and vice versa"
 msgstr ""
 
 #: Game.Levels.FunctionInj.L11_InjHasLeftInv
-msgid "In this level you show that an injective function with a nonempty domain has a left inverse."
+msgid ""
 msgstr ""
 
 #: Game.Levels.FunctionInj
@@ -5496,11 +5442,74 @@ msgstr ""
 msgid "In this level, you will prove that the the diagonal function is injective."
 msgstr ""
 
-#: Game.Levels.FunctionBij.L09_Preimage_Injective
+#: Game.Levels.FunctionBij
+msgid "Bijektivität"
+msgstr ""
+
+#: Game.Levels.FunctionBij
+msgid "Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf\n"
+"eine Insel komplett mit Wasser bedeckt zu sein scheint.\n"
+"\n"
+"Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,\n"
+"vereinzelte aus Lehm.\n"
+"\n"
+"Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt."
+msgstr ""
+
+#: Game.Levels.FunctionImage.L01_ImagePreimage
+msgid "Bild/Urbild"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L01_ImagePreimage
+msgid "`f '' S` ist das Bild,\n"
+"`f ⁻¹' V` das Urbild,\n"
+"\n"
+"`f '' S := {f a | a ∈ S}`\n"
+"`f ⁻¹' V := {a | f a ∈ V}`"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L01_ImagePreimage
+msgid ""
+msgstr ""
+
+#: Game.Levels.FunctionImage.L02_ImagePreimage
+msgid ""
+msgstr ""
+
+#: Game.Levels.FunctionImage.L03_InjectiveRange
+msgid "Range of Injective"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L03_InjectiveRange
+msgid "For an injective function `f : A → B` the fibres of the elements in the range\n"
+"are singletons."
+msgstr ""
+
+#: Game.Levels.FunctionImage.L04_LeftInvPreimage
+msgid "Preimage of the inverse"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L04_LeftInvPreimage
+msgid "The image of a set `S : Set A` along a  function `f : A → B` is the set of all elements\n"
+"`b : B` that are the image of some element `a : A` in `S`. We denote it by `f '' S` and\n"
+"define it as below.\n"
+"```\n"
+"f '' S = {b : B | ∃ a : A, a ∈ S ∧ f a = b}\n"
+"```\n"
+"\n"
+"Note that an element of the image is a triple `⟨b, a, h⟩` where `b` is the image of `a` and `h`\n"
+"is the proof that `a` is in `S` and `f a = b`.\n"
+"\n"
+"The image of function with a left in\n"
+"verse is a subset of the preimage of the inverse of\n"
+"the same subset."
+msgstr ""
+
+#: Game.Levels.FunctionImage.L05_Preimage_Injective
 msgid "Preimage of surjective is injective"
 msgstr ""
 
-#: Game.Levels.FunctionBij.L09_Preimage_Injective
+#: Game.Levels.FunctionImage.L05_Preimage_Injective
 msgid "Given a function `f : A → B` we obtain a function `preimage f : Set B → Set A`\n"
 "by taking the preimage of sets of `B`. Recall that\n"
 "```\n"
@@ -5510,22 +5519,37 @@ msgid "Given a function `f : A → B` we obtain a function `preimage f : Set B 
 "Show that `preimage f` is injective iff f is surjective."
 msgstr ""
 
-#: Game.Levels.FunctionBij.L09_Preimage_Injective
+#: Game.Levels.FunctionImage.L05_Preimage_Injective
 msgid "Now `change (f ⁻¹' {«{y}»}).Nonempty`"
 msgstr ""
 
-#: Game.Levels.FunctionBij
-msgid "Bijektivität"
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "Range of Surjection"
 msgstr ""
 
-#: Game.Levels.FunctionBij
-msgid "Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf\n"
-"eine Insel komplett mit Wasser bedeckt zu sein scheint.\n"
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "The range of a function is the set of all outputs.\n"
 "\n"
-"Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,\n"
-"vereinzelte aus Lehm.\n"
+"In this level you show that a function is surjective if and only if the range of\n"
+"the function is equal to the universal subset of the codomain. For `f : A → B`,\n"
+"the range of `f` is defined as\n"
 "\n"
-"Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt."
+"```\n"
+"range f : Set B := {b | ∃ a, f a = b}\n"
+"```"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "**Du**: Wie zeigt man denn schon wieder Gleichheit von Mengen?"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "**Robo**: Ich habe ein relevantes Resultat gefunden: `mem_range`.\n"
+"Such das mal in denem Inventar!"
+msgstr ""
+
+#: Game.Levels.FunctionImage
+msgid "Injektivität"
 msgstr ""
 
 #: Game
diff --git a/Game.lean b/Game.lean
index c15d239..97df290 100644
--- a/Game.lean
+++ b/Game.lean
@@ -18,6 +18,7 @@ import Game.Levels.NewStuff.Prime
 import Game.Levels.FunctionSurj
 import Game.Levels.FunctionInj
 import Game.Levels.FunctionBij
+import Game.Levels.FunctionImage
 -- import Game.Levels.SetTheory
 
 -- *uncomment the following line to get the incomplete planets.*
diff --git a/Game/Levels/FunctionBij.lean b/Game/Levels/FunctionBij.lean
index 7ed3d90..03a8cce 100644
--- a/Game/Levels/FunctionBij.lean
+++ b/Game/Levels/FunctionBij.lean
@@ -6,7 +6,6 @@ import Game.Levels.FunctionBij.L05_BijectionEquivalence
 import Game.Levels.FunctionBij.L06_CurryEquiv
 import Game.Levels.FunctionBij.L07_CurrySurjective
 import Game.Levels.FunctionBij.L08_Diagonal
-import Game.Levels.FunctionBij.L09_Preimage_Injective
 
 World "FunctionBij"
 Title "Bijektivität"
diff --git a/Game/Levels/FunctionImage.lean b/Game/Levels/FunctionImage.lean
new file mode 100644
index 0000000..a757b18
--- /dev/null
+++ b/Game/Levels/FunctionImage.lean
@@ -0,0 +1,9 @@
+import Game.Levels.FunctionImage.L01_ImagePreimage
+import Game.Levels.FunctionImage.L02_ImagePreimage
+import Game.Levels.FunctionImage.L03_InjectiveRange
+import Game.Levels.FunctionImage.L04_LeftInvPreimage
+import Game.Levels.FunctionImage.L05_Preimage_Injective
+import Game.Levels.FunctionImage.L06_SurjectiveRange
+
+World "FunctionImage"
+Title "Image/Preimage"
diff --git a/Game/Levels/FunctionImage/L01_ImagePreimage.lean b/Game/Levels/FunctionImage/L01_ImagePreimage.lean
new file mode 100644
index 0000000..f49b8ec
--- /dev/null
+++ b/Game/Levels/FunctionImage/L01_ImagePreimage.lean
@@ -0,0 +1,34 @@
+import Game.Metadata
+
+open Function Set
+
+World "FunctionImage"
+Level 1
+Title "Bild/Urbild"
+
+Introduction "
+`f '' S` ist das Bild,
+`f ⁻¹' V` das Urbild,
+
+`f '' S := {f a | a ∈ S}`
+`f ⁻¹' V := {a | f a ∈ V}`
+"
+
+/--  -/
+TheoremDoc Set.image_preimage_subset as "image_preimage_subset" in "Set"
+
+-- Set theory
+example {x : Nat} (h : x ∈ {a : ℕ | Even a}) : False := by
+  obtain ⟨⟩ := h
+  sorry
+
+Statement Set.image_preimage_subset {A B : Type} (f : A → B) (S : Set B) :
+f '' (f ⁻¹' S) ⊆ S := by
+  intro b
+  intro hb
+  simp at hb
+  obtain ⟨a, ha₁, ha₂⟩ := hb
+  rw [ha₂] at ha₁
+  assumption
+
+NewDefinition Set.image Set.preimage
diff --git a/Game/Levels/FunctionImage/L02_ImagePreimage.lean b/Game/Levels/FunctionImage/L02_ImagePreimage.lean
new file mode 100644
index 0000000..322e88c
--- /dev/null
+++ b/Game/Levels/FunctionImage/L02_ImagePreimage.lean
@@ -0,0 +1,22 @@
+import Game.Metadata
+
+
+World "FunctionImage"
+Level 2
+Title ""
+
+open Function Set
+
+Statement {A B : Type} {f : A → B} (hf : Surjective f) (s : Set B) :
+f '' (f ⁻¹' s) = s := by
+  ext b
+  simp
+  constructor
+  · apply image_preimage_subset -- Lvl 1
+  · intro hb
+    obtain ⟨a, ha⟩ := hf b
+    use a
+    constructor
+    · rw [ha]
+      assumption
+    · assumption
diff --git a/Game/Levels/FunctionInj/L03_InjectiveRange.lean b/Game/Levels/FunctionImage/L03_InjectiveRange.lean
similarity index 92%
rename from Game/Levels/FunctionInj/L03_InjectiveRange.lean
rename to Game/Levels/FunctionImage/L03_InjectiveRange.lean
index 5cb8615..3292e33 100644
--- a/Game/Levels/FunctionInj/L03_InjectiveRange.lean
+++ b/Game/Levels/FunctionImage/L03_InjectiveRange.lean
@@ -1,7 +1,6 @@
 import Game.Metadata
 
-
-World "FunctionInj"
+World "FunctionImage"
 Level 3
 
 Title "Range of Injective"
@@ -27,3 +26,5 @@ Statement Injective.exists_unique_of_mem_range {A B : Type} {f : A → B} (hf :
   · intro a' ha'
     apply hf
     rw [ha',ha]
+
+NewDefinition Set.Range
diff --git a/Game/Levels/FunctionInj/L08_LeftInvPreimage.lean b/Game/Levels/FunctionImage/L04_LeftInvPreimage.lean
similarity index 97%
rename from Game/Levels/FunctionInj/L08_LeftInvPreimage.lean
rename to Game/Levels/FunctionImage/L04_LeftInvPreimage.lean
index 47ffe41..68898ed 100644
--- a/Game/Levels/FunctionInj/L08_LeftInvPreimage.lean
+++ b/Game/Levels/FunctionImage/L04_LeftInvPreimage.lean
@@ -1,8 +1,8 @@
 import Game.Metadata
 
 
-World "FunctionInj"
-Level 8
+World "FunctionImage"
+Level 4
 
 Title "Preimage of the inverse"
 
diff --git a/Game/Levels/FunctionBij/L09_Preimage_Injective.lean b/Game/Levels/FunctionImage/L05_Preimage_Injective.lean
similarity index 97%
rename from Game/Levels/FunctionBij/L09_Preimage_Injective.lean
rename to Game/Levels/FunctionImage/L05_Preimage_Injective.lean
index 70bd8d1..252ae70 100644
--- a/Game/Levels/FunctionBij/L09_Preimage_Injective.lean
+++ b/Game/Levels/FunctionImage/L05_Preimage_Injective.lean
@@ -1,8 +1,8 @@
 import Game.Metadata
 
 
-World "FunctionBij"
-Level 9
+World "FunctionImage"
+Level 5
 
 Title "Preimage of surjective is injective"
 
diff --git a/Game/Levels/FunctionSurj/L13_SurjectiveRange.lean b/Game/Levels/FunctionImage/L06_SurjectiveRange.lean
similarity index 97%
rename from Game/Levels/FunctionSurj/L13_SurjectiveRange.lean
rename to Game/Levels/FunctionImage/L06_SurjectiveRange.lean
index 6482b6e..e9e84b5 100644
--- a/Game/Levels/FunctionSurj/L13_SurjectiveRange.lean
+++ b/Game/Levels/FunctionImage/L06_SurjectiveRange.lean
@@ -1,8 +1,8 @@
 import Game.Metadata
 
 
-World "FunctionSurj"
-Level 13
+World "FunctionImage"
+Level 6
 
 Title "Range of Surjection"
 
diff --git a/Game/Levels/FunctionImage/LXX_Set6.lean b/Game/Levels/FunctionImage/LXX_Set6.lean
new file mode 100644
index 0000000..0d053c5
--- /dev/null
+++ b/Game/Levels/FunctionImage/LXX_Set6.lean
@@ -0,0 +1,15 @@
+import Game.Metadata
+
+open Set
+
+-- DELETE?
+
+example (f : ℝ → ℝ) (hfib : ncard (f ⁻¹' {0}) = 2) : ∃ (x₁ x₂ : ℝ ), x₁ ≠ x₂ ∧ f x₁ = 0 ∧ f x₂ = 0 := by
+  apply ncard_eq_two.mp at hfib
+  obtain ⟨ x₁, x₂, h_ne, h_fib_eq ⟩ := hfib
+  use x₁, x₂
+  constructor
+  assumption
+  change x₁ ∈ f ⁻¹' {0} ∧ x₂ ∈ f ⁻¹' {0}
+  rw [h_fib_eq]
+  tauto
diff --git a/Game/Levels/FunctionInj.lean b/Game/Levels/FunctionInj.lean
index 291bf73..324fb8c 100644
--- a/Game/Levels/FunctionInj.lean
+++ b/Game/Levels/FunctionInj.lean
@@ -1,11 +1,9 @@
 import Game.Levels.FunctionInj.L01_Injective
 import Game.Levels.FunctionInj.L02_Injective
-import Game.Levels.FunctionInj.L03_InjectiveRange
 import Game.Levels.FunctionInj.L04_Injective
 import Game.Levels.FunctionInj.L05_Injective
 import Game.Levels.FunctionInj.L06_SuccHasLeftInv
 import Game.Levels.FunctionInj.L07_Extend
-import Game.Levels.FunctionInj.L08_LeftInvPreimage
 import Game.Levels.FunctionInj.L09_InjOfHasLeftInv
 import Game.Levels.FunctionInj.L10_RightInvOfLeftInv
 import Game.Levels.FunctionInj.L11_InjHasLeftInv
diff --git a/Game/Levels/FunctionInj/L04_Injective.lean b/Game/Levels/FunctionInj/L04_Injective.lean
index 369e1ac..f375777 100644
--- a/Game/Levels/FunctionInj/L04_Injective.lean
+++ b/Game/Levels/FunctionInj/L04_Injective.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 4
+Level 3
 
 Title "Monotone Funktionen"
 
diff --git a/Game/Levels/FunctionInj/L05_Injective.lean b/Game/Levels/FunctionInj/L05_Injective.lean
index 3edc215..69c55b8 100644
--- a/Game/Levels/FunctionInj/L05_Injective.lean
+++ b/Game/Levels/FunctionInj/L05_Injective.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 5
+Level 4
 
 Title "Monotone Funktionen"
 
diff --git a/Game/Levels/FunctionInj/L06_SuccHasLeftInv.lean b/Game/Levels/FunctionInj/L06_SuccHasLeftInv.lean
index 350db50..03c88a1 100644
--- a/Game/Levels/FunctionInj/L06_SuccHasLeftInv.lean
+++ b/Game/Levels/FunctionInj/L06_SuccHasLeftInv.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 6
+Level 5
 
 Title "Left Inverse"
 
diff --git a/Game/Levels/FunctionInj/L07_Extend.lean b/Game/Levels/FunctionInj/L07_Extend.lean
index b5f3921..d750516 100644
--- a/Game/Levels/FunctionInj/L07_Extend.lean
+++ b/Game/Levels/FunctionInj/L07_Extend.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 7
+Level 6
 
 Title "Choosing an arbitrary element of a nonempty type."
 
diff --git a/Game/Levels/FunctionInj/L09_InjOfHasLeftInv.lean b/Game/Levels/FunctionInj/L09_InjOfHasLeftInv.lean
index c663014..92d5c85 100644
--- a/Game/Levels/FunctionInj/L09_InjOfHasLeftInv.lean
+++ b/Game/Levels/FunctionInj/L09_InjOfHasLeftInv.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 9
+Level 7
 
 Title "Functions with left inverses are injective."
 
diff --git a/Game/Levels/FunctionInj/L10_RightInvOfLeftInv.lean b/Game/Levels/FunctionInj/L10_RightInvOfLeftInv.lean
index c2b7714..8ac6e3d 100644
--- a/Game/Levels/FunctionInj/L10_RightInvOfLeftInv.lean
+++ b/Game/Levels/FunctionInj/L10_RightInvOfLeftInv.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 10
+Level 8
 
 Title "Injections with nonempty domain have retract."
 
diff --git a/Game/Levels/FunctionInj/L11_InjHasLeftInv.lean b/Game/Levels/FunctionInj/L11_InjHasLeftInv.lean
index 2166947..09eb1da 100644
--- a/Game/Levels/FunctionInj/L11_InjHasLeftInv.lean
+++ b/Game/Levels/FunctionInj/L11_InjHasLeftInv.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 11
+Level 9
 
 Title "Injections have a left inverse, and vice versa"
 
@@ -18,7 +18,7 @@ open Function Set
 Statement {A B : Type} [hA : Nonempty A] (f : A → B ) : ∀ b : B, ∃ a : A, f a = b ∨ ¬ ∃ a' : A , f a' = b   := by
   have a₀ : A := Classical.arbitrary A
   intro b
-  by_cases hb : ∃ a' : A, f a' = b 
+  by_cases hb : ∃ a' : A, f a' = b
   · obtain ⟨a,ha⟩ := hb
     use a
     left
@@ -37,7 +37,7 @@ Statement injective_iff_hasLeftInverse {A B : Type} [hA : Nonempty A]  (f : A 
       /- exactly a previous level, now without hints -/
       have a₀ : A := Classical.arbitrary A
       intro b
-      by_cases hb : ∃ a' : A, f a' = b 
+      by_cases hb : ∃ a' : A, f a' = b
       · obtain ⟨a,ha⟩ := hb
         use a
         left
@@ -52,9 +52,9 @@ Statement injective_iff_hasLeftInverse {A B : Type} [hA : Nonempty A]  (f : A 
     obtain hpos | hneg := hg (f a)
     · assumption
     · push_neg at hneg
-      have : f a ≠ f a := hneg a 
+      have : f a ≠ f a := hneg a
       contradiction
-  · /- Injective f → HasLeftInverse f 
+  · /- Injective f → HasLeftInverse f
        exactly a previous level, now without hints-/
     intro hL
     intro a a' ha
@@ -63,4 +63,3 @@ Statement injective_iff_hasLeftInverse {A B : Type} [hA : Nonempty A]  (f : A 
     unfold LeftInverse at hg
     rw [hg a, hg a'] at ha
     assumption
-
diff --git a/Game/Levels/FunctionSurj.lean b/Game/Levels/FunctionSurj.lean
index afad8c1..aad9514 100644
--- a/Game/Levels/FunctionSurj.lean
+++ b/Game/Levels/FunctionSurj.lean
@@ -10,7 +10,6 @@ import Game.Levels.FunctionSurj.L09_LeftInverse
 import Game.Levels.FunctionSurj.L10_RightInverse
 import Game.Levels.FunctionSurj.L11_Surjective
 import Game.Levels.FunctionSurj.L12_Surjective
-import Game.Levels.FunctionSurj.L13_SurjectiveRange
 import Game.Levels.FunctionSurj.L14_choose
 import Game.Levels.FunctionSurj.L15_SurjectiveTFAE
 
diff --git a/Game/Levels/FunctionSurj/L14_choose.lean b/Game/Levels/FunctionSurj/L14_choose.lean
index 6aa62fd..4cc0db4 100644
--- a/Game/Levels/FunctionSurj/L14_choose.lean
+++ b/Game/Levels/FunctionSurj/L14_choose.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionSurj"
-Level 14
+Level 13
 
 Title "Every function with nonempty fibres has a right inverse."
 
diff --git a/Game/Levels/FunctionSurj/L15_SurjectiveTFAE.lean b/Game/Levels/FunctionSurj/L15_SurjectiveTFAE.lean
index 3de688a..8540a1d 100644
--- a/Game/Levels/FunctionSurj/L15_SurjectiveTFAE.lean
+++ b/Game/Levels/FunctionSurj/L15_SurjectiveTFAE.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionSurj"
-Level 15
+Level 14
 
 Title "Every surjection has a right inverse"