From 9815f76598b3eb4ac13b8613dd2fb5dd7e19f123 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Fri, 22 Dec 2023 16:33:02 +0000 Subject: [PATCH] hx -> h2 in mul_right_eq_one --- .../L06mul_right_eq_one.lean | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean index f355176..e55b8ea 100644 --- a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean +++ b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean @@ -61,21 +61,22 @@ We'll prove it using a new and very useful tactic called `have`. " Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by - Hint "We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0` - which we don't have. Yet. Execute `have h2 : x * y ≠ 0`. You'll be asked to + Hint (strict := true) "We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0` + which we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\ne`). + You'll be asked to prove it, and then you'll have a new hypothesis which you can apply `le_mul_right` to." - have hx : x * y ≠ 0 + have h2 : x * y ≠ 0 rw [h] exact one_ne_zero - Hint (hidden := true) "Now you can `apply le_mul_right at hx`." - apply le_mul_right at hx - Hint (hidden := true) "Now `rw [h] at hx` so you can `apply le_one at hx`." - rw [h] at hx - apply le_one at hx - Hint (hidden := true) "Now `cases hx with h0 h1` and deal with the two + 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 hx`." + rw [h] at h2 + apply le_one at h2 + Hint (hidden := true) "Now `cases h2 with h0 h1` and deal with the two cases separately." - cases hx with h0 h1 + cases h2 with h0 h1 · rw [h0, zero_mul] at h Hint (hidden := true) "`tauto` is good enough to solve this goal." tauto