From 0d828eda14220e4ed80a14068dbf37b4422c5a7d Mon Sep 17 00:00:00 2001
From: Ughur Alakbarov <58857108+ugur-a@users.noreply.github.com>
Date: Sat, 29 Jun 2024 12:37:32 +0200
Subject: [PATCH] Fix quoting

---
 Game/Levels/AdvMultiplication/L09mul_left_cancel.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean b/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean
index fc39c0b..2163fdc 100644
--- a/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean
+++ b/Game/Levels/AdvMultiplication/L09mul_left_cancel.lean
@@ -23,8 +23,8 @@ the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a
 so the induction hypothesis does not apply!
 
 Assume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is
-\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,
-because we now have the flexibility to change `c`.\"
+\"for all `c`, if `a * b = a * c` then `b = c`\". This *can* be proved by induction,
+because we now have the flexibility to change `c`.
 "
 
 Statement mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = c := by