diff --git a/Analysis/Section_2_1.lean b/Analysis/Section_2_1.lean
index 1472acab1..fd9ea507b 100644
--- a/Analysis/Section_2_1.lean
+++ b/Analysis/Section_2_1.lean
@@ -137,7 +137,7 @@ theorem Nat.recurse_zero (f: Nat → Nat → Nat) (c: Nat) : Nat.recurse f c 0 =
 theorem Nat.recurse_succ (f: Nat → Nat → Nat) (c: Nat) (n: Nat) :
     recurse f c (n++) = f n (recurse f c n) := by rfl
 
-/-- Proposition 2.1.16 (recursive definitions). -/
+/-- Proposition 2.1.16 (recursive definitions, existence). -/
 theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) :
     (a 0 = c ∧ ∀ n, a (n++) = f n (a n)) ↔ a = recurse f c := by
   constructor
@@ -154,7 +154,7 @@ theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) :
   exact recurse_succ _ _
 
 
-/-- Proposition 2.1.16 (recursive definitions). -/
+/-- Proposition 2.1.16 (recursive definitions, uniqueness). -/
 theorem Nat.recurse_uniq (f: Nat → Nat → Nat) (c: Nat) :
     ∃! (a: Nat → Nat), a 0 = c ∧ ∀ n, a (n++) = f n (a n) := by
   apply ExistsUnique.intro (recurse f c)
diff --git a/Analysis/Section_2_3.lean b/Analysis/Section_2_3.lean
index 51017219c..06fd6e2c6 100644
--- a/Analysis/Section_2_3.lean
+++ b/Analysis/Section_2_3.lean
@@ -136,7 +136,7 @@ theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.IsPos) : a *
   rw [lt_iff_add_pos]
   use d*c
 
-/-- Proposition 2.3.6 (Multiplication preserves order) -/
+/-- Proposition 2.3.6 (Multiplication preserves order, on the right) -/
 theorem Nat.mul_gt_mul_of_pos_right {a b c: Nat} (h: a > b) (hc: c.IsPos) :
     a * c > b * c := mul_lt_mul_of_pos_right h hc
 
@@ -146,7 +146,7 @@ theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.IsPos) : c * a
   simp [mul_comm]
   exact mul_lt_mul_of_pos_right h hc
 
-/-- Proposition 2.3.6 (Multiplication preserves order) -/
+/-- Proposition 2.3.6 (Multiplication preserves order, on the left) -/
 theorem Nat.mul_gt_mul_of_pos_left {a b c: Nat} (h: a > b) (hc: c.IsPos) :
     c * a > c * b := mul_lt_mul_of_pos_left h hc
 
@@ -195,7 +195,7 @@ Compare with Mathlib's {name}`Nat.pow_zero` -/
 @[simp]
 theorem Nat.pow_zero (m: Nat) : m ^ (0:Nat) = 1 := recurse_zero (fun _ prod ↦ prod * m) _
 
-/-- Definition 2.3.11 (Exponentiation for natural numbers) -/
+/-- Definition 2.3.11 (Exponentiation for natural numbers, successor) -/
 @[simp]
 theorem Nat.zero_pow_zero : (0:Nat) ^ 0 = 1 := recurse_zero (fun _ prod ↦ prod * 0) _
 
