diff --git a/Game/Levels/Implication/L06intro.lean b/Game/Levels/Implication/L06intro.lean
index 138d7a94..9d3339bc 100644
--- a/Game/Levels/Implication/L06intro.lean
+++ b/Game/Levels/Implication/L06intro.lean
@@ -27,8 +27,8 @@ NewTactic intro
 Introduction
 "We have seen how to `apply` theorems and assumptions
 of the form `P → Q`. But what if our *goal* is of the form `P → Q`?
-To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"
-in Lean. We do this with the `intro` tactic.
+To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\".
+In Lean, we do this with the `intro` tactic.
 "
 
 /-- $x=37\implies x=37$. -/