From bde52bbccef85ce782154d28de088d77948df214 Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Sat, 15 Aug 2026 09:08:55 +0530
Subject: [PATCH] fix: disambiguate duplicate Verso labels across Chapter 3

Thirty docstrings in Sections 3.1-3.5 shared a label with a sibling
declaration, including Exercise 3.1.2, Lemma 3.1.12, Proposition 3.1.17,
Axiom 3.6, Exercise 3.1.12, Exercises 3.2.2/3.2.3, Exercises 3.4.5/3.4.10/
3.4.11 and Definition 3.5.6.

Each now names what it covers while keeping the statement number.  The stray
full stop in "Exercise 3.1.12." goes at the same time, so the three labels
match the numbering used everywhere else in the file.
---
 Analysis/Section_3_1.lean | 34 +++++++++++++++++-----------------
 Analysis/Section_3_2.lean |  8 ++++----
 Analysis/Section_3_4.lean | 14 +++++++-------
 Analysis/Section_3_5.lean |  4 ++--
 4 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/Analysis/Section_3_1.lean b/Analysis/Section_3_1.lean
index bd2570860..211f4ce0c 100644
--- a/Analysis/Section_3_1.lean
+++ b/Analysis/Section_3_1.lean
@@ -253,14 +253,14 @@ abbrev SetTheory.Set.empty : Set := ∅
 abbrev SetTheory.Set.singleton_empty : Set := {(empty: Object)}
 abbrev SetTheory.Set.pair_empty : Set := {(empty: Object), (singleton_empty: Object)}
 
-/-- Exercise 3.1.2 -/
+/-- Exercise 3.1.2 (empty set is not a singleton) -/
 theorem SetTheory.Set.emptyset_neq_singleton : empty ≠ singleton_empty := by
   sorry
 
-/-- Exercise 3.1.2 -/
+/-- Exercise 3.1.2 (empty set is not a pair) -/
 theorem SetTheory.Set.emptyset_neq_pair : empty ≠ pair_empty := by sorry
 
-/-- Exercise 3.1.2 -/
+/-- Exercise 3.1.2 (singleton is not a pair) -/
 theorem SetTheory.Set.singleton_empty_neq_pair : singleton_empty ≠ pair_empty := by
   sorry
 
@@ -276,15 +276,15 @@ theorem SetTheory.Set.union_congr_left (A A' B:Set) (h: A = A') : A ∪ B = A' 
 -/
 theorem SetTheory.Set.union_congr_right (A B B':Set) (h: B = B') : A ∪ B = A ∪ B' := by sorry
 
-/-- Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 -/
+/-- Lemma 3.1.12 (Basic properties of unions, singletons) / Exercise 3.1.3 -/
 theorem SetTheory.Set.singleton_union_singleton (a b:Object) :
     ({a}:Set) ∪ ({b}:Set) = {a,b} := by
   sorry
 
-/-- Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 -/
+/-- Lemma 3.1.12 (Basic properties of unions, commutativity) / Exercise 3.1.3 -/
 theorem SetTheory.Set.union_comm (A B:Set) : A ∪ B = B ∪ A := by sorry
 
-/-- Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 -/
+/-- Lemma 3.1.12 (Basic properties of unions, associativity) / Exercise 3.1.3 -/
 theorem SetTheory.Set.union_assoc (A B C:Set) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := by
   -- this proof is written to follow the structure of the original text.
   ext x