diff --git a/Analysis/Section_5_1.lean b/Analysis/Section_5_1.lean
index 1f34c614b..bbe889a54 100644
--- a/Analysis/Section_5_1.lean
+++ b/Analysis/Section_5_1.lean
@@ -299,12 +299,12 @@ lemma Sequence.IsCauchy.mk {n₀:ℤ} (a: {n // n ≥ n₀} → ℚ) :
 noncomputable def Sequence.sqrt_two : Sequence := (fun n:ℕ ↦ ((⌊ (Real.sqrt 2)*10^n ⌋ / 10^n):ℚ))
 
 /--
-  Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)
+  Example 5.1.10 (a). (This requires extensive familiarity with Mathlib's API for the real numbers.)
 -/
 theorem Sequence.ex_5_1_10_a : (1:ℚ).Steady sqrt_two := by sorry
 
 /--
-  Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)
+  Example 5.1.10 (b). (This requires extensive familiarity with Mathlib's API for the real numbers.)
 -/
 theorem Sequence.ex_5_1_10_b : (0.1:ℚ).Steady (sqrt_two.from 1) := by sorry
 
@@ -354,12 +354,12 @@ lemma boundedBy_def {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : BoundedBy a M ↔ ∀ i
 
 abbrev Sequence.BoundedBy (a:Sequence) (M:ℚ) : Prop := ∀ n, |a n| ≤ M
 
-/-- Definition 5.1.12 (bounded sequences) -/
+/-- Definition 5.1.12 (bounded sequences, bounded by a given constant) -/
 lemma Sequence.boundedBy_def (a:Sequence) (M:ℚ) : a.BoundedBy M ↔ ∀ n, |a n| ≤ M := by rfl
 
 abbrev Sequence.IsBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M
 
-/-- Definition 5.1.12 (bounded sequences) -/
+/-- Definition 5.1.12 (bounded sequences, bounded) -/
 lemma Sequence.isBounded_def (a:Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M := by rfl
 
 /-- Example 5.1.13 (a) -/
diff --git a/Analysis/Section_5_2.lean b/Analysis/Section_5_2.lean
index df10bff3f..2c042c013 100644
--- a/Analysis/Section_5_2.lean
+++ b/Analysis/Section_5_2.lean
@@ -46,11 +46,11 @@ example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence) := by sorr
 /-- Example 5.2.2 (c) -/
 example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence) := by sorry
 
-/-- Definition 5.2.3 (Eventually ε-close sequences) -/
+/-- Definition 5.2.3 (Eventually ε-close sequences, unfolded) -/
 lemma Rat.eventuallyClose_def (ε: ℚ) (a b: Sequence) :
     ε.EventuallyClose a b ↔ ∃ N, ε.CloseSeq (a.from N) (b.from N) := by rfl
 
-/-- Definition 5.2.3 (Eventually ε-close sequences) -/
+/-- Definition 5.2.3 (Eventually ε-close sequences, in terms of the terms) -/
 lemma Rat.eventuallyClose_iff (ε: ℚ) (a b: ℕ → ℚ) :
     ε.EventuallyClose (a:Sequence) (b:Sequence) ↔ ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := by sorry
 
@@ -68,11 +68,11 @@ example : (0.01:ℚ).EventuallyClose ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Se
 abbrev Sequence.Equiv (a b: ℕ → ℚ) : Prop :=
   ∀ ε > (0:ℚ), ε.EventuallyClose (a:Sequence) (b:Sequence)
 
-/-- Definition 5.2.6 (Equivalent sequences) -/
+/-- Definition 5.2.6 (Equivalent sequences, unfolded) -/
 lemma Sequence.equiv_def (a b: ℕ → ℚ) :
     Equiv a b ↔ ∀ (ε:ℚ), ε > 0 → ε.EventuallyClose (a:Sequence) (b:Sequence) := by rfl
 
-/-- Definition 5.2.6 (Equivalent sequences) -/
+/-- Definition 5.2.6 (Equivalent sequences, in terms of the terms) -/
 lemma Sequence.equiv_iff (a b: ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := by
   sorry
 
diff --git a/Analysis/Section_5_5.lean b/Analysis/Section_5_5.lean
index 2861a06a8..fbcd4b5d7 100644
--- a/Analysis/Section_5_5.lean
+++ b/Analysis/Section_5_5.lean
@@ -32,10 +32,10 @@ theorem Real.upperBound_def (E: Set Real) (M: Real) : M ∈ upperBounds E ↔ 
 theorem Real.lowerBound_def (E: Set Real) (M: Real) : M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M :=
   mem_lowerBounds
 
-/-- API for Example 5.5.2 -/
+/-- API for Example 5.5.2 (the interval) -/
 theorem Real.Icc_def (x y:Real) : .Icc x y = { z | x ≤ z ∧ z ≤ y } := rfl
 
-/-- API for Example 5.5.2 -/
+/-- API for Example 5.5.2 (membership) -/
 theorem Real.mem_Icc (x y z:Real) : z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y := by simp [Real.Icc_def]
 
 /-- Example 5.5.2 -/
diff --git a/Analysis/Section_9_3.lean b/Analysis/Section_9_3.lean
index 2e8af602c..a65697835 100644
--- a/Analysis/Section_9_3.lean
+++ b/Analysis/Section_9_3.lean
@@ -49,19 +49,19 @@ Slight change from the book to accomodate the change to {lean}`Real.CloseFn`
 -/
 example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry
 
-/-- Example 9.3.4 -/
+/-- Example 9.3.4 (not close on the whole interval) -/
 example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by
   sorry
 
-/-- Example 9.3.4 -/
+/-- Example 9.3.4 (close near the point) -/
 example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := by
   sorry
 
-/-- Example 9.3.5 -/
+/-- Example 9.3.5 (not close on the whole interval) -/
 example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := by
   sorry
 
-/-- Example 9.3.5 -/
+/-- Example 9.3.5 (close near the point) -/
 example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := by
   sorry