From f837b2f86db1ccdb78011e0475925a9b8aa134f3 Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Sat, 18 Jul 2026 18:41:45 +0300
Subject: [PATCH] fix: attach Verso docs to exercise/example labels

Several exercise and example markers used plain /- comments, so the
labels never attached to the following declarations.

Co-authored-by: Cursor <cursoragent@cursor.com>
---
 Analysis/Section_3_5.lean | 4 ++--
 Analysis/Section_6_4.lean | 2 +-
 Analysis/Section_6_6.lean | 5 ++---
 Analysis/Section_7_2.lean | 3 +--
 Analysis/Section_9_2.lean | 4 ++--
 5 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/Analysis/Section_3_5.lean b/Analysis/Section_3_5.lean
index 7fb747590..aaa9f633e 100644
--- a/Analysis/Section_3_5.lean
+++ b/Analysis/Section_3_5.lean
@@ -439,13 +439,13 @@ theorem SetTheory.Set.diff_prod (A B C:Set) : (A \ B) ×ˢ C = (A ×ˢ C) \ (B 
 theorem SetTheory.Set.inter_of_prod (A B C D:Set) :
     (A ×ˢ B) ∩ (C ×ˢ D) = (A ∩ C) ×ˢ (B ∩ D) := by sorry
 
-/- Exercise 3.5.5 -/
+/-- Exercise 3.5.5 -/
 def SetTheory.Set.union_of_prod :
   Decidable (∀ (A B C D:Set), (A ×ˢ B) ∪ (C ×ˢ D) = (A ∪ C) ×ˢ (B ∪ D)) := by
   -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry
 
-/- Exercise 3.5.5 -/
+/-- Exercise 3.5.5 -/
 def SetTheory.Set.diff_of_prod :
   Decidable (∀ (A B C D:Set), (A ×ˢ B) \ (C ×ˢ D) = (A \ C) ×ˢ (B \ D)) := by
   -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean
index f056b72da..c1f47fbb4 100644
--- a/Analysis/Section_6_4.lean
+++ b/Analysis/Section_6_4.lean
@@ -308,7 +308,7 @@ theorem Sequence.Cauchy_iff_convergent (a:Sequence) :
 theorem Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ ¬ (a:Sequence).sup < (b:Sequence).sup := by
   sorry
 
-/- Exercise 6.4.7 -/
+/-- Exercise 6.4.7 -/
 def Sequence.tendsTo_real_iff :
   Decidable (∀ (a:Sequence) (x:ℝ), a.TendsTo x ↔ a.abs.TendsTo x) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
diff --git a/Analysis/Section_6_6.lean b/Analysis/Section_6_6.lean
index ee6361cb3..ff4c3c79a 100644
--- a/Analysis/Section_6_6.lean
+++ b/Analysis/Section_6_6.lean
@@ -20,7 +20,7 @@ namespace Chapter6
 /-- Definition 6.6.1 -/
 abbrev Sequence.subseq (a b: ℕ → ℝ) : Prop := ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ n, b n = a (f n)
 
-/- Example 6.6.2 -/
+/-- Example 6.6.2 -/
 example (a:ℕ → ℝ) : Sequence.subseq a (fun n ↦ a (2 * n)) := by sorry
 
 example {f: ℕ → ℕ} (hf: StrictMono f) : Function.Injective f := by sorry
@@ -60,8 +60,7 @@ theorem Sequence.convergent_of_subseq_of_bounded {a:ℕ→ ℝ} (ha: (a:Sequence
   have := limit_point_of_limsup hL_plus
   rw [limit_point_iff_subseq] at this; peel 2 this; solve_by_elim
 
-/- Exercise 6.6.2 -/
-
+/-- Exercise 6.6.2 -/
 def Sequence.exist_subseq_of_subseq :
   Decidable (∃ a b : ℕ → ℝ, a ≠ b ∧ Sequence.subseq a b ∧ Sequence.subseq b a) := by
     -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
diff --git a/Analysis/Section_7_2.lean b/Analysis/Section_7_2.lean
index 3e55513ff..a93f45840 100644
--- a/Analysis/Section_7_2.lean
+++ b/Analysis/Section_7_2.lean
@@ -273,8 +273,7 @@ theorem Series.telescope {a:ℕ → ℝ} (ha: Filter.atTop.Tendsto a (nhds 0)) :
     ((fun n:ℕ ↦ a n - a (n+1)):Series).convergesTo (a 0) := by
   sorry
 
-/- Exercise 7.2.1  -/
-
+/-- Exercise 7.2.1 -/
 def Series.exercise_7_2_1_convergent :
   Decidable ( (mk' (m := 1) (fun n ↦ (-1:ℝ)^(n:ℤ))).converges ) := by
   -- The first line of this proof should be `apply isTrue` or `apply isFalse`.
diff --git a/Analysis/Section_9_2.lean b/Analysis/Section_9_2.lean
index 2f80a6285..dda4c38e4 100644
--- a/Analysis/Section_9_2.lean
+++ b/Analysis/Section_9_2.lean
@@ -51,12 +51,12 @@ example : f_9_2_2 ∘ g_9_2_2 = fun x ↦ 4*x^2 := by grind
 
 example : g_9_2_2 ∘ f_9_2_2 = fun x ↦ 2*x^2 := by grind
 
-/- Exercise 9.2.1.  -/
-
+/-- Exercise 9.2.1. -/
 def Exercise_9_2_1a : Decidable (∀ (f g h : ℝ → ℝ), (f+g) ∘ h = f ∘ h + g ∘ h) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry
 
+/-- Exercise 9.2.1. -/
 def Exercise_9_2_1b : Decidable (∀ (f g h : ℝ → ℝ), f ∘ (g + h) = f ∘ g + f ∘ h) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry