From a4c2dcb12b44ba9bfb32496842e258c50fc039f1 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Wed, 29 Mar 2023 17:14:37 +0200 Subject: [PATCH] rewrite story for Predicate (continued) --- server/adam/Adam/Levels/Predicate/L02_Rewrite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean index 6d49164..4b0cd4f 100644 --- a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean +++ b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean @@ -14,7 +14,7 @@ Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c : Hint "**Du**: Schau mal, dieses Problem sieht so ähnlich aus wie eines, das wir auf *Implis* schon gelöst hatten. Nur, das hier jetzt Gleichheiten von Zahlen statt Genau-Dann-Wenn-Aussagen stehen! - **Robo**: Richtig. Und im Grunde macht das gar keinen Unterscheid. Du kannst `=` und `↔` praktisch mit `rw` praktisch gleich behandeln." + **Robo**: Richtig. Und im Grunde macht das gar keinen Unterscheid. Du kannst `=` und `↔` praktisch mit `rw` praktisch g"""""leich behandeln." Hint (hidden := true) "**Du**: Also auch `rw [hₓ]` und `rw [← hₓ]`? **Robo**: Probiers doch einfach."