From 8a563cf6f458c575cfc82c5a7bec65ab84d2bf0d Mon Sep 17 00:00:00 2001 From: Marco Colombo Date: Thu, 4 Jul 2024 17:02:25 +0200 Subject: [PATCH] Fix hint. --- Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean index 5610150..f9b6223 100644 --- a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean +++ b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean @@ -74,7 +74,7 @@ Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by exact one_ne_zero Hint (hidden := true) "Now you can `apply le_mul_right at h2`." apply le_mul_right at h2 - Hint (hidden := true) "Now `rw [h] at h2` so you can `apply le_one at h2`." + Hint (hidden := true) "Now `rw [{h}] at {h2}` so you can `apply le_one at {h2}`." rw [h] at h2 apply le_one at h2 Hint (hidden := true) "Now `cases h2 with h0 h1` and deal with the two