From f540b6376432ea8d99e09a96b4e4b419bd41d9b9 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Wed, 8 Mar 2023 16:20:14 +0100 Subject: [PATCH] test example --- server/testgame/TestGame/Levels/Sum/L02_Sum.lean | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean index 83e8429..c7b722f 100644 --- a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean +++ b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean @@ -31,15 +31,11 @@ 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] + Hint "Die zweite Summe `∑ x : Fin n, 1` kann `simp` zu `n` vereinfacht werden." simp - ring - -NewLemma Finset.sum_add_distrib add_comm + Hint "Bis auf Umordnung sind jetzt beide Seiten gleich, darum kann `ring` das Goal schließen. -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." + ring -Alternativ kann man auch mit `rw [add_comm]` dies explizit umordnen." +NewLemmas Finset.sum_add_distrib add_comm