levels

2023-03-01 11:56:01 +01:00
parent aca781879a
commit 0ebf890392
21 changed files with 471 additions and 198 deletions
@@ -5,7 +5,7 @@ import TestGame.Levels.Implication
 import TestGame.Levels.Predicate
 import TestGame.Levels.Contradiction
 import TestGame.Levels.Prime
-import TestGame.Levels.Induction
+import TestGame.Levels.Sum

 import TestGame.Levels.Numbers
 import TestGame.Levels.Inequality
@@ -48,6 +48,6 @@ Path SetTheory2 → Numbers

 Path Module → Basis → Module2

-Path Contradiction → Inequality → Induction → LeanStuff → Function → SetFunction
+Path Contradiction → Inequality → Sum → LeanStuff → Function → SetFunction

 MakeGame
@@ -113,3 +113,27 @@ Even Odd not_odd not_even

 LemmaSet logic : "Logik" :=
 not_not not_forall not_exists
+
+LemmaDoc Finset.sum_add_distrib as Finset.sum_add_distrib in "Sum"
+""
+
+LemmaDoc Fin.sum_univ_castSucc as Fin.sum_univ_castSucc in "Sum"
+""
+
+LemmaDoc Nat.succ_eq_add_one as Nat.succ_eq_add_one in "Sum"
+""
+
+LemmaDoc add_comm as add_comm in "Nat"
+""
+
+LemmaDoc mul_add as mul_add in "Nat"
+""
+
+LemmaDoc add_mul as add_mul in "Nat"
+""
+
+LemmaDoc arithmetic_sum as arithmetic_sum in "Sum"
+""
+
+LemmaDoc add_pow_two as add_pow_two in "Nat"
+""
@@ -1,10 +0,0 @@
-import TestGame.Levels.Induction.L01_Simp
-import TestGame.Levels.Induction.L02_Sum
-import TestGame.Levels.Induction.L03_Induction
-import TestGame.Levels.Induction.L04_SumOdd
-import TestGame.Levels.Induction.L05_Sum
-import TestGame.Levels.Induction.L06_SumComm
-
-Game "TestGame"
-World "Induction"
-Title "Induktion"
@@ -1,37 +0,0 @@
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
-import TestGame.Metadata
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Induction"
-Level 2
-
-Title "endliche Summe"
-
-Introduction
-"
-Jetzt wollen wir ein paar Lemmas zu Summen kennenlernen, die `simp` nicht automatisch
-verwendet.
-
-Als erstes, kann man eine endliche Summe $\\sum_{i = 0}^n a_i + b_i$ mit
-`rw [Finset.sum_add_distrib]` als zwei Summen $\\sum_{i = 0}^n a_i + \\sum_{j = 0}^n b_j$
-auseinandernehmen.
-
-Insbesondere ist auch zu beachten, dass der Index `i` keine natürliche Zahl ist, sondern
-vom Typ `Fin n`, das heisst, man muss diesen eigentlich immer mit `(i : ℕ)`
-als natürliche Zahl verwenden.
-"
-
-open BigOperators
-
-Statement
-"Zeige dass $\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$."
-    (n : ℕ) : ∑ i : Fin n, ((i : ℕ) + 1) = n + (∑ i : Fin n, (i : ℕ)) := by
-  rw [Finset.sum_add_distrib]
-  simp
-  ring
-
-NewTactics rw simp ring
@@ -1,45 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Ring
-import Mathlib
-
-
-Game "TestGame"
-World "Induction"
-Level 3
-
-Title "Induktion"
-
-Introduction
-"
-Induktion ist eine wichtige Beweismethode, nicht zuletzt auch wenn es um endliche Summen geht.
-
-Die Taktik `induction' n with n n_ih` teilt das Goal in zwei Goals auf:
-
-1. Induktionsanfang, wo `n` durch `0` ersetzt wird.
-2. Induktionsschritt, wo `n` durch `n.succ` (also `(n + 1)`) ersetzt wird und man die
-   Induktionshypothese als Annahme `n_ih` kriegt.
-
-Für den Induktionsschritt braucht man fast immer zwei technische Lemmas:
-
- `Fin.sum_univ_castSucc` um $\\sum_{i=0}^{n} a_i$ als
-  $\\sum_{i=0}^{n-1} a_i + a_n$ umzuschreiben.
- `nat_succ` um `n.succ` zu `n + 1` umzuschreiben.
-"
-
-- Note: I don't want to deal with Nat-division, so I stated it as `2 * ... = ...` instead.
-
-open BigOperators
-
-Statement arithmetic_sum
-"Zeige $\\sum_{i = 0}^n i = \\frac{n \\cdot (n + 1)}{2}$."
-  (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
-  induction' n with n hn
-  simp
-  rw [Fin.sum_univ_castSucc]
-  rw [mul_add]
-  simp
-  rw [mul_add, hn]
-  simp_rw [Nat.succ_eq_one_add]
-  ring
-
-NewTactics ring
@@ -1,30 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Ring
-import Mathlib
-
-Game "TestGame"
-World "Induction"
-Level 4
-
-Title "Bernoulli Ungleichung"
-
-Introduction
-"
-Hier nochmals eine Übung zur Induktion.
-"
-
-open BigOperators
-
-Statement
-"Zeige folgende Gleichung zur Summe aller ungeraden Zahlen:
-
-$\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
-    (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 := by
-  induction' n with n hn
-  simp
-  rw [Fin.sum_univ_castSucc]
-  simp
-  rw [hn, Nat.succ_eq_add_one]
-  ring
-
-NewTactics ring
@@ -1,47 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Ring
-import Mathlib
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Induction"
-Level 5
-
-Title "Induktion"
-
-Introduction
-"
-"
-
-open BigOperators
-
-lemma arithmetic_sum (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
-  induction' n with n hn
-  simp
-  rw [Fin.sum_univ_castSucc]
-  rw [mul_add]
-  simp
-  rw [mul_add, hn]
-  simp_rw [Nat.succ_eq_one_add]
-  ring
-
-
-Statement
-"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i)^2$."
-  (n : ℕ) : (∑ i : Fin (n + 1), (i : ℕ)^3) = (∑ i : Fin (n + 1), (i : ℕ))^2 := by
-  induction' n with n hn
-  simp
-  conv_rhs =>
-    rw [Fin.sum_univ_castSucc]
-    simp
-    rw [add_pow_two]
-    rw [arithmetic_sum]
-    rw [mul_assoc, add_assoc, ←pow_two, ←Nat.succ_mul n, Nat.succ_eq_add_one, ←pow_succ]
-  conv_lhs =>
-    rw [Fin.sum_univ_castSucc]
-    simp
-    rw [hn]
-
-
-NewTactics ring
@@ -27,11 +27,10 @@ dann gilt $P(n)$ für alle $n \\in \\mathbb{N}.$"
  apply h_step
  assumption

-- TODO: Why are these not shown.
-HiddenHint (n : ℕ) (P : ℕ → Prop) : P n =>
-"Benutze `induction n`."
+-- HiddenHint (n : ℕ) (P : ℕ → Prop) : P n =>
+-- "Benutze `induction n`."

-Hint (P : ℕ → Prop) : P 0 =>
+Hint (P : ℕ → Prop) : P Nat.zero =>
 "Das ist die Induktionsverankerung, hier musst du $P(0)$ zeigen."

 Hint (P : ℕ → Prop) (m : ℕ) (hi : P m) : P (Nat.succ m) =>
@@ -25,7 +25,7 @@ Wichtige Lemmas über Primzhalen werden mit
 import Data.Nat.Prime
 ```
 importiert (siehe
-[Docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html))
+[Docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html)).

 Insbesondere `Nat.prime_def_lt''` welches die aus der Schule bekannte Definition einer
 Primzahl `Prime p ↔ 2 ≤ p ∧ (∀ m, m ∣ p → m = 1 ∨ m = p)` gibt.
@@ -0,0 +1,10 @@
+import TestGame.Levels.Sum.L01_Simp
+import TestGame.Levels.Sum.L02_Sum
+import TestGame.Levels.Sum.L03_ArithSum
+import TestGame.Levels.Sum.L04_SumOdd
+import TestGame.Levels.Sum.L05_Sum
+import TestGame.Levels.Sum.L06_SumComm
+
+Game "TestGame"
+World "Sum"
+Title "Endliche Summe"
@@ -1,25 +1,24 @@
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
 import TestGame.Metadata

+import TestGame.Options.BigOperators
+
 set_option tactic.hygienic false

 Game "TestGame"
-World "Induction"
+World "Sum"
 Level 1

 Title "Simp"

 Introduction
 "
-In diesem Kapitel lernen wir endliche Summen und Induktion kennen.
+In diesem Kapitel lernen wir endliche Summen und mehr Übungen zur Induktion.

 Eine endliche Summe läuft erstmal immer über einen endlichen Index
 `Fin n`, welcher $n$ Elemente
 $\\{0, 1, \\ldots, n-1\\}$ beinhaltet.

-Der Syntax für  $\\sum_{i=0}^n a_i$ (\\sum) ist `∑ i : Fin n, …`
+Der Syntax für  $\\sum_{i=0}^n a_i$ ist `∑ i : Fin n, _` (\\sum)

 Als erstes kann die Taktik `simp` (für \"simplification\") ganz viel Triviales vereinfachen.
 `simp` ist eine der stärksten Taktiken in Lean und verwendet
@@ -32,12 +31,16 @@ Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
 lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
  sorry
 ```
+
+Die Taktik `simp` benützt alle Lemmas, die mit `@[simp]` markiert sind.
+
+(Tipp: `simp?` zeigt an, welche Lemmas `simp` benutzen würde.)
 "

 open BigOperators

 Statement
-"Zeige dass $\\sum_{i = 0} ^ {n-1} (0 + 0) = 0$."
+"Zeige $\\sum_{i = 0} ^ {n-1} (0 + 0) = 0$."
    (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
  simp

@@ -0,0 +1,46 @@
+import TestGame.Metadata
+
+import TestGame.Options.BigOperators
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Sum"
+Level 2
+
+Title "endliche Summe"
+
+Introduction
+"
+Generell sind aber nur solche Lemmas `@[simp]` markiert, klar eine Vereinfachung darstellen.
+
+So ist ein Lemma wie `Finset.sum_add_distrib` kein `simp`-Lemma, da beide Seiten je
+nach Situation bevorzugt sein könnte:
+
+$$
+  \\sum_{i = 0}^n a_i + b_i = \\sum_{i = 0}^n a_i + \\sum_{j = 0}^n b_j
+$$
+
+Dieses Lemma kann aber mit `rw` angewendet werden.
+"
+
+open BigOperators
+
+Statement
+"Zeige dass $\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$."
+    (n : ℕ) : ∑ i : Fin n, ((i : ℕ) + 1) = n + (∑ i : Fin n, (i : ℕ)) := by
+  rw [Finset.sum_add_distrib]
+  simp
+  ring
+
+NewTactics rw simp ring
+NewLemmas Finset.sum_add_distrib add_comm
+
+Hint (n : ℕ) : ∑ x : Fin n, ↑x + ∑ x : Fin n, 1 = n + ∑ i : Fin n, ↑i =>
+"Die zweite Summe `∑ x : Fin n, 1` kann `simp` zu `n` vereinfacht werden."
+
+Hint (n : ℕ) : ∑ x : Fin n, ↑x + n = n + ∑ x : Fin n, ↑x =>
+"Bis auf Umordnung sind jetzt beide Seiten gleich, darum kann `ring` das Goal schließen.
+
+Alternativ kann man auch mit `rw [add_comm]` dies explizit umordnen."
@@ -0,0 +1,85 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "Sum"
+Level 3
+
+Title "Arithmetische Summe"
+
+Introduction
+"
+Oft beweist man Aussagen über Summen am besten per Induktion.
+
+Eines der wichtigsten Lemmas für den Induktionsschritt ist
+`Fin.sum_univ_castSucc`, welches
+$\\sum_{i=0}^{n} a_i = \\sum_{i=0}^{n-1} a_i + a_n$ umschreibt.
+
+**Bemerkung:**
+
+Eine technische Sonderheit ist der kleine Pfeil `↑` in `∑ i : Fin (n + 1), ↑i`.
+Da `i : Fin n` technisch keine natürliche Zahl ist (sondern vom Typ `Fin n`), muss man
+dieses zuerst mit `↑i` oder `(i : ℕ)` in eine natürliche Zahl umwandeln. Diese nennt man
+*Coersion*.
+
+Gleichermassen, kommen hier im Induktionsschritt die Terme `↑(↑Fin.castSucc.toEmbedding i)`
+und `↑(Fin.last (n + 1))` vor. Diese Terme können mit `simp` vereinfacht werden.
+"
+
+-- Note: I don't want to deal with Nat-division, so I stated it as `2 * ... = ...` instead.
+
+set_option tactic.hygienic false
+
+open BigOperators
+
+Statement arithmetic_sum
+"Zeige $2 \\cdot \\sum_{i = 0}^n i = n \\cdot (n + 1)$."
+    (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
+  induction' n with n hn
+  simp
+  rw [Fin.sum_univ_castSucc]
+  rw [mul_add]
+  simp
+  rw [hn]
+  rw [Nat.succ_eq_add_one]
+  ring
+
+NewTactics ring
+NewLemmas Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul
+
+Hint (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) =>
+"Als Erinnerung, einen Induktionsbeweis startet man mit `induction n`."
+
+Hint (n : ℕ) : 2 * ∑ i : Fin (0 + 1), ↑i = 0 * (0 + 1) =>
+"Den Induktionsanker $n = 0$ kann `simp` oft beweisen."
+
+Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
+  2 * ∑ i : Fin (Nat.succ n + 1), ↑i = Nat.succ n * (Nat.succ n + 1) =>
+"Den Induktionsschritt beginnt man oft mit `rw [Fin.sum_univ_castSucc]`."
+
+-- Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
+--   2 * (∑ i : Fin (n + 1), ↑(Fin.castSucc.toEmbedding i) +
+--   ↑(Fin.last (n + 1))) = Nat.succ n * (Nat.succ n + 1) =>
+-- "Die Taktik `simp` vereinfacht `↑(↑Fin.castSucc.toEmbedding i)`. "
+
+Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
+  2 * (∑ x : Fin (n + 1), ↑x + (n + 1)) = Nat.succ n * (Nat.succ n + 1) =>
+"Um Die Induktionshypothese anzuwenden muss man noch
+$$2 \\cdot ((\\sum_{x=0}^n x) + (n + 1)) = 2 \\cdot \\sum_{x=0}^n x + 2 \\cdot (n + 1))$$
+umschreiben. Dazu kannst du `mul_add` benützen.
+"
+
+Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
+  2 * ∑ x : Fin (n + 1), ↑x + 2 * (n + 1) = Nat.succ n * (Nat.succ n + 1) =>
+"Jetzt kann die Induktionshypothese mit `rw` angewendet werden."
+
+Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
+  n * (n + 1) + 2 * (n + 1) = Nat.succ n * (Nat.succ n + 1) =>
+"
+Im Moment muss man hier `ring` noch helfen,
+indem man mit `rw [Nat.succ_eq_add_one]` zuerst `Nat.succ n = n + 1` umschreibt.
+
+(Dies wird irgendwann noch gefixt)
+"
@@ -0,0 +1,58 @@
+import TestGame.Metadata
+
+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "Sum"
+Level 4
+
+Title "Summe aller ungeraden Zahlen"
+
+Introduction
+"
+Hier nochmals eine Übung zur Induktion.
+"
+set_option tactic.hygienic false
+
+open BigOperators
+
+Statement
+"Zeige folgende Gleichung zur Summe aller ungeraden Zahlen:
+
+$\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
+    (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 := by
+  induction' n with n hn
+  simp
+  rw [Fin.sum_univ_castSucc]
+  simp
+  rw [hn]
+  rw [Nat.succ_eq_add_one]
+  ring
+
+HiddenHint (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 =>
+"
+Fange wieder mit `induction n` an.
+"
+
+HiddenHint (n : ℕ) : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 =>
+"
+Den Induktionsanfang kannst du wieder mit `simp` beweisen.
+"
+
+HiddenHint (n : ℕ) : ∑ i : Fin (Nat.succ n), ((2 : ℕ) * i + 1) = Nat.succ n ^ 2 =>
+"
+Den Induktionsschritt startest du mit `rw [Fin.sum_univ_castSucc]`.
+"
+
+HiddenHint (n : ℕ) (hn : ∑ i : Fin n, (2 * (i : ℕ) + 1) = n ^ 2) :
+  ∑ x : Fin n, (2 * (x : ℕ) + 1) + (2 * n + 1) = Nat.succ n ^ 2 =>
+"
+Hier kommt die Induktionshypothese ins Spiel.
+"
+
+HiddenHint (n : ℕ) : n ^ 2 + (2 * n + 1) = Nat.succ n ^ 2 =>
+"
+Mit `rw [Fin.sum_univ_castSucc]` und `ring` kannst du hier abschliessen.
+"
@@ -0,0 +1,103 @@
+import TestGame.Metadata
+
+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Sum"
+Level 5
+
+set_option tactic.hygienic false
+
+Title "Quadrat der Arithmetischen Summe"
+
+Introduction
+"
+Und hier noch eine etwas schwierigere Übung.
+
+Das Resultat aus Level 3 kannst du als `arithmetic_sum` wiederverwenden:
+$$
+2 \\cdot \\sum_{i = 0}^n i = n \\cdot (n + 1)
+$$
+"
+
+open BigOperators
+
+lemma arithmetic_sum (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
+  induction' n with n hn
+  simp
+  rw [Fin.sum_univ_castSucc]
+  rw [mul_add]
+  simp
+  rw [mul_add, hn]
+  simp_rw [Nat.succ_eq_one_add]
+  ring
+
+Statement
+"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i)^2$."
+  (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), (i : ℕ))^2 := by
+  induction' m with m hm
+  simp
+  rw [Fin.sum_univ_castSucc]
+  simp
+  rw [hm]
+  rw [Fin.sum_univ_castSucc (n := m + 1)]
+  simp
+  rw [add_pow_two]
+  rw [arithmetic_sum]
+  ring
+
+NewLemmas arithmetic_sum add_pow_two
+
+HiddenHint (m : ℕ) : ∑ i : Fin (Nat.zero + 1), ↑i ^ 3 = (∑ i : Fin (Nat.zero + 1), ↑i) ^ 2 =>
+"`simp` kann den Induktionsanfang beweisen."
+
+Hint (m : ℕ) : ∑ i : Fin (Nat.succ m + 1), ↑i ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+"Im Induktionsschritt musst du versuchen, das Goal so umzuformen, dass du
+`∑ i : Fin (m + 1), ↑i ^ 3` (Induktionshypothese) oder
+`2 * (∑ i : Fin (m + 1), ↑i)` (arithmetische Summe) erhälst.
+
+Als erstes kannst du mal mit dem bekannten `rw [Fin.sum_univ_castSucc]` anfangen.
+"
+
+HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), ↑(Fin.castSucc.toEmbedding i) ^ 3 +
+    ↑(Fin.last (m + 1)) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+"Mit `simp` kriegst du das `↑(Fin.castSucc.toEmbedding i)` weg"
+
+Hint (m : ℕ) : ∑ x : Fin (m + 1), (x : ℕ) ^ 3 + (m + 1) ^ 3 =
+    (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+"Jetzt kannst du die Induktionshypothese mit `rw` einsetzen."
+
+Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+"Die linke Seite ist jetzt erst mal gut. Um auf der rechten Seite `Fin.sum_univ_castSucc`
+anzuwenden, haben wir ein Problem: Lean schreibt immer die erste Instanz um, also würde gerne
+auf der linken Seite `(∑ i : Fin (m + 1), ↑i) ^ 2` umschreiben.
+
+Wir können Lean hier weiterhelfen, indem wir manche Argemente von `Fin.sum_univ_castSucc`
+explizit angeben. Die Funktion hat ein Argument mit dem Namen `n`, welches wir z.B. explizit
+angeben können:
+
+```
+rw [Fin.sum_univ_castSucc (n := m + 1)]
+```
+"
+
+HiddenHint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
+    (∑ i : Fin (m + 1), ↑(Fin.castSucc.toEmbedding i) + ↑(Fin.last (m + 1))) ^ 2 =>
+"wieder `simp`"
+
+Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (m + 1), ↑i + (m + 1)) ^ 2 =>
+"Die rechte Seite hat die Form $(a + b)^2$ welche mit `add_pow_two` zu $a^2 + 2ab + b^2$
+umgeschrieben werden kann."
+
+Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
+    (∑ i : Fin (m + 1), ↑i) ^ 2 + (2 * ∑ i : Fin (m + 1), ↑i) * (m + 1) + (m + 1) ^ 2 =>
+"Jetzt hast du in der Mitte `2 * ∑ i : Fin (m + 1), ↑i)`, welches du mit der
+arithmetischen Summe `arithmetic_sum` umschreiben kannst."
+
+Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 =
+    (∑ i : Fin (m + 1), ↑i) ^ 2 + m * (m + 1) * (m + 1) + (m + 1) ^ 2 =>
+"Den Rest sollte `ring` für dich übernehmen."
@@ -1,15 +1,14 @@
-
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
 import TestGame.Metadata

+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
+
 set_option tactic.hygienic false

 open BigOperators

 Game "TestGame"
-World "Induction"
+World "Sum"
 Level 6

 Title "Summe vertauschen"
@@ -1,14 +1,14 @@
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
 import TestGame.Metadata

+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
+
 set_option tactic.hygienic false

 open Nat

 Game "TestGame"
-World "Induction"
+World "Sum"
 Level 2

 Title "endliche Summe"
@@ -1,12 +1,12 @@
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib
-
 import TestGame.Metadata

+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
+
 set_option tactic.hygienic false

 Game "TestGame"
-World "Induction"
+World "Sum"
 Level 2

 Title "endliche Summe"
@@ -1,11 +1,13 @@
 import TestGame.Metadata
+
+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
-import Mathlib

 import TestGame.ToBePorted

 Game "TestGame"
-World "Induction"
+World "Sum"
 Level 5

 Title "Bernoulli Ungleichung"
@@ -0,0 +1,17 @@
+import Mathlib.Algebra.BigOperators.Fin
+
+open BigOperators
+
+open Lean PrettyPrinter Delaborator SubExpr
+
+@[ delab app.Finset.sum]
+def delabFinsetSum : Delab := do
+  guard $ (← getExpr).getAppNumArgs == 5
+  guard $ ((← getExpr).getArg! 3).isAppOf' ``Finset.univ
+  guard $ ((← getExpr).getArg! 4).isLambda
+  withNaryArg 4 do
+    let α ← withBindingDomain delab
+    withBindingBodyUnusedName fun n => do
+      let n : TSyntax `ident := ⟨n⟩
+      let b ← delab
+      `(∑ $n:ident : $α, $b)
@@ -0,0 +1,96 @@
+import Mathlib
+
+open Function Set
+
+example {A B : Type _ } (f : A → B) : f.Injective ↔ ∃ g : B → A, g ∘ f = id := by
+  constructor
+  · intro h
+    -- hard.
+    sorry
+  · intro h
+    rcases h with ⟨g, h⟩
+    unfold Injective
+    intro a b hab
+    rw [←id_eq a, ←id_eq b]
+    rw [← h]
+    rw [comp_apply]
+    rw [hab]
+    simp
+
+
+lemma singleton_mem_powerset
+    {U : Type _} {M : Set U} {x : U} (h : x ∈ M) :
+    {x} ∈ 𝒫 M := by
+  rw [mem_powerset_iff, singleton_subset_iff]
+  assumption
+
+example
+    {U : Type _} (M : Set U) :
+    {A : Set U // A ∈ 𝒫 M} = {A ∈ 𝒫 M | True} := by
+  simp_rw [coe_setOf, and_true]
+
+example
+    {U : Type _} (M : Set U) :
+    {A : Set U // A ∈ 𝒫 M} = 𝒫 M := by
+  rfl
+
+example
+    {U : Type _} (M : Set U) :
+    {x : U // x ∈ M} = M := by
+  rfl
+
+example
+    {U : Type _} (M : Set U) :
+    ∃ (f : M → 𝒫 M), Injective f := by
+  use fun x ↦ ⟨ _, singleton_mem_powerset x.prop ⟩
+  intro a b hab
+  simp at hab
+  rw [Subtype.val_inj] at hab
+  assumption
+
+instance {U : Type _} {M : Set U} : Membership ↑M ↑(𝒫 M) :=
+{ mem := fun x A ↦ x.1 ∈ A.1 }
+
+instance {U : Type _} {M : Set U} : Membership U (Set ↑M) :=
+{ mem := fun x A ↦ _ }
+
+
+example
+    {U : Type _} {M : Set U} (h_empty : M.Nonempty)
+    (f : {x : U // x ∈ M} → {A : Set U // A ∈ 𝒫 M}):
+    ¬ Surjective f := by
+  unfold Surjective
+  push_neg
+  --by_contra h_sur
+  let B : Set M := {x : M | x ∉ (f x)}
+  use ⟨B, sorry⟩
+  intro ⟨a, ha⟩
+  sorry
+  -- Too hard?
+
+#check singleton_mem_powerset
+#check Subtype.val_inj
+
+
+
+-- These are fun exercises for prime.
+example (x : ℕ) : 0 < x ↔ 1 ≤ x := by
+  rfl
+
+lemma le_cancel_left (n x : ℕ) (h : x ≠ 0): n ≤ n * x := by
+  induction n
+  simp
+  simp
+  rw [← zero_lt_iff] at h
+  assumption
+
+
+example (n m : ℕ) (g : m ≠ 0) (h : n ∣ m) : n ≤ m := by
+  rcases h with ⟨x, hx⟩
+  rw [hx]
+  apply le_cancel_left
+  by_contra k
+  rw [k] at hx
+  simp at hx
+  rw [hx] at g
+  contradiction