From a0fff024d78a5e37d86c1cf3ef60f13b529f992a Mon Sep 17 00:00:00 2001
From: JadAbouHawili <81527369+JadAbouHawili@users.noreply.github.com>
Date: Sat, 18 Apr 2026 11:13:47 +0300
Subject: [PATCH] doc: fix inaccurate unfold tactic doc

---
 Game/Levels/LinearIndependenceSpanWorld/Level03.lean | 2 +-
 Game/Levels/TutorialWorld/Level05.lean               | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/Game/Levels/LinearIndependenceSpanWorld/Level03.lean b/Game/Levels/LinearIndependenceSpanWorld/Level03.lean
index 41cb724e..80782e7d 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 f071d923..8f3e52b0 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`,