Add TheoremDoc for le_of_sq_le_sq and fix Level09 hint mismatches

- Add TheoremDoc for le_of_sq_le_sq with usage note about LinearAlgebraGame. prefix
- Fix Level09 hints for fx_sum_equality and fw_sum_equality to include
  LinearAlgebraGame. prefix (matching actual proof code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: ZRTMRH

Game/Levels/InnerProductWorld/Level07.lean

@@ -36,6 +36,14 @@ TheoremDoc LinearAlgebraGame.Cauchy_Schwarz as "Cauchy_Schwarz" in "Inner Produc
 variable {V : Type} [AddCommGroup V] [VectorSpace ℂ V]  [InnerProductSpace_v V]
 open Function Set VectorSpace Real InnerProductSpace_v Complex
 
+/--
+If `a² ≤ b²` and `b ≥ 0`, then `a ≤ b`. This is useful for converting squared inequalities
+back to regular inequalities when working with norms.
+
+**Usage:** Use the full name `LinearAlgebraGame.le_of_sq_le_sq` when applying this theorem.
+-/
+TheoremDoc LinearAlgebraGame.le_of_sq_le_sq as "le_of_sq_le_sq" in "Inner Product"
+
 -- Helper theorem: taking square roots preserves inequalities for non-negative numbers
 theorem le_of_sq_le_sq {a : ℝ} {b : ℝ} (h : a^2 ≤ b ^2 ) (hb : 0≤ b) : a ≤ b :=
   le_abs_self a |>.trans <| abs_le_of_sq_le_sq h hb

Game/Levels/LinearIndependenceSpanWorld/Level09.lean

@@ -271,7 +271,7 @@ Statement remove_redundant_span
   Hint "Now, you can prove that summing `fx'` over our set gives the correct value."
   Hint "We use a helper lemma that shows the sum equality."
   Hint "This lemma shows that fx' gives us x minus the contribution from w."
-  Hint (hidden := true) "Try `have fx'_sum : x - (fx w • w) = (sw ∪ (sx \\ \{{w}})).sum (fun v => fx' v • v) := fx_sum_equality K V x w sw sx fx fx' hw hfx hfx' set_eq`"
+  Hint (hidden := true) "Try `have fx'_sum : x - (fx w • w) = (sw ∪ (sx \\ \{{w}})).sum (fun v => fx' v • v) := LinearAlgebraGame.fx_sum_equality K V x w sw sx fx fx' hw hfx hfx' set_eq`"
   have fx'_sum : x - (fx w • w) = (sw ∪ (sx \ {w})).sum (fun v => fx' v • v) :=
     LinearAlgebraGame.fx_sum_equality K V x w sw sx fx fx' hw hfx hfx' set_eq
 
@@ -284,7 +284,7 @@ Statement remove_redundant_span
 
   Hint "Prove the sum equality by expanding definitions."
   Hint "This lemma shows that fw' reconstructs exactly the fx w • w term we need."
-  Hint (hidden := true) "Try `have fw'_sum : fx w • w = (sw ∪ (sx \\ \{{w}})).sum (fun v => fw' v • v) := fw_sum_equality K V w sw sx fx fw fw' hfw hfw'`"
+  Hint (hidden := true) "Try `have fw'_sum : fx w • w = (sw ∪ (sx \\ \{{w}})).sum (fun v => fw' v • v) := LinearAlgebraGame.fw_sum_equality K V w sw sx fx fw fw' hfw hfw'`"
   have fw'_sum : fx w • w = (sw ∪ (sx \ {w})).sum (fun v => fw' v • v) :=
     LinearAlgebraGame.fw_sum_equality K V w sw sx fx fw fw' hfw hfw'