From 47e9945ff9a01578e62eab7c9529b74e6a7e498f Mon Sep 17 00:00:00 2001 From: Hans Christian Schmitz Date: Fri, 17 Jan 2025 08:02:52 +0100 Subject: [PATCH] Fix typo in `contrapose! h` explainer in Algo L7 The explainer mistakenly swapped an n for an m, possibly causing confusion with the explainer mentioning a different hypothesis than the one resulting from the tactic, and one from which alone one cannot derive the new goal. --- Game/Levels/Algorithm/L07succ_ne_succ.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Algorithm/L07succ_ne_succ.lean b/Game/Levels/Algorithm/L07succ_ne_succ.lean index 555a1ec..42761f1 100644 --- a/Game/Levels/Algorithm/L07succ_ne_succ.lean +++ b/Game/Levels/Algorithm/L07succ_ne_succ.lean @@ -60,7 +60,7 @@ TheoremDoc MyNat.succ_ne_succ as "succ_ne_succ" in "Peano" /-- If $a \neq b$ then $\operatorname{succ}(a) \neq\operatorname{succ}(b)$. -/ Statement succ_ne_succ (m n : ℕ) (h : m ≠ n) : succ m ≠ succ n := by Hint "Start with `contrapose! h`, to change the goal into its - contrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`." + contrapositive, namely a hypothesis of `succ m = succ n` and a goal of `m = n`." contrapose! h Hint "Can you take it from here? (note: if you try `contrapose! h` again, it will take you back to where you started!)"