levels

2023-03-01 17:25:10 +01:00
parent 676560a0df
commit a18582a5f8
20 changed files with 303 additions and 185 deletions
@@ -116,6 +116,7 @@ function computeWorldLayout(worlds) {
    headless: true,
    styleEnabled: false
  })
+// TODO: Jon play around with graph layout

  const layout = cy.layout({name: "klay", klay: {direction: "DOWN"}} as LayoutOptions).run()
  let nodes = {}
@@ -6,6 +6,7 @@ import TestGame.Levels.Predicate
 import TestGame.Levels.Contradiction
 import TestGame.Levels.Prime
 import TestGame.Levels.Sum
+import TestGame.Levels.Induction

 import TestGame.Levels.Numbers
 import TestGame.Levels.Inequality
@@ -42,12 +43,15 @@ Conclusion
 "Fertig!"


-Path Proposition → Implication → Predicate → Prime
-Path Predicate → Contradiction → LeanStuff → SetTheory → SetTheory2 → SetFunction
+Path Proposition → Implication → Predicate
+Path Predicate → Contradiction → Sum → LeanStuff
+Path LeanStuff → SetTheory → SetTheory2 → SetFunction
+
+Path Predicate → Prime → Induction
+Path Sum → Inequality → Induction
+
 Path SetTheory2 → Numbers
-
 Path Module → Basis → Module2
-
-Path Contradiction → Inequality → Sum → LeanStuff → Function → SetFunction
+Path LeanStuff → Function → SetFunction

 MakeGame
@@ -42,7 +42,7 @@ LemmaDoc Nat.succ_pos as Nat.succ_pos in "Nat"
 "
 "

-LemmaDoc zero_lt_iff as zero_lt_iff in "Nat"
+LemmaDoc Nat.pos_iff_ne_zero as Nat.pos_iff_ne_zero in "Nat"
 "
 "

@@ -0,0 +1,5 @@
+import TestGame.Levels.Induction.L01_Induction
+
+Game "TestGame"
+World "Induction"
+Title "Übungen Induktions"
@@ -0,0 +1,37 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Induction"
+Level 1
+
+Title "Induktion"
+
+Introduction
+"
+Dieses Kapitel enthält noch ein paar Übungen zur Induktion.
+"
+
+Statement
+""
+    : 4 ∣ 5^n + 7 := by
+  induction n
+  simp
+  rcases n_ih
+  rw [Nat.pow_succ, Nat.mul_succ, add_assoc, h, mul_comm, ←mul_add]
+  simp
+
+--NewLemmas Nat.pow_succ, Nat.mul_succ, add_assoc, mul_comm, ←mul_add
+
+-- example (n : ℕ) : Even (n^2 + n) := by
+--   induction n
+--   simp
+--   rw [Nat.succ_eq_add_one]
+--   rcases n_ih with ⟨x, h⟩
+--   use x + n_1 + 1
+--   ring_nf at *
+--   rw [←h]
+--   ring
@@ -1,8 +1,7 @@
-import TestGame.Levels.Inequality.L01_Induction
-import TestGame.Levels.Inequality.L02_LE
-import TestGame.Levels.Inequality.L03_Pos
+import TestGame.Levels.Inequality.L01_LE
+import TestGame.Levels.Inequality.L02_Pos
+import TestGame.Levels.Inequality.L03_Linarith
 import TestGame.Levels.Inequality.L04_Linarith
-import TestGame.Levels.Inequality.L05_Linarith

 Game "TestGame"
 World "Inequality"
@@ -2,7 +2,7 @@ import TestGame.Metadata

 Game "TestGame"
 World "Inequality"
-Level 2
+Level 1

 Title "Kleinergleich"

@@ -1,8 +1,12 @@
 import TestGame.Metadata

+import Mathlib.Tactic.LibrarySearch
+
+set_option tactic.hygienic false
+
 Game "TestGame"
 World "Inequality"
-Level 3
+Level 2

 Title "Kleinergleich"

@@ -13,25 +17,45 @@ Es gibt zwei intrinsische Möglichkeiten, zu sagen dass `(n : ℕ)` nicht Null i

 Das folgende Lemma kannst du immer brauchen um zwischen den beiden zu wechseln.

-Note: `0 < n` wird in Lemmanamen oft mit `_pos` beschrieben anstatt `zero_lt`, siehe z.B.
-`Nat.succ_pos`.
+(*Note:* `0 < n` wird in Lemma-Namen oft mit `_pos` beschrieben anstatt `zero_lt`, siehe z.B.
+`Nat.succ_pos`.)
+
+
 "

-Statement zero_lt_iff
-"$0 < n$ und $n \\ne 0$ sind äquivalente Aussagen."
+Statement Nat.pos_iff_ne_zero
+"Benutze Induktion um zu zeigen, dass $0 < n$ und $n \\ne 0$ äquivalent sind."
    (n : ℕ) : 0 < n ↔ n ≠ 0 := by
-  constructor
-  intro h
-  by_contra g
-  rw [g] at h
-  contradiction
-  intro h
  induction n
-  contradiction
+  simp
+  constructor
+  intro
+  simp
+  intro
  apply Nat.succ_pos

+NewTactics simp
 NewLemmas Nat.succ_pos

+Hint : 0 < Nat.zero ↔ Nat.zero ≠ 0 =>
+"Den Induktionsanfang kannst du oft mit `simp` lösen."
+
+Hint (n : ℕ) (h : 0 < n ↔ n ≠ 0) : 0 < Nat.succ n ↔ Nat.succ n ≠ 0 =>
+"Jetzt der Induktionsschritt. Fang mal mit `constructor` an."
+
+HiddenHint (n : ℕ) : 0 < Nat.succ n → Nat.succ n ≠ 0 =>
+"Auch das kann `simp`."
+
+Hint (n : ℕ) : n.succ ≠ 0 =>
+"Auch das kann `simp`."
+
+Hint (n : ℕ) : 0 < Nat.succ n =>
+"Hier kannst du das Lemma `Nat.succ_pos` mit `apply` anwenden."
+
+
+
+/- Second, less ideal path -/
+
 Hint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
 "An dieser Stelle fürst du am besten einen Beweis durch Widerspruch."

@@ -50,5 +74,5 @@ Hint (n : ℕ) (h : n ≠ 0) : 0 < n =>
 HiddenHint (n : ℕ) (h : n ≠ 0) : 0 < n =>
 "Starte mit `induction n`."