@@ -347,15 +347,15 @@ theorem SetTheory.Set.ssubset_def (X Y:Set) : X ⊂ Y ↔ (X ⊆ Y ∧ X ≠ Y)
 /-- Remark 3.1.15 -/
 theorem SetTheory.Set.subset_congr_left {A A' B:Set} (hAA':A = A') (hAB: A ⊆ B) : A' ⊆ B := by sorry
 
-/-- Examples 3.1.16 -/
+/-- Examples 3.1.16 (reflexivity) -/
 @[simp, refl]
 theorem SetTheory.Set.subset_self (A:Set) : A ⊆ A := by sorry
 
-/-- Examples 3.1.16 -/
+/-- Examples 3.1.16 (the empty set is a subset) -/
 @[simp]
 theorem SetTheory.Set.empty_subset (A:Set) : ∅ ⊆ A := by sorry
 
-/-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
+/-- Proposition 3.1.17 (Partial ordering by set inclusion, transitivity) -/
 theorem SetTheory.Set.subset_trans {A B C:Set} (hAB:A ⊆ B) (hBC:B ⊆ C) : A ⊆ C := by
   -- This proof is written to follow the structure of the original text.
   rw [subset_def]
@@ -365,11 +365,11 @@ theorem SetTheory.Set.subset_trans {A B C:Set} (hAB:A ⊆ B) (hBC:B ⊆ C) : A 
   apply hBC x at hx
   assumption
 
-/-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
+/-- Proposition 3.1.17 (Partial ordering by set inclusion, antisymmetry) -/
 theorem SetTheory.Set.subset_antisymm (A B:Set) (hAB:A ⊆ B) (hBA:B ⊆ A) : A = B := by
   sorry
 
-/-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
+/-- Proposition 3.1.17 (Partial ordering by set inclusion, strict transitivity) -/
 theorem SetTheory.Set.ssubset_trans (A B C:Set) (hAB:A ⊂ B) (hBC:B ⊂ C) : A ⊂ C := by
   sorry
 
@@ -425,17 +425,17 @@ lemma SetTheory.Set.subtype_mk_coe {A:Set} {x:Object} (hx:x ∈ A) : A.subtype_m
 
 abbrev SetTheory.Set.specify (A:Set) (P: A → Prop) : Set := SetTheory.specify A P
 
-/-- Axiom 3.6 (axiom of specification) -/
+/-- Axiom 3.6 (axiom of specification, membership) -/
 theorem SetTheory.Set.specification_axiom {A:Set} {P: A → Prop} {x:Object} (h: x ∈ A.specify P) :
     x ∈ A :=
   (SetTheory.specification_axiom A P).1 x h
 
-/-- Axiom 3.6 (axiom of specification) -/
+/-- Axiom 3.6 (axiom of specification, the property holds) -/
 theorem SetTheory.Set.specification_axiom' {A:Set} (P: A → Prop) (x:A) :
     x.val ∈ A.specify P ↔ P x :=
   (SetTheory.specification_axiom A P).2 x
 
-/-- Axiom 3.6 (axiom of specification) -/
+/-- Axiom 3.6 (axiom of specification, the specified set is a subset) -/
 @[simp]
 theorem SetTheory.Set.specification_axiom'' {A:Set} (P: A → Prop) (x:Object) :
     x ∈ A.specify P ↔ ∃ h:x ∈ A, P ⟨ x, h ⟩ := by
@@ -793,15 +793,15 @@ theorem SetTheory.Set.union_eq_partition (A B:Set) : A ∪ B = (A \ B) ∪ (A 
 theorem SetTheory.Set.specification_from_replacement {A:Set} {P: A → Prop} :
     ∃ B, B ⊆ A ∧ ∀ x, x.val ∈ B ↔ P x := by sorry
 
-/-- Exercise 3.1.12. -/
+/-- Exercise 3.1.12 (unions) -/
 theorem SetTheory.Set.subset_union_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
     A' ∪ B' ⊆ A ∪ B := by sorry
 
-/-- Exercise 3.1.12. -/
+/-- Exercise 3.1.12 (intersections) -/
 theorem SetTheory.Set.subset_inter_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
     A' ∩ B' ⊆ A ∩ B := by sorry
 
-/-- Exercise 3.1.12. -/
+/-- Exercise 3.1.12 (differences: a counterexample) -/
 theorem SetTheory.Set.subset_diff_subset_counter :
     ∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A' \ B') ⊆ (A \ B) := by sorry
 
diff --git a/Analysis/Section_3_2.lean b/Analysis/Section_3_2.lean
index cc1cc28ea..069383161 100644
--- a/Analysis/Section_3_2.lean
+++ b/Analysis/Section_3_2.lean
@@ -110,17 +110,17 @@ theorem SetTheory.Set.replace_exists (h: axiom_of_universal_specification) (A:Se
     ∃ (Z:Set), ∀ y, y ∈ Z ↔ ∃ a : A, P a y := by
   sorry
 
-/-- Exercise 3.2.2 -/
+/-- Exercise 3.2.2 (no set contains itself) -/
 theorem SetTheory.Set.not_mem_self (A:Set) : (A:Object) ∉ A := by sorry
 
-/-- Exercise 3.2.2 -/
+/-- Exercise 3.2.2 (no two sets contain each other) -/
 theorem SetTheory.Set.not_mem_mem (A B:Set) : (A:Object) ∉ B ∨ (B:Object) ∉ A := by sorry
 
-/-- Exercise 3.2.3 -/
+/-- Exercise 3.2.3 (universal specification) -/
 theorem SetTheory.Set.univ_iff : axiom_of_universal_specification ↔
   ∃ (U:Set), ∀ x, x ∈ U := by sorry
 
-/-- Exercise 3.2.3 -/
+/-- Exercise 3.2.3 (there is no universal set) -/
 theorem SetTheory.Set.no_univ : ¬ ∃ (U:Set), ∀ (x:Object), x ∈ U := by sorry
 
 
diff --git a/Analysis/Section_3_4.lean b/Analysis/Section_3_4.lean
index e27e95fa1..9a546c698 100644
--- a/Analysis/Section_3_4.lean
+++ b/Analysis/Section_3_4.lean
@@ -309,11 +309,11 @@ theorem SetTheory.Set.preimage_of_union {X Y:Set} (f:X → Y) (A B: Set) :
 theorem SetTheory.Set.preimage_of_diff {X Y:Set} (f:X → Y) (A B: Set) :
     preimage f (A \ B) = (preimage f A) \ (preimage f B)  := by sorry
 
-/-- Exercise 3.4.5 -/
+/-- Exercise 3.4.5 (image of a preimage) -/
 theorem SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) :
     (∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := by sorry
 
-/-- Exercise 3.4.5 -/
+/-- Exercise 3.4.5 (preimage of an image) -/
 theorem SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) :
     (∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by sorry
 
@@ -344,26 +344,26 @@ theorem SetTheory.Set.union_pair_exists (X Y:Set) : ∃ Z:Set, ∀ x, x ∈ Z 
 theorem SetTheory.Set.iInter'_insensitive {I:Set} (β β':I) (A: I → Set) :
     iInter' I β A = iInter' I β' A := by sorry
 
-/-- Exercise 3.4.10 -/
+/-- Exercise 3.4.10 (union over a union of index sets) -/
 theorem SetTheory.Set.union_iUnion {I J:Set} (A: (I ∪ J:Set) → Set) :
     iUnion I (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
     ∪ iUnion J (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
     = iUnion (I ∪ J) A := by sorry
 
-/-- Exercise 3.4.10 -/
+/-- Exercise 3.4.10 (a union of nonempty index sets is nonempty) -/
 theorem SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := by sorry
 
-/-- Exercise 3.4.10 -/
+/-- Exercise 3.4.10 (intersection over a union of index sets) -/
 theorem SetTheory.Set.inter_iInter {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) (A: (I ∪ J:Set) → Set) :
     iInter I hI (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
     ∩ iInter J hJ (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
     = iInter (I ∪ J) (union_of_nonempty hI hJ) A := by sorry
 
-/-- Exercise 3.4.11 -/
+/-- Exercise 3.4.11 (complement of a union) -/
 theorem SetTheory.Set.compl_iUnion {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
     X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := by sorry
 
-/-- Exercise 3.4.11 -/
+/-- Exercise 3.4.11 (complement of an intersection) -/
 theorem SetTheory.Set.compl_iInter {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
     X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := by sorry
 
diff --git a/Analysis/Section_3_5.lean b/Analysis/Section_3_5.lean
index 12ea3aa57..bbadf63aa 100644
--- a/Analysis/Section_3_5.lean
+++ b/Analysis/Section_3_5.lean
@@ -171,11 +171,11 @@ noncomputable abbrev SetTheory.Set.curry_equiv {X Y Z:Set} : (X → Y → Z) ≃
 abbrev SetTheory.Set.tuple {I:Set} {X: I → Set} (x: ∀ i, X i) : Object :=
   ((fun i ↦ ⟨ x i, by rw [mem_iUnion]; use i; exact (x i).property ⟩):I → iUnion I X)
 
-/-- Definition 3.5.6 -/
+/-- Definition 3.5.6 (indexed product) -/
 abbrev SetTheory.Set.iProd {I: Set} (X: I → Set) : Set :=
   ((iUnion I X)^I).specify (fun t ↦ ∃ x : ∀ i, X i, t = tuple x)
 
-/-- Definition 3.5.6 -/
+/-- Definition 3.5.6 (membership in an indexed product) -/
 theorem SetTheory.Set.mem_iProd {I: Set} {X: I → Set} (t:Object) :
     t ∈ iProd X ↔ ∃ x: ∀ i, X i, t = tuple x := by
   simp only [iProd, specification_axiom'']; constructor