From 71e5424a17e3f23c9100bdc596bcfc3df3d9709b Mon Sep 17 00:00:00 2001 From: Arnaud Date: Fri, 11 Jul 2025 14:00:36 +0200 Subject: [PATCH] Remove extra space, that prevent translation --- Game/Levels/AdvMultiplication/L09mul_left_cancel.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean b/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean index 2163fdc..997fbc9 100644 --- a/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean +++ b/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean @@ -40,7 +40,7 @@ Statement mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = · rw [h2] rfl · Hint "The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\". - You can `apply` it `at` any hypothesis of the form `a * d = a * ?`. " + You can `apply` it `at` any hypothesis of the form `a * d = a * ?`." Hint (hidden := true) "Split into cases `c = 0` and `c = succ e` with `cases c with e`." cases c with e · rw [mul_succ, mul_zero] at h