levels up to 'Lean'

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

@@ -3,6 +3,8 @@ import TestGame.Metadata
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Tactic.Ring
 
+import TestGame.Options.BigOperators
+
 set_option tactic.hygienic false
 
 Game "TestGame"
@@ -56,7 +58,7 @@ 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) =>
+Hint : 2 * ∑ i : Fin (Nat.zero + 1), ↑i = Nat.zero * (Nat.zero + 1) =>
 "Den Induktionsanker $n = 0$ kann `simp` oft beweisen."
 
 Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) :
@@ -77,7 +79,8 @@ 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."
+"`simp` vereinfacht `↑(↑Fin.castSucc.toEmbedding i)` zu `↑i`.
+Danach 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) =>

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

@@ -36,7 +36,7 @@ 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 =>
+HiddenHint : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 =>
 "
 Den Induktionsanfang kannst du wieder mit `simp` beweisen.
 "
@@ -54,5 +54,5 @@ 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.
+Mit `rw [Nat.succ_eq_add_one]` und `ring` kannst du hier abschliessen.
 "

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

@@ -44,7 +44,7 @@ $$
 open BigOperators
 
 Statement
-"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i)^2$."
+"Zeige $\\sum_{i = 0}^m i^3 = (\\sum_{i = 0}^m i)^2$."
   (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), (i : ℕ))^2 := by
   induction' m with m hm
   simp
@@ -59,26 +59,35 @@ Statement
 
 NewLemmas arithmetic_sum add_pow_two
 
-HiddenHint (m : ℕ) : ∑ i : Fin (Nat.zero + 1), ↑i ^ 3 = (∑ i : Fin (Nat.zero + 1), ↑i) ^ 2 =>
+HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (m + 1), ↑i) ^ 2 =>
+"Führe auch hier einen Induktionsbeweis."
+
+HiddenHint : ∑ 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.
+Hint (m : ℕ) : ∑ i : Fin (Nat.succ m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+"Im Induktionsschritt willst du das Goal so umformen, dass du folgende Therme
+ersetzen kannst:
 
+* `∑ i : Fin (m + 1), ↑i ^ 3` (Induktionshypothese)
+* `2 * (∑ i : Fin (m + 1), ↑i)` (arithmetische Summe)
+"
+
+HiddenHint (m : ℕ) : ∑ i :
+    Fin (Nat.succ m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+"
 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 +
+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."
+"Jetzt kannst du die Induktionshypothese benützen."
 
-Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 =>
+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.
@@ -94,12 +103,18 @@ 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`"
+"Wenn du noch einen AUsdruck `↑(Fin.castSucc.toEmbedding i)` hast, solltest du mal
+`simp` aufrufen."
 
 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."
 
+HiddenHint (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 =>
+"Wenn du noch einen AUsdruck `↑(Fin.castSucc.toEmbedding i)` hast, solltest du mal
+`simp` aufrufen."
+
 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