levels

2023-02-13 17:48:11 +01:00
parent 992781ba11
commit af3afc3a94
32 changed files with 658 additions and 74 deletions
@@ -7,6 +7,8 @@ import TestGame.Levels.Contradiction
 import TestGame.Levels.Prime
 import TestGame.Levels.Induction

+import TestGame.Levels.Numbers
+
 import TestGame.Levels.LeanStuff
 import TestGame.Levels.SetTheory
 import TestGame.Levels.Function
@@ -39,9 +41,9 @@ Conclusion


 Path Proposition → Implication → Predicate → Prime
-Path Predicate → Contradiction → LeanStuff → SetTheory → SetFunction
+Path Predicate → Contradiction → LeanStuff → SetTheory → SetTheory2 → SetFunction
 Path Predicate → Induction → LeanStuff → Function → SetFunction
-Path SetTheory → SetTheory2
+Path SetTheory2 → Numbers


 MakeGame
@@ -35,18 +35,18 @@ bevor du dann mit dem Beweis forfährst.
 Statement
    "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
    $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
-    (A B : Prop) (h : A → ¬ B) (g : A ∧ B) : False := by
-  rcases g with ⟨h₁, h₂⟩
+    (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
+  rcases k with ⟨h₁, h₂⟩
  have h₃ : ¬ B
  apply h
  assumption
  contradiction

-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False =>
+Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
 " Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
 "

-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>
+Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
 "
 Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\"

@@ -63,6 +63,7 @@ have k : ¬ B

 Conclusion ""

-NewTactics contradiction rcases haveₓ assumption apply
+NewTactics «have»
+DisabledTactics «suffices»

 NewLemmas Even Odd not_even not_odd
@@ -23,7 +23,7 @@ suffices h : [Aussage]
 [Beweis des Goals (mithilfe von h)]
 [Beweis der Aussage h]
 ```
-Auf Deutsch entspricht `suffices h : [Aussage]` dem Ausdruck
+Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
 \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"

 Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
@@ -35,18 +35,18 @@ dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen
 Statement
    "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
    $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
-    (A B : Prop) (h : A → ¬ B) (g : A ∧ B) : False := by
-  rcases g with ⟨h₁, h₂⟩
+    (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
+  rcases k with ⟨h₁, h₂⟩
  suffices k : ¬ B
  contradiction
  apply h
  assumption

-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False =>
+Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
 " Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
 "

-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>
+Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
 " Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\"

  In Lean :
@@ -60,6 +60,7 @@ Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>

 Conclusion ""

-NewTactics contradiction apply assumption rcases sufficesₓ
+NewTactics «suffices»
+DisabledTactics «have»

 NewLemmas Even Odd not_even not_odd
@@ -52,4 +52,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>

 Conclusion ""

-NewTactics by_contra sufficesₓ haveₓ contradiction apply assumption
+NewTactics by_contra contradiction apply assumption
@@ -46,4 +46,4 @@ HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>

 Conclusion ""

-NewTactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption
+NewTactics contradiction constructor intro by_contra apply assumption
@@ -1,4 +1,11 @@
-import TestGame.Levels.Function.L01_xxx
+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

 Game "TestGame"
 World "Function"
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 1
+
+Title ""
+
+Introduction
+"
+Funktionen werden in Lean mit `ℕ → ℕ` geschrieben (`\\to`), also dem gleichen
+Pfeil wie Implikationen.
+
+Eine abstrakte Funktion ist ein entsprechendes Element `(f : ℕ → ℕ)` oder `(g : ℕ → ℝ)`.
+Dies sagt aber gar nichts darüber, wie `f` tatsächlich definiert ist.
+
+Hat man eine Funktion `(f : A → B)` und ein Element `(x : A)` dann ist `f x` der
+Bildpunkt in `B`. In Lean braucht man also keine Klammern um $f(x)$ zu schreiben.
+
+Eplizite, anonyme Funktionen kann man mit dem Syntax `fun (n : ℕ) ↦ n ^ 2` definieren
+(entweder `↦` (`\\map`) oder `=>` als Pfeil in der Mitte).
+"
+
+Statement
+"Zeige, dass es eine Funktion $\\mathbb{N} \\to \\mathbb{Z}$ gibt, für die $f(x) < x$ gilt."
+    : ∃ f : ℕ → ℤ, ∀ x, f x < x := by
+  use (fun x ↦ x - 1)
+  simp
@@ -1,26 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Function"
-Level 1
-
-Title "Abbildungen"
-
-Introduction
-"
-In diesem Kapitel lernen wir mit Abbildungen/Funktionen umzugehen.
-
-Funktionen auf `ℕ`.
-
-"
-
-Statement
-    "TODO"
-    : True := by
-  trivial
-
-NewTactics rw
@@ -0,0 +1,59 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 2
+
+Title ""
+
+Introduction
+"
+Ausserhalb eines Beweises kann man Funktionen mit `def`
+(anstatt `lemma`/`example`/`theorem`) definieren:
+
+```
+def f (x : ℚ) : ℚ := 1 / (1 + x^2)
+
+def f : ℚ → ℚ := fun x ↦ 1 / (1 + x^2)
+```
+
+(die beiden Varianten sind äquivalent.)
+
+Um eine anonyme Funktion `fun x ↦ 1 / (1 + x^2)` innerhalb eines Beweis einem Namen
+zuzuordnen, benützt man `let`:
+
+```
+let f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
+```
+
+Die Taktiken `let` und `have` sind fast gleich, mit einem wichtigen Unterschied. Mit
+
+```
+have f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
+```
+
+vergisst Lean sofort wie `f` konstruiert wurde, und weiss nur noch dass es eine Funktion
+`(f : ℕ → ℕ)` gibt. Mit `let` kann Lean jederzeit auf die Definition von `f` zugreifen.
+"
+
+def f (x : ℤ) : ℤ := (x + 1) ^ 2
+
+Statement
+"
+Given the function
+```
+def f (x : ℤ) : ℤ := (x + 1) ^ 2
+```
+show that $f(x) = x^2 + 2x + 1$.
+
+"
+    : ∀ x, f x = x ^ 2 + 2 * x + 1 := by
+  intro x
+  unfold f
+  ring
+
+Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
+"If your function has been defined with a `def` then usually you need to use `unfold f` to
+help Lean replacing it with it's definition (alternatively `sim [f]`
+oder `rw [f]` funktionieren auch)."
@@ -0,0 +1,20 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 3
+
+Title ""
+
+Introduction
+"
+Komposition von Funktionen kann als `g ∘ f` geschrieben werden.
+
+TODO
+"
+
+Statement
+"TODO: Find an exercise."
+    (U S T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x)  := by
+  trivial
@@ -0,0 +1,27 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 4
+
+Title ""
+
+Introduction
+"
+"
+
+open Set
+
+def f2 : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+
+#eval (f2 + f2) 2
+
+#check range f2
+
+Statement
+""
+    : True := by
+  trivial
+
+#check Set.piecewise
@@ -0,0 +1,24 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 5
+
+Title ""
+
+Introduction
+"
+"
+open Set Function
+
+def f3 : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+
+#eval (f3 + f3) 2
+
+example : ¬ f3.Injective := by
+  unfold Injective
+  push_neg
+  use 2
+  use 3
+  simp
@@ -0,0 +1,19 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 6
+
+Title ""
+
+Introduction
+"
+"
+
+Statement
+""
+ : (fun (n : ℤ) ↦ n + 1).Injective := by
+  intro a b hab
+  simp at hab
+  assumption
@@ -0,0 +1,19 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 7
+
+Title "Surjektive"
+
+Introduction
+"
+"
+
+Statement
+""
+: (fun (n : ℤ) ↦ n + 1).Surjective := by
+  intro y
+  use y-1
+  simp
@@ -0,0 +1,23 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 8
+
+Title ""
+
+Introduction
+"
+"
+
+Statement
+""
+  : (fun (n : ℤ) ↦ n + 1).Bijective := by
+  constructor
+  intro a b hab
+  simp at hab
+  assumption
+  intro y
+  use y-1
+  simp
@@ -1,4 +1,6 @@
-import TestGame.Levels.LeanStuff.L01_xxx
+import TestGame.Levels.LeanStuff.L01_Type
+import TestGame.Levels.LeanStuff.L02_Universe
+import TestGame.Levels.LeanStuff.L03_ImplicitArguments

 Game "TestGame"
 World "LeanStuff"
@@ -0,0 +1,42 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "LeanStuff"
+Level 1
+
+Title "Typen"
+
+Introduction
+"
+Dieses Kapitel führt ein paar Lean-spezifische Sachen ein, die du wissen solltest.
+
+Mathematisch haben diese Sachen keinen Inhalt, aber es ist wichtig, dass du etwas
+verstehst wie Lean manche Sachen macht.
+
+Als erstes geht es um Typen.
+
+Oft sieht man Argumente von der Form `(U : Type)` was heisst \"sei $U$ ein Typ.\"
+Als Mathematiker kann man sich Typen ein bisschen wie Mengen vorstellen, in dem Sinn
+dass sie die Grundlage der Mathematik bilden: Alles sind Typen.
+
+Zum Beispiel ist `ℕ` der Typ der natürlichen Zahlen, `Prop` der Typ der logischen
+Aussagen, und ein Ring ist ein Typ `(R : Type)` zusammen mit einer Instanz `[Ring R]`,
+die sagt, dass auf diesem Typ eine Ringstruktur besteht.
+
+**Achtung**: Wie du aber gleich sehen wirst sind Typen und Mengen in Lean komplett
+unterschiedliche Sachen! (Und Mengen nehmen in Lean nicht die fundamentale Funktion
+ein, die sie in der Mathe innehaben.)
+"
+
+Statement
+""
+    (R : Type) [CommRing R] (a b : R) : a + b = b + a := by
+  ring
+
+Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
+"Die Taktik `ring` funktioniert in jedem Typen,
+der mindestens eine Instanz `[Ring R]` hat."
@@ -17,10 +17,36 @@ Dieses Kapitel führt ein paar Lean-spezifische Sachen ein, die du wissen sollte
 Mathematisch haben diese Sachen keinen Inhalt, aber es ist wichtig, dass du etwas
 verstehst wie Lean manche Sachen macht.

+Als erstes geht es um implizite und explizite Argumente von Lemmas. **Explizite Argumente**
+schreibt man mit runden Klammern `()`, **impliziete Argumente** mit geschweiften `{}`.

- Implizite und explizite Argumente.
- Types
+Als implizit werden alle Argumente markiert, die Lean selbständig aus dem Kontext
+erschliessen und einfüllen kann.

+Als Beispiel hier zweimal das gleiche Lemma, einmal ohne impliziten Argumenten und einmal mit
+```
+lemma not_or_of_imp' (A B : Prop) (h : A → B) : ¬A ∨ B := sorry
+
+lemma not_or_of_imp {A B : Prop} (h : A → B) : ¬A ∨ B := sorry
+```
+
+Hat man nun `g : C → D` dann braucht man diese Lemmas mit
+`have := not_or_of_imp g` oder `have := not_or_of_imp' C D g`.
+
+Wie man sieht erschliesst Lean die impliziten Argumente automatisch und es wäre deshalb
+unnötig, diese jedes Mal explizit angeben zu müssen.
+
+TODO
+(Trick mit `@not_or_of_imp` kann man sagen, dass man **alle** Argumente angeben möchte und mir
+`not_or_of_imp g (B := D)` könnte man ein spezifisches implizites Argument spezifizieren.
+Wenn man diese Tricks braucht, heisst das aber meistens, das etwas nicht optimal definiert
+ist.)
+
+TODO
+Zudem gibt es noch Argumente in eckigen Klammern `[]`. Dies sind auch implizite
+Argumente, die aber von der **Instance Resolution** gefüllt werden sollen. Dies
+wird später kommen, aber ein typisches Beispiel ist `(S : Type _) [ring S]` was Lean
+sagt, es soll suchen gehen, ob es weiss, dass `S` ein Ring ist.
 "

 open Set
@@ -30,3 +56,6 @@ Statement
  trivial

 NewTactics rw
+
+#check not_not
+#check not_or_of_imp
@@ -0,0 +1,37 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "LeanStuff"
+Level 2
+
+Title "Universen"
+
+Introduction
+"
+In der Mathematik stösst man manchmal an Mengentheoretische Grenzen, und so auch in Lean.
+
+Klassisch ist bekannt dass die \"Menge aller Mengen\" nicht existieren kann.
+
+Falls man an diese Grenzen stösst (z.B. in der Mengenlehre oder Kategorientheorie) hat Lean
+Universen bereit: `Type` ist eigentlich `Type 0` und es gibt auch `Type 1, Type 2, ...`
+
+Deshalb sieht man oft in Lean-Code `(R : Type _)` wenn es keine mengentheoretischen
+Probleme gibt (`_` ist ein Platzhalter) oder `universe u` am Anfang und dann `(R : Type u)`
+falls man diese mengentheoretischen Probleme kontrollieren muss.
+
+In der Praxis kommt man aber relativ weit, wenn man sich erst mal nicht mit Universen
+beschäftigt, und lediglich weiss, dass es sowas gibt.
+"
+
+Statement
+"TODO"
+    (R S : Type _) [CommRing R] (a b : R) : a + b = b + a := by
+  ring
+
+Hint (R : Type _) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
+"Die Taktik `ring` funktioniert in jedem Typen,
+der mindestens eine Instanz `[Ring R]` hat."
@@ -0,0 +1,57 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "LeanStuff"
+Level 3
+
+Title "Implizite Argumente"
+
+Introduction
+"
+
+Auch wichtiger Syntax ist der Unterschied zwischen
+impliziten und expliziten Argumenten von Lemmas. **Explizite Argumente**
+schreibt man mit runden Klammern `()`, **impliziete Argumente** mit geschweiften `{}`.
+
+Als implizit werden alle Argumente markiert, die Lean selbständig aus dem Kontext
+erschliessen und einfüllen kann.
+
+Als Beispiel hier zweimal das gleiche Lemma, einmal ohne impliziten Argumenten und einmal mit
+```
+lemma not_or_of_imp' (A B : Prop) (h : A → B) : ¬A ∨ B := sorry
+
+lemma not_or_of_imp {A B : Prop} (h : A → B) : ¬A ∨ B := sorry
+```
+
+Hat man nun `g : C → D` dann braucht man diese Lemmas mit
+`have := not_or_of_imp g` oder `have := not_or_of_imp' C D g`.
+
+Wie man sieht erschliesst Lean die impliziten Argumente automatisch und es wäre deshalb
+unnötig, diese jedes Mal explizit angeben zu müssen.
+
+TODO
+(Trick mit `@not_or_of_imp` kann man sagen, dass man **alle** Argumente angeben möchte und mir
+`not_or_of_imp g (B := D)` könnte man ein spezifisches implizites Argument spezifizieren.
+Wenn man diese Tricks braucht, heisst das aber meistens, das etwas nicht optimal definiert
+ist.)
+
+
+Nebenbemerkung: Es gibt auch noch implizite **Klassen-Elemente** mit eckigen Klammern `[]`
+wie zum Beispiel `[CommRing R]` im vorigen Beispiel. Diese werden später behandelt,
+und sagen Lean, dass es für dieses Argument eine **Instanz** suchen gehen soll. Diese
+Instanzen werden mehrheitlich dafür verwendet, mathematische Strukturen auf Typen zu
+definieren, aber das kommt alles später.
+"
+
+Statement
+"TODO"
+    (R S : Type _) [CommRing R] (a b : R) : a + b = b + a := by
+  ring
+
+Hint (R : Type _) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
+"Die Taktik `ring` funktioniert in jedem Typen,
+der mindestens eine Instanz `[Ring R]` hat."
@@ -0,0 +1,2 @@
+import TestGame.Levels.Numbers.L01_PNat
+import TestGame.Levels.Numbers.L02_PNat
@@ -0,0 +1,82 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Numbers"
+Level 1
+
+Title ""
+
+Introduction
+"
+-- Level name : Positive natürliche Zahlen
+
+import data.pnat.basic
+
+/-
+In diesem Level lernst du neben `ℕ` weitere Arten von
+Zahlen kennen: `ℕ+`,`ℤ`, `ℚ`, `ℝ`, `ℂ`.
+
+Manchmal sieht man in der Literatur Diskussionen, ob die natürlichen Zahlen jetzt bei `0` oder `1`
+anfangen, wobei zumindest in der formalisierten Mathematik (z.B. ZFC-Mengenlehre)
+eigentlich immer `ℕ = {0, 1, 2, 3, …}` definiert wird.
+
+So ist auch in Lean `1` als `0.succ` und `2 = 1.succ = 0.succ.succ` definiert und
+Lean hat eine separate Notation `ℕ+` (oder `pnat`) für alle *positiven* natürlichen Zahlen.
+
+Dies ist als Sub-Typ von `ℕ` definiert:
+`def pnat := {n : ℕ // 0 < n}`
+
+ein Element `(p : ℕ+)` besteht also aus einer natürlichen Zahl `(p.val : ℕ)`
+(oder auch `p.1`, wobei `p.val` bevorzugt ist) sowie einem Beweis, dass diese positiv ist,
+`p.property` (oder `p.2`).
+
+Solche Strukturen mit mehr als einem Feld kann man in Lean mit dem anonymen Konstruktor `⟨_, _⟩`
+erstellen, wie du schon einmal beim `∃` gesehen hast: `(⟨n, h⟩ : ℕ+)`
+"
+
+Statement
+""
+    (a : ℕ+) : (a : ℕ) ≠ 0 := by
+  apply ne_of_gt
+  rcases a with ⟨a, ha⟩
+  assumption
+
+
+-- -/
+
+-- /- Hint : a.property
+-- `have ha := a.property` speichert die `ℕ+`-Eigenschaft dass `0 < a.val`
+-- gilt als neue Variable.
+-- -/
+
+-- /- Hint : ne_of_lt/ne_of_gt
+-- `a < b → a ≠ b`
+-- oder
+-- `a < b → b ≠ a`
+
+-- alternativ kannst du auch mit `symmetry` ein symmetrischen Goal drehen.
+-- -/
+
+-- /- Lemma : no-side-bar
+-- Beweise.
+-- -/
+-- example (a : ℕ+) : (a : ℕ) ≠ 0 :=
+-- begin
+--   have ha := a.property,
+--   symmetry,
+--   apply ne_of_lt,
+--   exact ha,
+-- end
+
+-- /- Axiom : ne_of_lt
+-- `a < b → a ≠ b`.
+-- -/
+
+-- /- Axiom : ne_of_gt
+-- `a < b → b ≠ a`.
+-- -/
+
+-- /- Tactic : symmetry
+-- Dreht ein symmetrisches Goal wie `A = B`, `A ≠ B`, `A ↔ B`, ...
+-- -/
@@ -0,0 +1,24 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Numbers"
+Level 2
+
+Title ""
+
+Introduction
+"
+  Das Lemma, das du gerade bewiesen hast, findest du als `pnat.ne_zero`
+"
+
+Statement
+""
+    (a b : ℕ+) : (a : ℕ) * b ≠ 0 := by
+  by_contra h
+  rw [Nat.mul_eq_zero] at h
+  cases h
+  have := PNat.ne_zero a
+  contradiction
+  have := PNat.ne_zero b
+  contradiction
@@ -32,7 +32,7 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B =>
 HiddenHint (A : Prop) (hA : A) : A =>
  "Du hast einen Beweis dafür in den *Annahmen*."

-NewTactics constructor assumption
+NewTactics constructor
 DisabledTactics tauto

 -- Statement
@@ -33,7 +33,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B =>
 HiddenHint (A : Prop) (hA : A) : A =>
  "Du hast einen Beweis dafür in den *Annahmen*."

-NewTactics constructor assumption
+NewTactics rcases
 DisabledTactics tauto

 -- Statement
@@ -1,4 +1,7 @@
-import TestGame.Levels.SetFunction.L01_xxx
+import TestGame.Levels.SetFunction.L01_Image
+import TestGame.Levels.SetFunction.L02_Preimage
+import TestGame.Levels.SetFunction.L03_Range
+import TestGame.Levels.SetFunction.L04_ImageUnion

 Game "TestGame"
 World "SetFunction"
@@ -0,0 +1,65 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "SetFunction"
+Level 1
+
+Title ""
+
+open Set
+
+Introduction
+"
+Wenn man mit Abildungen auf Mengen arbeitet, muss man in Lean etwas aufpassen, um
+die Typen (z.B. `(U : Type _)`) und Mengen von diesen Typen (z.B. `(S : Set U)`)
+zu unterscheiden.
+
+Abbildungen sind prinzipiell immer auf Typen definiert. Wenn eine Funktion nicht
+auf dem ganzen Typen definiert ist, hat man prinzipiell zwei Optionen:
+
+1. Nach dem Motto \"Chunk in, chunk out\" werden in der Mathlib Funktionen
+oft einfach auf irgendwas gesetzt wenn sie nicht definiert sind, so gibt `1 / 0` in `ℕ`
+einfach `0`. Dies funktioniert, weil dann alle relevanten Theoreme, die von `x / n`
+handeln, dann Annahmen der Form `(h : n ≠ 0)` haben.
+2. Man kann auch Funktionen auf *Subtypen* definieren, also z.B. auf `ℕ+`.
+
+
+"
+
+
+--     /- Image of Union -/
+-- lemma image_unionₓ
+
+Statement
+""
+    (S T : Set ℕ) (f : ℕ → ℕ) : (f '' S) ∪ (f '' T) = f '' (S ∪ T) := by
+  ext i
+  rw [mem_union]
+  simp_rw [mem_image]
+  constructor
+  intro h
+  rcases h with ⟨x, hx, hx'⟩ | ⟨x, hx, hx'⟩
+  use x
+  constructor
+  apply mem_union_left
+  assumption
+  assumption
+  use x
+  constructor
+  apply mem_union_right
+  assumption
+  assumption
+  rintro ⟨x, hx, hx'⟩
+  rw [mem_union] at hx
+  rcases hx with hx | hx
+  left
+  use x
+  constructor
+  assumption
+  assumption
+  right
+  use x
+  constructor
+  assumption
+  assumption
@@ -1,24 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "SetFunction"
-Level 1
-
-Title "Abbildungen"
-
-Introduction
-"
-Fortsetzung: Funktionen auf Mengen.
-
-"
-
-Statement
-    "TODO"
-    : True := by
-  trivial
-
-NewTactics rw
@@ -0,0 +1,21 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "SetFunction"
+Level 2
+
+Title ""
+
+Introduction
+"
+"
+
+Statement
+""
+    (U : Set ℕ) (f : ℕ → ℕ) : U ⊆ f ⁻¹' (f '' U) := by
+  intro x hx
+  use x
+  constructor
+  assumption
+  rfl
@@ -0,0 +1,21 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "SetFunction"
+Level 3
+
+Title ""
+
+Introduction
+"
+"
+
+Statement
+""
+    (U : Set ℕ) (f : ℕ → ℕ) : U ⊆ f ⁻¹' (f '' U) := by
+  intro x hx
+  use x
+  constructor
+  assumption
+  rfl
@@ -0,0 +1,18 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "SetFunction"
+Level 4
+
+Title ""
+
+Introduction
+"
+"
+
+Statement
+""
+    (I U V : Type _) (f : U → V) (N : I → Set V) :
+    f ⁻¹' (⋃ (i : I), N i) = ⋃ i, f ⁻¹' (N i) := by
+  simp
@@ -208,14 +208,14 @@ TacticDoc use
 TODO
 "

-TacticDoc sufficesₓ
+TacticDoc «suffices»
 "
 ## Beschreibung

 TODO
 "

-TacticDoc haveₓ
+TacticDoc «have»
 "
 ## Beschreibung