set theory levels

2023-02-02 14:44:58 +01:00
parent 73a44bd057
commit 404f346920
52 changed files with 1602 additions and 37 deletions
@@ -0,0 +1,42 @@
+import TestGame.Metadata
+
+import Mathlib.Init.Set
+import Mathlib.Tactic.Tauto
+
+set_option tactic.hygienic false
+set_option autoImplicit false
+
+Game "TestGame"
+World "SetTheory"
+Level 1
+
+Title "Mengen"
+
+Introduction
+"
+In diesem Kapitel schauen wir uns Mengen an.
+
+Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst,
+alle Elemente in einer Menge haben den gleichen Typ.
+
+Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine
+Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben.
+
+Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus
+`X`.  `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied
+zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht
+austauschbar!
+
+Um zu beweisen, dass etwas in `univ` ist, kannst du verschiedenste deiner Taktiken anwenden,
+zum Beispiel `tauto`.
+"
+
+open Set
+
+Statement mem_univ
+    "4 ist ein Element der Menge aller natürlichen Zahlen." {A : Type _} (x : A) :
+    x ∈ (univ : Set A) := by
+  trivial
+  -- tauto
+
+Tactics tauto trivial
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+
+import Mathlib.Init.Set
+import Mathlib.Tactic.Tauto
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 2
+
+Title "leere Menge"
+
+Introduction
+"
+Gleich wie bei `univ` gibt es leere Mengen `∅` von verschiedenen Typen.
+So ist `(∅ : Set ℕ)` in Lean nicht das gleiche wie `(∅ : Set ℤ)`. (`\\empty`)
+
+Zudem hat die Verneinung `¬ (x ∈ A)` die Notation `x ∉ A` (`\\nin`), gleich wie bei `=` and `≠`.
+
+Um zu zeigen, dass etwas nicht in der leeren Menge ist, kannst du wieder `tauto` verwenden.
+"
+
+open Set
+
+Statement not_mem_empty
+    "Kein Element ist in der leeren Menge enthalten." {A : Type _} (x : A) :
+    x ∉ (∅ : Set A) := by
+  tauto
@@ -0,0 +1,45 @@
+import TestGame.Metadata
+
+import Mathlib.Init.Set
+import Mathlib.Tactic.Tauto
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 3
+
+Title "Teilmengen"
+
+Introduction
+"
+Hat man zwei Mengen `(A B : Set ℕ)` kann man fragen, ob diese Teilmengen
+voneinander sind: `A ⊆ B` (`\\sub`/`\\ss`) ist die Notation für Teilmengen, die auch gleich
+sein können.
+
+`A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert, das heisst, ein `⊆` kann immer auch mit `intro x hx`
+angegangen werden.
+
+Die Taktik `tauto` macht das automatisch, aber um dies zu lernen ist `tauto` hier deaktiviert.
+Benutze also `intro`:
+"
+
+namespace MySet
+
+open Set
+
+theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by
+  trivial
+
+theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
+  tauto
+
+Statement subset_empty_iff
+"." (A : Set ℕ) : A ⊆ univ := by
+  intro h hA
+  apply mem_univ -- or `trivial`.
+
+Tactics intro trivial apply
+-- blocked: tauto simp
+
+end MySet
@@ -0,0 +1,61 @@
+import TestGame.Metadata
+import TestGame.Levels.SetTheory.L03_Subset
+
+import Mathlib.Init.Set
+import Mathlib.Tactic.Tauto
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 4
+
+Title "Teilmengen"
+
+Introduction
+"
+Ein zentrales Lemma ist `Subset.antisymm_iff` welches folgendes sagt:
+
+```
+A = B ↔ A ⊆ B ∧ B ⊆ A
+```
+
+Fast immer wenn man Gleichheiten von Mengen zeigen muss, will man diese in zwei Ungleichungen
+aufteilen.
+"
+
+namespace MySet
+
+open Set
+
+-- Copied some lemmas from `Matlib.Data.Set.Basic` in order to not import the entire file.
+theorem tmp {α : Type _} {s t : Set α} : s = t → s ⊆ t :=
+  fun h₁ _ h₂ => by rw [← h₁] ; exact h₂
+
+theorem Subset.antisymm_iff {α : Type _} {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a :=
+  ⟨fun e => ⟨tmp e, tmp e.symm⟩, fun ⟨h₁, h₂⟩ => Set.ext fun _ => ⟨@h₁ _, @h₂ _⟩⟩
+
+@[simp]
+theorem empty_subset {α : Type _} (s : Set α) : ∅ ⊆ s :=
+  fun.
+
+Statement subset_empty_iff
+"Die einzige Teilmenge der leeren Menge ist die leere Menge."
+    {A : Type _} (s : Set A) :
+    s ⊆ ∅ ↔ s = ∅ := by
+  constructor
+  intro h
+  rw [Subset.antisymm_iff]
+  constructor
+  assumption
+  simp only [empty_subset]
+  intro a
+  rw [Subset.antisymm_iff] at a
+  rcases a with ⟨h₁, h₂⟩
+  assumption
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
+
+end MySet
@@ -0,0 +1,52 @@
+import TestGame.Metadata
+import TestGame.Levels.SetTheory.L04_SubsetEmpty
+
+--import Mathlib.Data.Set.Basic
+import Mathlib.Init.Set
+import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.PushNeg
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 5
+
+Title "Nonempty"
+
+Introduction
+"
+Das Gegenteil von `A = ∅` ist `A ≠ ∅`, aber in Lean wird der Ausdruck `A.Nonempty` bevorzugt.
+Dieser ist dadurch existiert, dass in `A` ein Element existiert: `∃x, x ∈ A`.
+
+Zeige dass die beiden Ausdrücke äquivalent sind:
+"
+
+namespace MySet
+
+open Set
+
+theorem subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by
+  constructor
+  intro h
+  rw [Subset.antisymm_iff]
+  constructor
+  assumption
+  simp only [empty_subset]
+  intro a
+  rw [Subset.antisymm_iff] at a
+  rcases a with ⟨h₁, h₂⟩
+  assumption
+
+Statement eq_empty_iff_forall_not_mem
+""
+    {A : Type _} (s : Set A) :
+    s = ∅ ↔ ∀ x, x ∉ s := by
+  rw [←subset_empty_iff]
+  rfl -- This is quite a miracle :)
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
+
+end MySet
@@ -0,0 +1,35 @@
+import TestGame.Metadata
+import TestGame.Levels.SetTheory.L05_Empty
+
+import Mathlib.Data.Set.Basic
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 6
+
+Title "Nonempty"
+
+Introduction
+"
+Das Gegenteil von `A = ∅` ist `A ≠ ∅`, aber in Lean wird der Ausdruck `A.Nonempty` bevorzugt.
+Dieser ist dadurch existiert, dass in `A` ein Element existiert: `∃x, x ∈ A`.
+
+Zeige dass die beiden Ausdrücke äquivalent sind:
+"
+
+open Set
+
+Statement nonempty_iff_ne_empty
+""
+    {A : Type _} (s : Set A) :
+    s.Nonempty ↔ s ≠ ∅ := by
+  rw [Set.Nonempty]
+  rw [ne_eq, eq_empty_iff_forall_not_mem]
+  push_neg
+  rfl
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,31 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 7
+
+Title "Schnittmenge und Vereinigung"
+
+Introduction
+"
+Die klassischen Mengenoperationen sind
+Schnittmenge `∩` (`\\inter`), Vereinigung `∪` (`\\union`) und
+Differenz `\\` (`\\\\`).
+
+Die Taktik `simp` kann triviale Aussagen with Vereinigung mit der
+leeren Menge vereinfachen.
+"
+
+open Set
+
+Statement
+"" (A B : Set ℕ) : (A ∪ ∅) ∩ B = A ∩ (univ ∩ B) := by
+  simp
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,35 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 8
+
+Title "Schnittmenge und Vereinigung"
+
+Introduction
+"
+Ansonsten gibt es jegliche Lemmas in
+
+`import Mathlib.Data.Set.Basic`
+
+die beim Umgang mit diesen Operationen weiterhelfen. Schaue in der Bibliothek auf
+der Seite nach Lemmas, die dir hier weiterhelfen!
+"
+
+open Set
+
+Statement
+""
+    (A B : Set ℕ) : univ \ (A ∩ B) = (univ \ A) ∪ (univ \ B) ∪ (A \ B) := by
+  rw [diff_inter]
+  rw [union_assoc]
+  rw [←union_diff_distrib]
+  rw [univ_union]
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,35 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+
+Game "TestGame"
+World "SetTheory"
+Level 9
+
+Title "Komplement"
+
+Introduction
+"
+Das Komplement einer Menge wird als `Aᶜ` (`\\^c`) geschrieben. Wichtige Lemmas
+sind `not_mem_compl_iff` und `compl_eq_univ_diff`.
+"
+
+open Set
+
+#check not_mem_compl_iff
+#check compl_eq_univ_diff
+
+Statement
+""
+    (A : Set ℕ) (h : Aᶜ ⊆ A) : A = univ := by
+  apply Subset.antisymm
+  simp only [subset_univ]
+  intros x hx
+  by_cases h4 : x ∈ Aᶜ
+  exact mem_of_subset_of_mem h h4
+  rw [←not_mem_compl_iff]
+  exact h4
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,58 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+
+Game "TestGame"
+World "SetTheory"
+Level 10
+
+Title "Morgansche Regeln"
+
+Introduction
+"
+Die De-Morgan'schen Regeln sagen `(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ`
+und `(A ∩ B)ᶜ = Aᶜ ∪ Bᶜ` sind in Lean als
+
+`compl_union` und `compl_inter`.
+
+
+Zudem gibt es die Lemmas `mem_compl_iff : x ∈ Aᶜ ↔ x ∉ A` und
+`not_mem_compl_iff`, mit welchen
+man die de-Morganschen Regeln einfach selber beweisen könnten.
+
+
+Die meisten Aufgaben über Mengen sind eine Kombination von `rw` und `simp_rw` verschiedenster
+Lemmas in `import Mathlib.Data.Set`.
+
+Die Taktik `simp_rw` funktioniert ähnlich wie `rw`, aber sie versucht jedes Lemma so oft
+wie möglich anzuwenden. Wir kennen also 4 etwas verwandte Optionen um Lemmas und Theoreme zu
+brauchen:
+
+- `rw [lemma_A, lemma_B]`: führt jedes Lemma genau einmal aus in der Reihenfolge.
+- `simp_rw [lemma_A, lemma_B]` : führt jedes Lemma in Reihenfolge so oft aus wie möglich.
+- `simp only [lemma_A, lemma_B]` : sucht eine Kombination der beiden Lemmas, ohne bestimmte
+                                   Reihenfolge.
+- `simp [lemma_A, lemma_B]` : Braucht die beiden Lemmas und alle simp-Lemmas.
+"
+
+open Set
+
+#check compl_union
+#check compl_inter
+#check mem_compl_iff
+
+Statement
+""
+    (A B C : Set ℕ) : (A \ B)ᶜ ∩ (C \ B)ᶜ = ((univ \ A) \ C) ∪ (univ \ Bᶜ) := by
+  rw [←compl_union]
+  rw [←union_diff_distrib]
+  rw [diff_diff]
+  simp_rw [←compl_eq_univ_diff]
+  rw [←compl_inter]
+  rw [diff_eq_compl_inter]
+  rw [inter_comm]
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+-- TODOs
+-- Lemmas compl_union compl_inter mem_compl_iff
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Mathlib.Data.Set.Basic
+
+Game "TestGame"
+World "SetTheory"
+Level 11
+
+Title "Strikte Teilmenge"
+
+Introduction
+"
+Strikte Teilmengen sind in Lean eher selten, aber wir schauen sie hier
+trotzdem kurz an : `A ⊂ B` (`\\ssub`) bedeutet `(A ⊆ B) ∧ (¬B ⊆ A)`.
+Entsprechend, kann man die gleichen Methoden wie beim UND benützen
+(`rcases`/`constructor`).
+
+Zudem kann man mit `rw [ssubset_def]` explizit die Definition einsetzen.
+
+Note: `rw [subset_def]` macht das gleiche für `⊆`.
+"
+
+--open Set
+
+Statement
+""
+    (A B : Set ℕ) (h : A ⊂ B) : ∃ x, x ∈ B \ A := by
+  cases' h with h₁ h₂
+  rw [Set.subset_def] at h₂
+  rw [not_forall] at h₂
+  cases' h₂ with x hx
+  use x
+  rw [not_imp] at hx
+  rw [Set.mem_diff]
+  exact hx
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,37 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+
+Game "TestGame"
+World "SetTheory"
+Level 12
+
+Title "Konkrete Mengen"
+
+Introduction
+"
+Nun schauen wir uns konkrete Mengen an. Man schreibt diese mit
+geschweiften Klammern: `{0, 4, 117, 3}`. Meistens muss man
+den Typ explizit angeben, weil lein nicht weiss, ob man mit `Set` (Mengen)
+oder `Finset` (endliche Mengen) arbeiten möchte: `({4, 9} : Set ℕ)`.
+
+`Finset` schauen wir uns später an.
+
+Um mit expliziten Mengen zu arbeiten, ist die Implementationsweise wichtig.
+
+Intern ist eine Menge `{0, 9, 5, 2}` iterativ als Vereinigung von
+Singletons definiert: `{0} ∪ ( {9} ∪ ( {5} ∪ {2} ))`.
+
+Die folgende Aufgabe ist entsprechend mit `rfl` lösbar.
+"
+
+open Set
+
+Statement
+"Die Menge $\\{4, 9\\}}$ ist per Definition \\{4}\\cup\\{9\\}." :
+    ({4, 9} : Set ℕ) = Set.insert 4 {9} := by
+  rfl
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,39 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+
+Game "TestGame"
+World "SetTheory"
+Level 13
+
+Title "Konkrete Mengen"
+
+Introduction
+"
+Um zu überprüfen, dass gewisse Elemente in
+konkreten Mengen enthalten sind, gibt es nicht direkt eine Taktik, aber ein
+einfaches Rezept:
+
+```
+simp_rw [mem_insert_iff, mem_singleton_iff] at *
+```
+
+vereinfacht Aussagen der Form `6 ∈ { 0, 6, 1}` zu `(6 = 0) ∨ (6 = 6) ∨ (6 = 1)`,
+und dann kann `tauto` diese Aussage beweisen.
+
+Bei `⊆` kann man wie schon vorher zuerst mit `intro x hx` die Definition
+auseinandernehmen und dann gleich vorgehen.
+
+"
+
+open Set
+
+Statement
+"" :
+    ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by
+  intro x hx
+  simp_rw [mem_insert_iff, mem_singleton_iff] at *
+  tauto
+
+Tactics simp_rw intro tauto rw
+--Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,37 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "SetTheory2"
+Level 1
+
+Title "Mengen mit Konditionen"
+
+Introduction
+"
+Eine wichtige mathematische Notation ist Teilmengen zu erstellen,
+die gewissen Bedingungen unterliegen.
+
+`{n : ℕ | Odd n}` ist die Menge aller natürlichen Zahlen, die ungerade sind.
+Diese Konstruktion hat in Lean den Namen `setOf`
+
+Um zu beweisen, dass ein Element in einer Teilmenge mit Bedingungen ist, braucht
+man `rw [mem_setOf]`. Danach muss man zeigen, dass die Bedinung für
+dieses Element erfüllt ist.
+"
+
+open Set
+
+Statement
+"" :
+    3 ∈ {n : ℕ | Odd n}  := by
+  rw [mem_setOf]
+  use 1
+  ring
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,42 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "SetTheory2"
+Level 2
+
+Title "Potenzmenge"
+
+Introduction
+"
+Eine andere wichtige Menge ist die Potenzmenge einer Menge, welche als
+`𝒫 A` geschrieben wird (`\\powerset`). Diese ist als `{S | S ⊆ A}` definiert, also
+alle Mengen, die in $A$ enthalten sind.
+
+Eines der wichtigsten Lemmas ist `mem_powerset_iff: x ∈ 𝒫 s ↔ x ⊆ s` welches
+im Grunde die Definition einsetzt.
+"
+
+open Set
+
+Statement
+"" (X Y : Set ℕ):
+    𝒫 X ∪ 𝒫 Y ⊆ 𝒫 (X ∪ Y)  := by
+  intro A hA
+  rw [mem_union] at hA
+  simp_rw [mem_powerset_iff] at *
+  rcases hA with hA | hA
+  apply subset_union_of_subset_left
+  assumption
+  apply subset_union_of_subset_right
+  assumption
+
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,41 @@
+import TestGame.Metadata
+
+import Mathlib
+import Mathlib.Algebra.Parity
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "SetTheory2"
+Level 3
+
+Title ""
+
+Introduction
+"
+Um anzunehmen, dass zwei Mengen disjunkt sind schreibt man
+`Disjoint S T`, welches dadurch definiert ist das die
+einzige gemeinsame Teilmenge die leere Menge ist,
+also etwa `A ⊆ S → A ⊆ T → A ⊆ ∅`.
+
+Beachte, dass `Disjoint` in Lean genereller definiert ist als
+für Mengen, deshalb siehst du die Symbole
+`≤` anstatt `⊆` und `⊥` anstatt `∅`, aber diese bedeuten genau
+das gleiche.
+"
+
+open Set
+
+Statement
+"" :
+    ¬Disjoint ({n : ℤ | ∃ k, n = 2 * k} : Set ℤ) ({3, 5, 6, 9, 11} : Set ℤ) := by
+  unfold Disjoint
+  rw [not_forall] -- why not `push_neg`?
+  use {6}
+  simp
+  use 3
+  ring
+
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,39 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib
+
+Game "TestGame"
+World "SetTheory2"
+Level 4
+
+Title ""
+
+Introduction
+"
+"
+
+open Set
+
+Statement
+"" :
+    {2, 7} ⊆ {n : ℕ | n = 2 ∨ (n ≤ 10 ∧ Odd n)}  := by
+  rw [setOf_or, setOf_and]
+  intro x hx
+  rw [mem_union, mem_inter_iff]
+  simp_rw [mem_setOf, mem_insert_iff, mem_singleton_iff] at *
+  rcases hx with hx | hx
+  left
+  assumption
+  right
+  constructor
+  linarith
+  use 3
+  rw [hx]
+  ring
+
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,33 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib
+
+Game "TestGame"
+World "SetTheory2"
+Level 5
+
+Title ""
+
+Introduction
+"
+Zu der Teilmengen-Schreibweise (`SetOf`) gibt es noch zwei spezielle
+Syntax, die abundzu auftreten.
+
+Der erste ist `{ x ∈ S | 0 ≤ x}` ( für z.B `(S : Set ℤ)`),
+welcher eine Abkürzung für `{ x : ℤ | x ∈ S ∧ 0 ≤ x}` ist.
+Entsprechend hilft auch hier `setOf_and`.
+
+"
+
+open Set
+
+Statement
+"" (S : Set ℤ) :
+    { x ∈ (S : Set ℤ) | 0 ≤ x} ⊆ S := by
+  library_search
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "SetTheory2"
+Level 6
+
+Title ""
+
+Introduction
+"
+"
+
+open Set
+
+Statement
+"" :
+    3 ∈ {n : ℕ | Odd n}  := by
+  rw [mem_setOf]
+  use 1
+  ring
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,27 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib
+
+Game "TestGame"
+World "SetTheory2"
+Level 7
+
+Title ""
+
+Introduction
+"
+Wir haben bereits `∪` und `∩` kennengelernt. Von beiden gibt es auch eine Version für Familien
+von Mengen: $\\bigcup_i A_ i$ und $\\bigcap_j B_ j$.
+
+"
+
+open Set
+
+Statement
+"" : True := sorry
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Set.Basic
+import Mathlib.Algebra.Parity
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "SetTheory"
+Level 21
+
+Title ""
+
+Introduction
+"
+"
+
+open Set
+
+Statement
+"" :
+    3 ∈ {n : ℕ | Odd n}  := by
+  rw [mem_setOf]
+  use 1
+  ring
+
+Tactics constructor intro rw assumption rcases simp tauto trivial
+
+Lemmas Subset.antisymm_iff empty_subset
@@ -0,0 +1,109 @@
+import Mathlib
+
+open Set
+
+namespace Finset
+
+theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) :
+    Finset.powerset {x} = {∅, {x}} := by
+  ext y
+  rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton]
+
+end Finset
+
+/- The powerset of a singleton contains only `∅` and the singleton. -/
+theorem powerset_singleton {U : Type _} (x : U) :
+    𝒫 ({x} : Set U) = {∅, {x}} := by
+  ext y
+  rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]
+
+theorem subset_insert_iff_of_not_mem {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s)
+    : s ⊆ insert a t ↔ s ⊆ t := by
+  constructor
+  · intro g y hy
+    specialize g hy
+    rw [mem_insert_iff] at g
+    rcases g with g | g
+    · rw [g] at hy
+      contradiction
+    · assumption
+  · intro g y hy
+    specialize g hy
+    exact mem_insert_of_mem _ g
+
+theorem subset_insert_iff_of_not_mem' {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s)
+    (g : s ⊆ t) : s ⊆ insert a t := by
+  intro y hy
+  specialize g hy
+  exact mem_insert_of_mem _ g
+
+lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) :
+    S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by
+  simp_rw [mem_powerset_iff]
+  constructor
+  · intro h
+    by_cases hs : x ∈ S
+    · right
+      use S \ {x}
+      rw [insert_diff_singleton, insert_eq_of_mem hs, diff_singleton_subset_iff]
+      exact ⟨h, rfl⟩
+    · left
+      exact (subset_insert_iff_of_not_mem hs).mp h
+  · intro h
+    rcases h with h | ⟨B, h₁, h₂⟩
+    · exact le_trans h (subset_insert x A)
+    · rw [←h₂]
+      exact insert_subset_insert h₁
+
+lemma mem_powerset_insert_iff' {U : Type _} (A S : Set U) (x : U) :
+    S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by
+  rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff]
+
+lemma powerset_insert {U : Type _} (A : Set U) (x : U) :
+    𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by
+  ext y
+  rw [mem_powerset_insert_iff, mem_union, mem_image]
+
+
+
+
+
+example : ({0} : Set ℕ) ∪ {1, 2} = {0, 2, 1} := by
+  rw [union_insert, singleton_union]
+  simp only [insert_comm, ←insert_emptyc_eq]
+
+example : powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by
+  simp_rw [powerset_insert, powerset_singleton]
+  simp only [image_insert_eq, union_insert, image_singleton, union_singleton]
+  simp only [insert_comm, ←insert_emptyc_eq]
+
+-- This one is much slower, but it still works
+example : powerset {0, 1, 2, 4} =
+    {∅, {0}, {1}, {0, 1}, {2}, {1, 2}, {0, 2}, {0, 1, 2},
+    {4}, {0, 4}, {1, 4}, {0, 1, 4}, {2, 4}, {1, 2, 4}, {0, 2, 4}, {0, 1, 2, 4}} := by
+  simp_rw [powerset_insert, powerset_singleton]
+  simp only [image_insert_eq, union_insert, image_singleton, union_singleton]
+  simp only [insert_comm, ←insert_emptyc_eq]
+
+example : ({∅, {0}, {1}, {0, 1}} : Finset (Finset ℕ)) = {∅, {1}, {0}, {0, 1}} := by
+  simp only []
+
+example : ({{0, 2}, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}} := by
+  rw [Subset.antisymm_iff]
+  constructor <;>
+  intro A hA <;>
+  simp_rw [mem_insert_iff, mem_singleton_iff] at *
+  · rw [pair_comm 2 0, insert_comm 5 3]
+    tauto
+  · rw [pair_comm 0 2, insert_comm 3 5]
+    tauto
+
+-- A trick to compare two concrete sets.
+example (A : Set ℕ) : ({{0, 2}, A, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}, A} := by
+  simp only [insert_comm, ←insert_emptyc_eq]
+
+example : ({{0, 2}, {3, 5, 6}} : Finset (Finset ℕ)) = {{2, 0}, {5, 3, 6}} := by
+  simp only
+
+-- Trick:
+-- attribute [default_instance] Set.instSingletonSet
@@ -1,5 +1,15 @@
 import TestGame.Metadata

