diff --git a/Analysis/Section_3_6.lean b/Analysis/Section_3_6.lean
index b5a171e1..b472310b 100644
--- a/Analysis/Section_3_6.lean
+++ b/Analysis/Section_3_6.lean
@@ -275,7 +275,7 @@ theorem SetTheory.Set.card_insert {X:Set} (hX: X.finite) {x:Object} (hx: x ∉ X
 theorem SetTheory.Set.card_union {X Y:Set} (hX: X.finite) (hY: Y.finite) :
     (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card := by sorry
 
-/-- Proposition 3.6.14 (b) / Exercise 3.6.4 -/
+/-- Proposition 3.6.14 (b') / Exercise 3.6.4 -/
 theorem SetTheory.Set.card_union_disjoint {X Y:Set} (hX: X.finite) (hY: Y.finite)
   (hdisj: Disjoint X Y) : (X ∪ Y).card = X.card + Y.card := by sorry
 
@@ -283,7 +283,7 @@ theorem SetTheory.Set.card_union_disjoint {X Y:Set} (hX: X.finite) (hY: Y.finite
 theorem SetTheory.Set.card_subset {X Y:Set} (hX: X.finite) (hY: Y ⊆ X) :
     Y.finite ∧ Y.card ≤ X.card := by sorry
 
-/-- Proposition 3.6.14 (c) / Exercise 3.6.4 -/
+/-- Proposition 3.6.14 (c') / Exercise 3.6.4 -/
 theorem SetTheory.Set.card_ssubset {X Y:Set} (hX: X.finite) (hY: Y ⊂ X) :
     Y.card < X.card := by sorry
 
@@ -291,7 +291,7 @@ theorem SetTheory.Set.card_ssubset {X Y:Set} (hX: X.finite) (hY: Y ⊂ X) :
 theorem SetTheory.Set.card_image {X Y:Set} (hX: X.finite) (f: X → Y) :
     (image f X).finite ∧ (image f X).card ≤ X.card := by sorry
 
-/-- Proposition 3.6.14 (d) / Exercise 3.6.4 -/
+/-- Proposition 3.6.14 (d') / Exercise 3.6.4 -/
 theorem SetTheory.Set.card_image_inj {X Y:Set} (hX: X.finite) {f: X → Y}
   (hf: Function.Injective f) : (image f X).card = X.card := by sorry
 
diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean
index 3a63507b..64c42e55 100644
--- a/Analysis/Section_4_4.lean
+++ b/Analysis/Section_4_4.lean
@@ -53,7 +53,7 @@ def Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) :
   -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
   sorry
 
-/-- Exercise 4.4.2 (b) -/
+/-- Exercise 4.4.2 (b') -/
 def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n, a (n+1) < a n) := by
   -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
   sorry
diff --git a/Analysis/Section_6_2.lean b/Analysis/Section_6_2.lean
index 1e4ea084..b55c98c5 100644
--- a/Analysis/Section_6_2.lean
+++ b/Analysis/Section_6_2.lean
@@ -80,13 +80,13 @@ theorem EReal.refl (x:EReal) : x ≤ x := by sorry
 /-- Proposition 6.2.5(b) / Exercise 6.2.1 -/
 theorem EReal.trichotomy (x y:EReal) : x < y ∨ x = y ∨ x > y := by sorry
 
-/-- Proposition 6.2.5(b) / Exercise 6.2.1 -/
+/-- Proposition 6.2.5(b') / Exercise 6.2.1 -/
 theorem EReal.not_lt_and_eq (x y:EReal) : ¬ (x < y ∧ x = y) := by sorry
 
-/-- Proposition 6.2.5(b) / Exercise 6.2.1 -/
+/-- Proposition 6.2.5(b'') / Exercise 6.2.1 -/
 theorem EReal.not_gt_and_eq (x y:EReal) : ¬ (x > y ∧ x = y) := by sorry
 
-/-- Proposition 6.2.5(b) / Exercise 6.2.1 -/
+/-- Proposition 6.2.5(b''') / Exercise 6.2.1 -/
 theorem EReal.not_lt_and_gt (x y:EReal) : ¬ (x < y ∧ x > y) := by sorry
 
 /-- Proposition 6.2.5(c) / Exercise 6.2.1 -/
@@ -164,7 +164,7 @@ example (E: Set EReal) : sSup E < sInf E ↔ E = ∅ := by sorry
 /-- Theorem 6.2.11 (a) / Exercise 6.2.2 -/
 theorem EReal.mem_le_sup (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sSup E := by sorry
 
-/-- Theorem 6.2.11 (a) / Exercise 6.2.2 -/
+/-- Theorem 6.2.11 (a') / Exercise 6.2.2 -/
 theorem EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : sInf E ≤ x := by sorry
 
 /-- Theorem 6.2.11 (b) / Exercise 6.2.2 -/
diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean
index f056b72d..0960398b 100644
--- a/Analysis/Section_6_4.lean
+++ b/Analysis/Section_6_4.lean
@@ -154,7 +154,7 @@ theorem Sequence.gt_limsup_bounds {a:Sequence} {x:EReal} (h: x > a.limsup) :
   convert lt_of_le_of_lt ((a.from N).le_sup hn') ha using 1
   grind
 
-/-- Proposition 6.4.12(a) -/
+/-- Proposition 6.4.12(a') -/
 theorem Sequence.lt_liminf_bounds {a:Sequence} {y:EReal} (h: y < a.liminf) :
     ∃ N ≥ a.m, ∀ n ≥ N, a n > y := by
   sorry
@@ -167,7 +167,7 @@ theorem Sequence.lt_limsup_bounds {a:Sequence} {x:EReal} (h: x < a.limsup) {N:
   choose n hn hxn _ using exists_between_lt_sup hx
   grind
 
-/-- Proposition 6.4.12(b) -/
+/-- Proposition 6.4.12(b') -/
 theorem Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N:ℤ} (hN: N ≥ a.m) :
     ∃ n ≥ N, a n < x := by
   sorry
@@ -175,10 +175,10 @@ theorem Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N:
 /-- Proposition 6.4.12(c) / Exercise 6.4.3 -/
 theorem Sequence.inf_le_liminf (a:Sequence) : a.inf ≤ a.liminf := by sorry
 
-/-- Proposition 6.4.12(c) / Exercise 6.4.3 -/
+/-- Proposition 6.4.12(c') / Exercise 6.4.3 -/
 theorem Sequence.liminf_le_limsup (a:Sequence) : a.liminf ≤ a.limsup := by sorry
 
-/-- Proposition 6.4.12(c) / Exercise 6.4.3 -/
+/-- Proposition 6.4.12(c'') / Exercise 6.4.3 -/
 theorem Sequence.limsup_le_sup (a:Sequence) : a.limsup ≤ a.sup := by sorry
 
 /-- Proposition 6.4.12(d) / Exercise 6.4.3 -/
@@ -191,7 +191,7 @@ theorem Sequence.limit_point_of_limsup {a:Sequence} {L_plus:ℝ} (h: a.limsup =
     a.LimitPoint L_plus := by
   sorry
 
-/-- Proposition 6.4.12(e) / Exercise 6.4.3 -/
+/-- Proposition 6.4.12(e') / Exercise 6.4.3 -/
 theorem Sequence.limit_point_of_liminf {a:Sequence} {L_minus:ℝ} (h: a.liminf = L_minus) :
     a.LimitPoint L_minus := by
   sorry