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