+import Mathlib.Order.SymmDiff
+import Mathlib.Logic.Function.Iterate
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.SolveByElim
+import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.ByContra
+import Mathlib.Tactic.Lift
+import Mathlib.Data.Set.Basic
+import Mathlib.Data.Finset.Powerset
+import Mathlib.Tactic.LibrarySearch
 import Mathlib

 set_option tactic.hygienic false
@@ -45,3 +55,243 @@ Statement
  rw [Set.univ_union]

 Tactics rw
+
+
+example : 4 ∈ (univ : Set ℕ) := by
+  trivial
+
+example (A : Set ℕ) : 4 ∉ (∅ : Set ℕ) := by
+  trivial
+
+example (A : Set ℕ) : A ⊆ univ := by
+  intro x h
+  trivial
+
+-- -- subset_empty_iff
+-- example {s : Set α} : s ⊆ ∅ ↔ s = ∅ := by
+--   constructor
+--   intro h
+--   rw [Subset.antisymm_iff]
+--   constructor
+--   assumption
+--   simp only [empty_subset]
+--   intro a
+--   rw [Subset.antisymm_iff] at a
+--   rcases a with ⟨h₁, h₂⟩
+--   assumption
+
+-- -- eq_empty_iff_forall_not_mem
+-- example {s : Set α} : s = ∅ ↔ ∀ x, x ∉ s := by
+--   rw [←subset_empty_iff]
+--   rfl
+
+-- -- nonempty_iff_ne_empty
+-- example (X : Type _) (s : Set X) : Set.Nonempty s ↔ s ≠ ∅ := by
+--   rw [Set.Nonempty]
+--   rw [ne_eq, eq_empty_iff_forall_not_mem]
+--   push_neg
+--   rfl
+
+
+-- example (A B : ℝ): A = B ↔ A ≤ B ∧ B ≤ A := by library_search
+
+namespace Finset
+
+theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) :
+    Finset.powerset {x} = {∅, {x}} := by
+  ext y
+  rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton]
+
+end Finset
+
+/- The powerset of a singleton contains only `∅` and the singleton. -/
+theorem powerset_singleton {U : Type _} (x : U) :
+    𝒫 ({x} : Set U) = {∅, {x}} := by
+  ext y
+  rw [mem_powerset_iff, subset_singleton_iff_eq]
+  rw [mem_insert_iff, mem_singleton_iff]
+
+
+lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) :
+    S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by
+  rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff]
+
+-- lemma powerset_insert {U : Type _} (A : Set U) (x : U) :
+--     𝒫 (insert x A) = 𝒫 A ∪ ({B : Set U | B \ {x} ∈ 𝒫 A}) := by
+--   sorry
+
+theorem subset_insert_iff_of_not_mem {U : Type _ }{s t : Set U} (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t := by
+  rw [subset_insert_iff, erase_eq_of_not_mem h]
+
+lemma mem_powerset_insert_iff₂ {U : Type _} (A S : Set U) (x : U) :
+    S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by
+  simp_rw [mem_powerset_iff]
+  constructor
+  · intro h
+    by_cases hs : x ∈ S
+    · sorry
+    · left
+      rw [Finset.subset_insert_iff_of_not_mem]
+  · intro h
+    rcases h with h | ⟨B, h₁, h₂⟩
+    · exact le_trans h (subset_insert x A)
+    · rw [←h₂]
+      exact insert_subset_insert h₁
+
+lemma powerset_insert {U : Type _} (A : Set U) (x : U) :
+    𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by
+  rw [Subset.antisymm_iff]
+  constructor <;>
+  intro B hB <;>
+  simp_rw [mem_powerset_insert_iff₂, mem_union, mem_image] at hB ⊢ <;>
+  assumption
+
+
+example : powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by
+  simp_rw [powerset_insert, powerset_singleton, Finset.powerset_insert, Finset.powerset_singleton]
+  simp only [image_insert_eq, union_insert, image_singleton, union_singleton]
+  simp only [insert_comm, ←insert_emptyc_eq]
+
+example [DecidableEq ℕ] : Finset.powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by
+  repeat' rw [@ Finset.powerset_insert ℕ]
+  repeat' rw [@Finset.powerset_singleton ℕ]
+  --simp only [image_insert_eq, union_insert, image_singleton, union_singleton]
+
+
+example : powerset {0, 1, 2, 4} =
+    {∅, {0}, {1}, {0, 1}, {2}, {1, 2}, {0, 2}, {0, 1, 2},
+    {4}, {0, 4}, {1, 4}, {0, 1, 4}, {2, 4}, {1, 2, 4}, {0, 2, 4}, {0, 1, 2, 4}} := by
+  simp_rw [powerset_insert, powerset_singleton]
+  simp_rw [image_insert_eq, image_singleton]
+
+
+
+example : Finset.powerset ({0, 1} : Finset ℕ) = {{0, 1}, ∅, {1}, {0}} := by
+  have h : Finset.powerset ({0, 1} : Finset ℕ) = {∅, {0}, {1}, {0, 1}}
+  rfl
+  rw [h]
+  simp only []
+
+
+example : ({∅, {0}, {1}, {0, 1}} : Finset (Finset ℕ)) = {∅, {1}, {0}, {0, 1}} := by
+  simp only []
+
+
+
+lemma subset_of_subset_diff {U : Type _} (A B C : Set U) (h : A ⊆ B \ C) : A ⊆ B :=
+  fun _ hx => mem_of_mem_diff (h hx)
+
+lemma subset_of_subset_diff' {U : Type _} (A B C : Set U) (h : A ⊆ B) : A \ C ⊆ B :=
+  sorry
+
+lemma mem_powerset' {U : Type _} {A B C : Set U}
+    (h' : B ∈ 𝒫 C) (h : A ⊆ B) :
+    A ∈ 𝒫 C := by
+  rw [mem_powerset_iff] at h' ⊢
+  exact le_trans h h'
+
+example (A B : Set ℕ) : A = B ↔ ∀ x, x ∈ A ↔ x ∈ B := by
+  exact ext_iff
+
+
+
+lemma NO.powerset_insert {U : Type _} (A : Set U) (x : U) :
+    𝒫 (insert x A) = 𝒫 A ∪ ({insert x B | B ∈ 𝒫 A}) := by
+  ext y
+  rw [mem_powerset_insert_iff]
+  constructor
+  · intro h
+    rw [mem_union, mem_setOf]
+    by_cases hx : x ∈ y
+    · right
+      use y \ {x}
+      constructor
+      · assumption
+      · rw [insert_diff_singleton, insert_eq_of_mem hx]
+    · left
+      rw [diff_singleton_eq_self hx] at h
+      assumption
+  · intro h
+    rw [mem_union, mem_setOf] at h
+    rcases h with h | h
+    · apply mem_powerset' h
+      simp
+    · rcases h with ⟨B, hB⟩
+      rw [←hB.2]
+      apply mem_powerset' hB.1
+      simp
+
+-- lemma xxx {U : Type _} (x y : U):
+--     ({insert x B | B ∈ {∅, }}) = {({x} : Set U), {x, y}} := by
+--   sorry
+
+-- lemma hh {U : Type _} (A : Set U) (x : U) :
+--     A \ {x} ∈
+
+lemma diff_singleton_eq_iff {U : Type _} {A B : Set U} {x : U} :
+    A \ {x} = B ↔ A = B ∨ A = insert x B := by sorry
+
+lemma x1 {U : Type _} (x : U) : insert x (∅ : Set U) = {x} := by sorry
+
+--set_option maxHeartbeats 20000
+
+
+example {U : Type _} {x y : U} : ({x, y} : Set U) = {y, x} := by
+  exact pair_comm x y
+
+example {U : Type _} {A : Set U} {x y : U} : insert x (insert y A) = insert y (insert x A) := by
+  exact insert_comm x y A
+
+open Classical
+
+#check decide
+
+example : ({{0, 2}, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}} := by
+  rw [Subset.antisymm_iff]
+  constructor <;>
+  intro A hA <;>
+  simp_rw [mem_insert_iff, mem_singleton_iff] at *
+  · rw [pair_comm 2 0, insert_comm 5 3]
+    tauto
+  · rw [pair_comm 0 2, insert_comm 3 5]
+    tauto
+
+example (A : Set ℕ) : ({{0, 2}, A, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}, A} := by
+  simp only [insert_comm, ←insert_emptyc_eq]
+
+
+example : ({{0, 2}, {3, 5, 6}} : Finset (Finset ℕ)) = {{2, 0}, {5, 3, 6}} := by
+  simp only
+
+
+  -- -- This works but does not scale well
+  -- ext x
+  -- simp_rw [powerset_insert, powerset_singleton]
+  -- simp_rw [mem_union, mem_setOf, mem_insert_iff, mem_singleton_iff]
+  -- simp_rw [diff_singleton_eq_iff, x1]
+  -- tauto
+
+
+
+
+  -- rw [Subset.antisymm_iff]
+  -- constructor
+  -- intro A hA
+  -- rw [mem_powerset_iff] at hA
+  -- simp_rw [mem_insert_iff, mem_singleton_iff] at *
+
+
+example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by
+  intro a ha
+  simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at *
+  tauto
+
+example : ({0} : Set ℕ) ∪ {1, 2} = {0, 2, 1} := by
+  rw [Subset.antisymm_iff]
+  intro A hA
+  --rw [Set.mem_insert_iff]
+
+
+
+-- Trick:
+-- attribute [default_instance] Set.instSingletonSet
@@ -0,0 +1,96 @@
+import TestGame.Metadata
+
+import Mathlib
+import Duper.Tactic
+
+
+import Mathlib.Order.Disjoint
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 4
+
+Title "Mengen"
+
+Introduction
+"
+`∈ ∉ ⊆ ⊂ ⋃ ⋂`
+"
+
+open Set
+
+-- open_locale cardinal
+
+variables {X : Type _} (x : X) (A B : Set X)
+
+#check A.Nonempty
+#check Nonempty A
+#check insert x A -- {x} ∪ A
+-- #check disjoint A B -- needs Mathlib.Order.Disjoint
+#check A ∆ B
+#check Nontrivial A
+
+#check ({2} : Set ℕ)
+
+example : ({2} : Set ℕ) ⊆ {4, 2, 3} := by
+  simp only [mem_singleton_iff, mem_insert_iff, or_self, singleton_subset_iff, or_false, or_true]
+
+example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by
+  intro n hn
+  simp only [mem_insert_iff, mem_singleton_iff] at *
+  tauto
+
+example : {2, 3, 5} ⊆ (univ : Set ℕ) := by
+  tauto
+
+example : 3 ∈ ({4, 2, 5, 7, 3} : Set ℕ) := by
+  tauto
+
+example : ({4, 9} : Set ℕ) = Set.insert 4 {9} := by
+  rfl
+
+
+
+
+#check Finset.card
+
+variable (A : Finset ℕ)
+
+#check A.card
+
+-- card_union_eq
+example (A B : Finset ℕ) (h : Disjoint A B) : (A ∪ B).card = A.card + B.card := by
+  -- Not a suitable proof for the course.
+  rw [← Finset.disjUnion_eq_union A B h, Finset.card_disjUnion _ _ _]
+
+example : ¬Disjoint {n : ℤ | ∃ k, n = 2 * k} {3, 5, 6, 9, 11} := by
+  rw [not_disjoint_iff]
+  use 6
+  constructor
+  rw [mem_setOf_eq]
+  use 3
+  tauto
+
+example : {n : ℕ | Even n ∨ Odd n} = univ := by
+  rw [setOf_or]
+
+
+
+
+#check Set.eq_of_mem_singleton
+#check {n : ℤ | ∃ k, n = 2 * k}
+#check {n : ℤ // ∃ k, n = 2 * k}
+#check ℤ
+variables (C : Set ℤ)
+#check {n ∈ C | ∃ (k : ℤ), n = 2 * k}
+#check {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k}
+#check {x ∈ A | x = x}
+#check {y | y ∈ A}
+#check setOf_and
+#check setOf_or
+#check Disjoint C univ
+
+example : {n ∈ C | ∃ (k : ℤ), n = 2 * k} = {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} := by
+  rfl