diff --git a/Game/Levels/LinearIndependenceSpanWorld/Level03.lean b/Game/Levels/LinearIndependenceSpanWorld/Level03.lean
index 41cb724..80782e7 100644
--- a/Game/Levels/LinearIndependenceSpanWorld/Level03.lean
+++ b/Game/Levels/LinearIndependenceSpanWorld/Level03.lean
@@ -49,7 +49,7 @@ Statement span_mono {A B : Set V} (hAB : A ⊆ B) : span K V A ⊆ span K V B :=
   Hint (hidden := true) "Try `intro x hxA`"
   intro x hxA
   Hint "Now we have `x ∈ span K V A` and need to show `x ∈ span K V B`."
-  Hint "Let's unfold the definition of span to see what it means for x to be in the span of A."
+  Hint "Let's unfold the definition of span everywhere to see what it means for x to be in the span of A."
   Hint (hidden := true) "Try `unfold span at *`"
   unfold span at *
   Hint "The span consists of all linear combinations. Let's unfold that definition too."
diff --git a/Game/Levels/TutorialWorld/Level05.lean b/Game/Levels/TutorialWorld/Level05.lean
index f071d92..8f3e52b 100644
--- a/Game/Levels/TutorialWorld/Level05.lean
+++ b/Game/Levels/TutorialWorld/Level05.lean
@@ -8,9 +8,11 @@ Title "The `unfold` and `apply` tactics"
 ## Summary
 
 If we have some object or function with some definition, `unfold object` will rewrite the object
-with its definition everywhere. Lean often unfolds terms automatically, but some tactics and definitions
+with its definition in the goal. Lean often unfolds terms automatically, but some tactics and definitions
 are not unfolded automatically. The `unfold` tactic also helps make it easier to take the next steps.
 
+`unfold object at h` unfolds at the assumption `h` whereas `unfold object at *` unfolds everywhere.
+
 ## Example:
 
 If you have a goal `(P → Q) → (¬ Q → ¬ P)`, with `¬ P` (\"Not\" P) being defined as `P → False`,