diff --git a/Analysis/MeasureTheory/Section_1_4_2.lean b/Analysis/MeasureTheory/Section_1_4_2.lean
index 6a7339b2..a4e024cd 100644
--- a/Analysis/MeasureTheory/Section_1_4_2.lean
+++ b/Analysis/MeasureTheory/Section_1_4_2.lean
@@ -154,7 +154,7 @@ theorem BorelSigmaAlgebra.generated_by_boxes (d:ℕ) : BorelSigmaAlgebra (Euclid
 theorem BorelSigmaAlgebra.generated_by_elementary (d:ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by { E : Set (EuclideanSpace' d) | IsElementary E }  := by sorry
 
 open Ordinal in
-/-- Exercise 1.4.15 (Recursive definition of generated sigma-algebra)-/
+/-- Exercise 1.4.15 (Recursive definition of generated sigma-algebra). -/
 def ConcreteSigmaAlgebra.generated_by_eq {X:Type*} (F: Set (Set X)) :
   (ConcreteSigmaAlgebra.generated_by F).measurableSets =
   ⋃ α < ω₁,
@@ -181,7 +181,7 @@ theorem BorelSigmaAlgebra.prod {d₁ d₂:ℕ} {E : Set (EuclideanSpace' d₁)}
   :=
   by sorry
 
-/-- Exercise 1.4.18(i) -/
+/-- Exercise 1.4.18(i) (slice along first factor). -/
 theorem BorelSigmaAlgebra.slice_fst {d₁ d₂:ℕ} {E : Set (EuclideanSpace' (d₁+d₂))}
   (hE: (BorelSigmaAlgebra (EuclideanSpace' (d₁+d₂))).measurable E)
   (x₂ : EuclideanSpace' d₂ ) :
@@ -189,7 +189,7 @@ theorem BorelSigmaAlgebra.slice_fst {d₁ d₂:ℕ} {E : Set (EuclideanSpace' (d
   :=
   by sorry
 
-/-- Exercise 1.4.18(i) -/
+/-- Exercise 1.4.18(i) (slice along second factor). -/
 theorem BorelSigmaAlgebra.slice_snd {d₁ d₂:ℕ} {E : Set (EuclideanSpace' (d₁+d₂))}
   (hE: (BorelSigmaAlgebra (EuclideanSpace' (d₁+d₂))).measurable E)
   (x₁ : EuclideanSpace' d₁ ) :