From 0a3c422511f01c70444b103f92db972567bd6c75 Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Sat, 15 Aug 2026 09:07:32 +0530
Subject: [PATCH] fix: disambiguate duplicate Verso labels across Chapter 6

Thirteen docstrings in Sections 6.3-6.7 shared a label with a sibling
declaration: Definition 6.3.1, Lemma 6.4.13, Lemma 6.5.2, Lemma 6.6.4 and
Proposition 6.7.3(e).

Each now names the case it covers - sup/inf, limsup/liminf, the three ratio
regimes of the geometric limit, reflexivity/transitivity - keeping the
statement number intact.
---
 Analysis/Section_6_3.lean | 4 ++--
 Analysis/Section_6_4.lean | 8 ++++----
 Analysis/Section_6_5.lean | 6 +++---
 Analysis/Section_6_6.lean | 4 ++--
 Analysis/Section_6_7.lean | 4 ++--
 5 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/Analysis/Section_6_3.lean b/Analysis/Section_6_3.lean
index e9e2939d7..8e9a86d0b 100644
--- a/Analysis/Section_6_3.lean
+++ b/Analysis/Section_6_3.lean
@@ -20,10 +20,10 @@ Main constructions and results of this section:
 
 namespace Chapter6
 
-/-- Definition 6.3.1 -/
+/-- Definition 6.3.1 (supremum of a sequence) -/
 noncomputable abbrev Sequence.sup (a:Sequence) : EReal := sSup { x | ∃ n ≥ a.m, x = a n }
 
-/-- Definition 6.3.1 -/
+/-- Definition 6.3.1 (infimum of a sequence) -/
 noncomputable abbrev Sequence.inf (a:Sequence) : EReal := sInf { x | ∃ n ≥ a.m, x = a n }
 
 /-- Example 6.3.3 (a) -/
diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean
index 014649c87..2738ef128 100644
--- a/Analysis/Section_6_4.lean
+++ b/Analysis/Section_6_4.lean
@@ -201,19 +201,19 @@ theorem Sequence.tendsTo_iff_eq_limsup_liminf {a:Sequence} (c:ℝ) :
   a.TendsTo c ↔ a.liminf = c ∧ a.limsup = c := by
   sorry
 
-/-- Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4 -/
+/-- Lemma 6.4.13 (Comparison principle, sup) / Exercise 6.4.4 -/
 theorem Sequence.sup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
     a.sup ≤ b.sup := by sorry
 
-/-- Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4 -/
+/-- Lemma 6.4.13 (Comparison principle, inf) / Exercise 6.4.4 -/
 theorem Sequence.inf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
     a.inf ≤ b.inf := by sorry
 
-/-- Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4 -/
+/-- Lemma 6.4.13 (Comparison principle, limsup) / Exercise 6.4.4 -/
 theorem Sequence.limsup_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
     a.limsup ≤ b.limsup := by sorry
 
-/-- Lemma 6.4.13 (Comparison principle) / Exercise 6.4.4 -/
+/-- Lemma 6.4.13 (Comparison principle, liminf) / Exercise 6.4.4 -/
 theorem Sequence.liminf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, a n ≤ b n) :
     a.liminf ≤ b.liminf := by sorry
 
diff --git a/Analysis/Section_6_5.lean b/Analysis/Section_6_5.lean
index 262e75f96..314c65577 100644
--- a/Analysis/Section_6_5.lean
+++ b/Analysis/Section_6_5.lean
@@ -70,15 +70,15 @@ theorem Sequence.lim_of_power_decay {k:ℕ} :
     · simp
   simp [lim_eq, ha', eq_zero_of_pow_eq_zero hlim]
 
-/-- Lemma 6.5.2 / Exercise 6.5.2 -/
+/-- Lemma 6.5.2 (ratio of absolute value less than one) / Exercise 6.5.2 -/
 theorem Sequence.lim_of_geometric {x:ℝ} (hx: |x| < 1) : ((fun (n:ℕ) ↦ x^n):Sequence).TendsTo 0 := by
   sorry
 
-/-- Lemma 6.5.2 / Exercise 6.5.2 -/
+/-- Lemma 6.5.2 (ratio one) / Exercise 6.5.2 -/
 theorem Sequence.lim_of_geometric' {x:ℝ} (hx: x = 1) : ((fun (n:ℕ) ↦ x^n):Sequence).TendsTo 1 := by
   sorry
 
-/-- Lemma 6.5.2 / Exercise 6.5.2 -/
+/-- Lemma 6.5.2 (ratio minus one or of absolute value greater than one) / Exercise 6.5.2 -/
 theorem Sequence.lim_of_geometric'' {x:ℝ} (hx: x = -1 ∨ |x| > 1) :
     ((fun (n:ℕ) ↦ x^n):Sequence).Divergent := by
   sorry
diff --git a/Analysis/Section_6_6.lean b/Analysis/Section_6_6.lean
index ff4c3c79a..242026709 100644
--- a/Analysis/Section_6_6.lean
+++ b/Analysis/Section_6_6.lean
@@ -35,10 +35,10 @@ example :
     (fun n ↦ (10:ℝ)^(-(n:ℤ)-1)) := by
   sorry
 
-/-- Lemma 6.6.4 / Exercise 6.6.1 -/
+/-- Lemma 6.6.4 (reflexivity) / Exercise 6.6.1 -/
 theorem Sequence.subseq_self (a:ℕ → ℝ) : Sequence.subseq a a := by sorry
 
-/-- Lemma 6.6.4 / Exercise 6.6.1 -/
+/-- Lemma 6.6.4 (transitivity) / Exercise 6.6.1 -/
 theorem Sequence.subseq_trans {a b c:ℕ → ℝ} (hab: Sequence.subseq a b) (hbc: Sequence.subseq b c) :
     Sequence.subseq a c := by sorry
 
diff --git a/Analysis/Section_6_7.lean b/Analysis/Section_6_7.lean
index ff2b8d96c..e690a0e15 100644
--- a/Analysis/Section_6_7.lean
+++ b/Analysis/Section_6_7.lean
@@ -175,11 +175,11 @@ theorem Real.ratPow_neg {x:ℝ} (hx: x > 0) (q:ℝ) : rpow x (-q) = 1 / rpow x q
 theorem Real.ratPow_mono {x y:ℝ} (hx: x > 0) (hy: y > 0) {q:ℝ} (h: q > 0) : x > y ↔ rpow x q > rpow y q := by
   sorry
 
-/-- Proposition 6.7.3(e) / Exercise 6.7.1 -/
+/-- Proposition 6.7.3(e) (base greater than one) / Exercise 6.7.1 -/
 theorem Real.ratPow_mono_of_gt_one {x:ℝ} (hx: x > 1) {q r:ℝ} : rpow x q > rpow x r ↔ q > r := by
   sorry
 
-/-- Proposition 6.7.3(e) / Exercise 6.7.1 -/
+/-- Proposition 6.7.3(e) (base less than one) / Exercise 6.7.1 -/
 theorem Real.ratPow_mono_of_lt_one {x:ℝ} (hx0: 0 < x) (hx: x < 1) {q r:ℝ} : rpow x q > rpow x r ↔ q < r := by
   sorry