levels

server/testgame/TestGame/LemmaDocs.lean

@@ -126,3 +126,6 @@ LemmaDoc arithmetic_sum as arithmetic_sum in "Sum"
 
 LemmaDoc add_pow_two as add_pow_two in "Nat"
 ""
+
+LemmaDoc Finset.sum_comm as Finset.sum_comm in "Sum"
+""

server/testgame/TestGame/Levels/Induction/L01_Induction.lean

@@ -16,8 +16,8 @@ Dieses Kapitel enthält noch ein paar Übungen zur Induktion.
 "
 
 Statement
-""
-    : 4 ∣ 5^n + 7 := by
+"Zeige dass $5^n + 7$ durch $4$ teilbar ist."
+    (n : ℕ) : 4 ∣ 5^n + 7 := by
   induction n
   simp
   rcases n_ih

server/testgame/TestGame/Levels/Predicate/L06_Exists.lean

@@ -24,7 +24,7 @@ Beachte das Komma `,` welches die Variablen des `∃` (`\\exists`) von der Aussa
 
 Hierzu gibt es 3 wichtige Taktiken:
 
-1) Definitionen wie `Even` kann man mit `unfold even at *` im Infoview einsetzen.
+1) Definitionen wie `Even` kann man mit `unfold Even at *` im Infoview einsetzen.
    Das ändert Lean-intern nichts und ist nur für den Benutzer. Man kann auch einen
    Term `(h : Even x)` einfach so behandeln als wäre es ein Term `(h : ∃ r, x = 2 * r)`.
 2) Bei einer Annahme `(h : ∃ r, ...)` kann man mit `rcases h with ⟨y, hy⟩` ein solches `y`
@@ -43,16 +43,16 @@ Statement even_square
   ring
 
 Hint (n : ℕ) (h : Even n) : Even (n ^ 2) =>
-"Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
-`unfold even at *` ersetzen.
+"Wenn du die Definition von `Even` nicht kennst, kannst du diese mit `unfold Even` oder
+`unfold Even at *` ersetzen.
 Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
 genau gleich, wenn du das `unfold` rauslöscht."
 
-Hint (n : ℕ) (h : ∃ r, n = 2 * r) : ∃ r, n ^ 2 = 2 * r =>
+Hint (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r =>
 "Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
 ein `x` erhalten, dass die Aussage erfüllt."
 
-Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = 2 * r =>
+Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r =>
 "Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
 die Aussage erfüllen soll."
 

server/testgame/TestGame/Levels/Sum.lean

@@ -2,8 +2,8 @@ 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
+import TestGame.Levels.Sum.L05_SumComm
+import TestGame.Levels.Sum.L06_Summary
 
 Game "TestGame"
 World "Sum"

server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean

@@ -18,7 +18,7 @@ set_option tactic.hygienic false
 
 open BigOperators
 
-Statement
+Statement odd_arithmetic_sum
 "Zeige folgende Gleichung zur Summe aller ungeraden Zahlen:
 
 $\\sum_{i = 0}^n (2n + 1) = n ^ 2$."

server/testgame/TestGame/Levels/Sum/L05_SumComm.lean

@@ -0,0 +1,36 @@
+import TestGame.Metadata
+
+import TestGame.Options.BigOperators
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Tactic.Ring
+
+import TestGame.Options.ArithSum
+
+set_option tactic.hygienic false
+
+open BigOperators
+
+Game "TestGame"
+World "Sum"
+Level 5
+
+Title "Summe vertauschen"
+
+Introduction
+"
+Verschachtelte endliche Summen kann man beliebig tauschen.
+
+$$\\sum_{i=0}^n\\sum_{j=0}^m a_{ij} = \\sum_{j=0}^m\\sum_{i=0}^n a_{ij}$$
+
+Dieses Lemma heisst `Finset.sum_comm`
+"
+
+
+Statement
+"Zeige dass
+$\\sum_{i=0}^n\\sum_{j=0}^m  2^i (1 + j) = \\sum_{j=0}^m\\sum_{i=0}^n  2^i (1 + j)$."
+    (n m : ℕ) : ∑ i : Fin n, ∑ j : Fin m, ( 2^i * (1 + j) : ℕ) =
+    ∑ j : Fin m, ∑ i : Fin n, ( 2^i * (1 + j) : ℕ) := by
+  rw [Finset.sum_comm]
+
+NewLemmas Finset.sum_comm

server/testgame/TestGame/Levels/Sum/L06_SumComm.lean

@@ -1,24 +0,0 @@
-import TestGame.Metadata
-
-import TestGame.Options.BigOperators
-import Mathlib.Algebra.BigOperators.Fin
-
-set_option tactic.hygienic false
-
-open BigOperators
-
-Game "TestGame"
-World "Sum"
-Level 6
-
-Title "Summe vertauschen"
-
-Introduction
-"
-"
-
-Statement
-""
-    (n m : ℕ) : ∑ i : Fin n, ∑ j : Fin m, (i : ℕ) * j =
-    ∑ j : Fin m, ∑ i : Fin n, (i : ℕ) * j := by
-  rw [Finset.sum_comm]

server/testgame/TestGame/Levels/Sum/L06_Summary.lean

@@ -5,17 +5,34 @@ import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
 import TestGame.ToBePorted
+import TestGame.Options.ArithSum
 
 Game "TestGame"
 World "Sum"
-Level 5
+Level 6
 
 set_option tactic.hygienic false
 
-Title "Quadrat der Arithmetischen Summe"
+Title "Zusammenfassung"
 
 Introduction
 "
+Zusammenfassung aus diesem Kapitel
+
+## Notationen / Begriffe
+
+|                      | Beschreibung                              |
+|:---------------------|:------------------------------------------|
+| `Fin n`              | Ist ein Typ mit Zahlen $0, \\ldots, n-1$. |
+| `∑ (i : Fin n), a i` | $\\sum_{i=0}^{n-1} a_i$                   |
+
+## Taktiken
+
+|    | Taktik                    | Beispiel                             |
+|:---|:--------------------------|:-------------------------------------|
+| 20 | `simp`                    | Simplifikation.                      |
+| 21 | `induction n`             | Induktion über $n$                   |
+
 Und hier noch eine etwas schwierigere Übung.
 
 Das Resultat aus Level 3 kannst du als `arithmetic_sum` wiederverwenden:
@@ -26,16 +43,6 @@ $$
 
 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

server/testgame/TestGame/Options/ArithSum.lean

@@ -0,0 +1,14 @@
+import Mathlib.Tactic.Ring
+import Mathlib.Algebra.BigOperators.Fin
+
+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