diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index a8ff296..c7ba685 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -23,7 +23,7 @@ Zeige, dass $A$ wahr ist." assumption HiddenHint (A : Prop) (hA : A) : A => -"Auch hier kann `assumption` den Beweis von `A` finden." +"Auch hier kann `assumption` den Beweis von `{A}` finden." Conclusion "" diff --git a/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean index 76ab5f6..640072a 100644 --- a/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean +++ b/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean @@ -33,7 +33,7 @@ $\\sum_{i = 0}^n (2n + 1) = n ^ 2$." HiddenHint (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 => " -Fange wieder mit `induction n` an. +Fange wieder mit `induction {n}` an. " HiddenHint : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 => @@ -49,7 +49,7 @@ 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. +Hier kommt die Induktionshypothese {hn} ins Spiel. " HiddenHint (n : ℕ) : n ^ 2 + (2 * n + 1) = Nat.succ n ^ 2 =>