-Hint (m : ℕ) : 0 < Nat.succ m =>
-"Hier kannst du das Lemma `Nat.succ_pos` anwenden."
+ HiddenHint : 0 < Nat.zero =>
+"Mit `contradiction` kannst du den Induktionsanfang schliessen."
@@ -0,0 +1,23 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Linarith
+
+Game "TestGame"
+World "Inequality"
+Level 3
+
+Title "Linarith"
+
+Introduction
+"
+Die Taktik `linarith` kann alle Systeme von linearen (Un-)gleichungen über `ℤ`, `ℚ`, etc. lösen.
+Über `ℕ` ist sie etwas schwächer, aber einfache Aussagen kann sie trotzdem beweisen.
+"
+
+Statement
+"Wenn $n \\ge 2$, zeige, dass $n$ nich Null sein kann."
+    (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
+  linarith
+
+NewTactics linarith
+
+NewLemmas Nat.pos_iff_ne_zero
@@ -9,15 +9,20 @@ Title "Linarith"

 Introduction
 "
-Die Taktik `linarith` kann alle Systeme von linearen (Un-)gleichungen über `ℤ`, `ℚ`, etc. lösen.
-Über `ℕ` ist sie etwas schwächer, aber einfache Aussagen kann sie trotzdem beweisen.
+Sobald man mit einem Ring arbeitet, der eine lineare Order hat (also z.B. `ℤ` oder `ℚ`),
+ist `linarith` stärker und kann Systeme von Gleichungen und Ungleichungen angehen.
+
+`linarith` kann aber nur mit linearen Ungleichungen umgehen, mit Termen der Form `x ^ 2`
+kann es nicht umgehen.
 "

 Statement
-"Wenn $n \\ge 2$, zeige, dass $n$ nich Null sein kann."
-    (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
+"
+Angenommen man hat für zwei Ganzzahlen $x, y$ folgende Ungleichungen.
+$$
+\\begin{aligned} 5 * y &\\le 35 - 2 * x \\\\ 2 * y &\\le x + 3 \\end{aligned}
+$$
+Zeige, dass $y \\le 5$.
+"
+    (x y : ℤ) (h₂ : 5 * y ≤ 35 - 2 * x) (h₃ : 2 * y ≤ x + 3) : y ≤ 5 := by
  linarith
-
-NewTactics linarith
-
-NewLemmas zero_lt_iff
@@ -1,28 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Linarith
-
-Game "TestGame"
-World "Inequality"
-Level 5
-
-Title "Linarith"
-
-Introduction
-"
-Sobald man mit einem Ring arbeitet, der eine lineare Order hat (also z.B. `ℤ` oder `ℚ`),
-ist `linarith` stärker und kann Systeme von Gleichungen und Ungleichungen angehen.
-
-`linarith` kann aber nur mit linearen Ungleichungen umgehen, mit Termen der Form `x ^ 2`
-kann es nicht umgehen.
-"
-
-Statement
-"
-Angenommen man hat für zwei Ganzzahlen $x, y$ folgende Ungleichungen.
-$$
-\\begin{aligned} 5 * y &\\le 35 - 2 * x \\\\ 2 * y &\\le x + 3 \\end{aligned}
-$$
-Zeige, dass $y \\le 5$.
-"
-    (x y : ℤ) (h₂ : 5 * y ≤ 35 - 2 * x) (h₃ : 2 * y ≤ x + 3) : y ≤ 5 := by
-  linarith
@@ -1,5 +1,7 @@
 import TestGame.Metadata

+import Mathlib
+
 Game "TestGame"
 World "Inequality"
 Level 1
@@ -8,6 +10,7 @@ Title "Induktion"

 set_option tactic.hygienic false

+
 Introduction
 "
 Hier lernst du Induktion und Ungleichungen kennen. Beides essenziele Grundlagen, die du
@@ -27,9 +30,6 @@ dann gilt $P(n)$ für alle $n \\in \\mathbb{N}.$"
  apply h_step
  assumption

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

@@ -1,6 +1,7 @@
 import TestGame.Levels.LeanStuff.L01_Type
 import TestGame.Levels.LeanStuff.L02_Universe
 import TestGame.Levels.LeanStuff.L03_ImplicitArguments
+import TestGame.Levels.LeanStuff.L04_InstanceArguments

 Game "TestGame"
 World "LeanStuff"
@@ -27,9 +27,10 @@ Zum Beispiel ist `ℕ` der Typ der natürlichen Zahlen, `Prop` der Typ der logis
 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.)
+**Achtung**: Wie du aber gleich sehen wirst sind Typen und Mengen in Lean unterschiedliche
+Sachen.
+
+Hier ein kleines Beispiel zu Typen und Instanzen:
 "

 Statement
@@ -38,5 +39,11 @@ Statement
  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."
+"
+Die Taktik `ring` funktioniert in jedem Typen,
+ist aber stärker, je nach Instanz auf dem Typen.
+
+In Mathlib sind Instanzen `[CommSemiring ℕ]`, [CommRing ℤ]`, `[Field ℚ]`, etc. definiert.
+Die Taktik `ring` muss eine dieser Instanzen finden, die sagen, dass die Addition kommutative ist,
+damit das Lemma `add_comm` angewendet und die Aussage bewiesen werden kann.
+"
@@ -1,61 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "LeanStuff"
-Level 1
-
-Title ""
-
-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 implizite und explizite Argumente 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.)
-
-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
-
-Statement
-    "TODO" : True := by
-  trivial
-
-NewTactics rw
-
-#check not_not
-#check not_or_of_imp
@@ -12,26 +12,40 @@ Title "Universen"

 Introduction
 "
-In der Mathematik stösst man manchmal an Mengentheoretische Grenzen, und so auch in Lean.
+Ein weitere Syntax, den man in Lean abundzu sieht sind Universen.

-Klassisch ist bekannt dass die \"Menge aller Mengen\" nicht existieren kann.
+Diese sind für Mathematiker erst einmal nicht so wichtig, und es reicht zu wissen,
+dass diese existieren.

-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, ...`
+Da alle Objekte in Lean einen Typ haben, kann man sich fragen, welchen Typ hat eigentlich `Type`
+selber? Die Anwort darauf ist dass `Type` vom Typ `Type 1` ist und dieses wiederum vom Typ `Type 2`
+usw.

-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.
+Da Lemmas in Lean gerne so algemein wie möglich formuliert werden, sieht man oft `(R : Type _)`
+anstatt `(R : Type)`, wobei `_` einfach ein Platzhalter für eine Zahl ist.

-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.
+Alternativ kann man auch explizit Universum-Levels definieren, so sind die folgenden beiden
+Aussdrücke äquivalent:
+
+```
+variable (R : Type _)
+
+universe u
+variable (R : Type u)
+```
+
+In der Praxis kann man immer ohne bedenken `Type _` verwendenen und wenn man auf
+(mengentheoretische)
+Probleme stösst, muss man dan eventuell die Universen spezifizieren.
+
+*Die Normalform ist eigentlich `(R : Type _)` zu schreiben solange man kein Grund hat
+das Universum einzuschränken.*
 "

 Statement
-"TODO"
-    (R S : Type _) [CommRing R] (a b : R) : a + b = b + a := by
+""
+    (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."
+-- Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a =>
+-- ""
@@ -1,6 +1,7 @@
 import TestGame.Metadata

 import Mathlib
+import TestGame.Options.BigOperators

 set_option tactic.hygienic false

@@ -20,38 +21,43 @@ 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
+Als Beispiel schauen wir uns ein bekanntes Lemma an:
 ```
-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
+lemma Fin.sum_univ_castSucc {β : Type _} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
+    ∑ i : Fin (n + 1), f i = ∑ i : Fin n, f (↑Fin.castSucc.toEmbedding i) + f (Fin.last n) := by
+  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.
+Hier ist unter anderem `n` als implizites Argument angegeben, da Lean aus `f` herauslesen kann,
+was `n` sein muss. Falls man trotzdem einmal das implizites Argument angeben muss
+(z.B. um `rw` zu helfen, wenn es mehrere Möglichkeiten gibt),
+kann man dies mit `Fin.sum_univ_castSucc (n := m + 1)` machen.
 "

-Statement
-"TODO"
-    (R S : Type _) [CommRing R] (a b : R) : a + b = b + a := by
-  ring
+open BigOperators

-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."
+Statement
+"Zeige $(\\sum_{i=0}^{m} i) + (m + 1) = \\sum_{i=0}^{m + 1} i$."
+    (m : ℕ) :
+      ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by
+  rw [Fin.sum_univ_castSucc (n := m + 1)]
+  rfl
+
+OnlyTactics rw rfl
+
+NewLemmas Fin.sum_univ_castSucc
+
+HiddenHint (m : ℕ) :
+  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
+"Das Lemma `Fin.sum_univ_castSucc` hilft."
+
+Hint (m : ℕ) :
+  ∑ i : Fin m, (Fin.castSucc.toEmbedding i : ℕ) + ↑(Fin.last m) + (m + 1) =
+  ∑ i : Fin (Nat.succ m + 1), ↑i =>
+"Hier hat `rw` die falsche der beiden Summen umgeschrieben. Hilf ihm mit
+`rw [Fin.sum_univ_castSucc (n := m + 1)]`."
+
+Hint (m : ℕ) :
+  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) =
+  ∑ i : Fin (m + 1), ↑i + (m + 1) =>
+"Jetzt sind beide Seiten gleich und das Goal kann mit `rfl` geschlossen werden."
@@ -0,0 +1,78 @@
+import TestGame.Metadata
+
+import Mathlib
+import TestGame.Options.BigOperators
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "LeanStuff"
+Level 4
+
+Title "Instanz-Argumente"
+
+Introduction
+"
+Bezüglich impliziten Argumente gibt es noch einige weitere Punkte oder Tricks,
+die man wissen sollte.
+
+* Instanz-Argumente wie `[Ring R]` sind auch impilzite Argumente. Der Unterschied ist, dass
+  Lean einen anderen Mechanismus braucht, um diese zu füllen: Es sucht nach einer entsprechenden
+  *Instanz* und, setzt die erste solche Instanz ein.
+  Ausserhalb eines Beweises könnte man auch mit
+  ```
+  #synth Ring ℤ
+  ```
+  testen, ob Lean eine ensprechende Instanz findet. Instanzen werden dafür gebraucht, Typen
+  mit (algebraischer) Stukturen zu versehen.
+* Ein `_` irgendwo im Lean-Code ist immer ein Platzhalter, den Lean versucht aus dem Kontext zu
+  füllen. Das kann praktisch sein, wenn man etwas nicht ausschreiben will, das offensichtlich ist.
+* Mit `@` kann man forcieren, dass alle Argumente explizit sind.
+  Für ein Lemma
+  ```
+  lemma not_or_of_imp {A B : Prop} (h : A → B) :
+      ¬A ∨ B := sorry
+  ```
+  heisst das zum Beispiel dass `not_or_of_imp g` das gleiche ist wie
+  `@not_or_of_imp _ _ g`.
+
+  Und `Fin.sum_univ_castSucc (n := m + 1)` könnte man auch als
+  `@Fin.sum_univ_castSucc _ _ (m + 1)` schreiben.
+"
+
+open BigOperators
+
+Statement
+"Zeige $(\\sum_{i=0}^{m} i) + (m + 1) = \\sum_{i=0}^{m + 1} i$."
+    (m : ℕ) :
+      ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by
+  rw [Fin.sum_univ_castSucc (n := m + 1)]
+  rfl
+
+OnlyTactics rw rfl
+
+NewLemmas Fin.sum_univ_castSucc
+
+Hint (m : ℕ) :
+  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
+"
+  Probier nochmals das gleiche, diesmal mit
+```
+rw [@Fin.sum_univ_castSucc _ _ (m + 1)]
+```
+anstatt
+```
+rw [Fin.sum_univ_castSucc (n := m + 1)]
+```
+"
+
+Hint (m : ℕ) :
+  ∑ i : Fin m, (Fin.castSucc.toEmbedding i : ℕ) + ↑(Fin.last m) + (m + 1) =
+  ∑ i : Fin (Nat.succ m + 1), ↑i =>
+"Sackgasse!"
+
+
+Hint (m : ℕ) :
+  ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) =
+  ∑ i : Fin (m + 1), ↑i + (m + 1) =>
+"Jetzt sind beide Seiten gleich und das Goal kann mit `rfl` geschlossen werden."
@@ -34,7 +34,6 @@ Statement
  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 =>
@@ -3,6 +3,8 @@ import TestGame.Metadata
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring

+set_option tactic.hygienic false
+
 Game "TestGame"
 World "Sum"
 Level 3
@@ -13,13 +15,19 @@ 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.
+Mit `induction n` startet man einen Induktionsbeweis. Dies erstellt 2 neue Goals:
+
+* **Induktionsanfang**: `n = 0`. Dieser kann ganz oft direkt mit `simp` bewiesen werden.
+* **Induktionsschritt**: Man kriegt eine Annahme `(n_ih : P n)` und muss `P (n + 1)`
+  beweisen. Für endliche Summen will man normalerweise danach zuerst
+  `rw [Fin.sum_univ_castSucc]` brauchen, 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`.
+Eine technische Sonderheit bezüglich endlichen Summen
+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*.
@@ -28,25 +36,21 @@ Gleichermassen, kommen hier im Induktionsschritt die Terme `↑(↑Fin.castSucc.
 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
+  induction n
  simp
  rw [Fin.sum_univ_castSucc]
  rw [mul_add]
  simp
-  rw [hn]
+  rw [n_ih]
  rw [Nat.succ_eq_add_one]
  ring

-NewTactics ring
+NewTactics induction
 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) =>