diff --git a/analysis/Analysis/Section_2_2.lean b/analysis/Analysis/Section_2_2.lean
index 03f9c990..af094ab9 100644
--- a/analysis/Analysis/Section_2_2.lean
+++ b/analysis/Analysis/Section_2_2.lean
@@ -186,6 +186,7 @@ instance Nat.instLE : LE Nat where
 instance Nat.instLT : LT Nat where
   lt n m := n ≤ m ∧ n ≠ m
 
+/-- Compare with Mathlib's `le_iff_exists_add`. -/
 lemma Nat.le_iff (n m:Nat) : n ≤ m ↔ ∃ a:Nat, m = n + a := by rfl
 
 lemma Nat.lt_iff (n m:Nat) : n < m ↔ (∃ a:Nat, m = n + a) ∧ n ≠ m := by rfl
diff --git a/analysis/Analysis/Section_2_epilogue.lean b/analysis/Analysis/Section_2_epilogue.lean
index a7414952..844eb33e 100644
--- a/analysis/Analysis/Section_2_epilogue.lean
+++ b/analysis/Analysis/Section_2_epilogue.lean
@@ -118,7 +118,7 @@ abbrev natCast (P : PeanoAxioms) : ℕ → P.Nat := fun n ↦ match n with
   | Nat.succ n => P.succ (natCast P n)
 
 /-- One can start the proof here with `unfold Function.Injective`, although it is not strictly necessary. -/
-theorem natCast_injective (P : PeanoAxioms) : Function.Injective P.natCast  := by
+theorem natCast_injective (P : PeanoAxioms) : Function.Injective P.natCast := by
   sorry
 
 /-- One can start the proof here with `unfold Function.Surjective`, although it is not strictly necessary. -/
diff --git a/analysis/Analysis/Section_3_1.lean b/analysis/Analysis/Section_3_1.lean
index cd9355cc..95e686b2 100644
--- a/analysis/Analysis/Section_3_1.lean
+++ b/analysis/Analysis/Section_3_1.lean
@@ -449,7 +449,7 @@ theorem SetTheory.Set.specification_axiom'' {A:Set} (P: A → Prop) (x:Object) :
 
 theorem SetTheory.Set.specify_subset {A:Set} (P: A → Prop) : A.specify P ⊆ A := by sorry
 
-/-- This exercise may require some understanding of how  subtypes are implemented in Lean. -/
+/-- This exercise may require some understanding of how subtypes are implemented in Lean. -/
 theorem SetTheory.Set.specify_congr {A A':Set} (hAA':A = A') {P: A → Prop} {P': A' → Prop}
   (hPP': (x:Object) → (h:x ∈ A) → (h':x ∈ A') → P ⟨ x, h⟩ ↔ P' ⟨ x, h'⟩ ) :
     A.specify P = A'.specify P' := by sorry
diff --git a/analysis/Analysis/Section_3_3.lean b/analysis/Analysis/Section_3_3.lean
index 096b095c..37ecc3d1 100644
--- a/analysis/Analysis/Section_3_3.lean
+++ b/analysis/Analysis/Section_3_3.lean
@@ -490,10 +490,10 @@ theorem Function.inverse_bijective {X Y: Set} {f: Function X Y} (h: f.bijective)
 theorem Function.inverse_inverse {X Y: Set} {f: Function X Y} (h: f.bijective) :
     (f.inverse h).inverse (f.inverse_bijective h) = f := by sorry
 
+/-- Exercise 3.3.7 -/
 theorem Function.comp_bijective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.bijective)
   (hg: g.bijective) : (g ○ f).bijective := by sorry
 
-/-- Exercise 3.3.7 -/
 theorem Function.inv_of_comp {X Y Z:Set} {f: Function X Y} {g : Function Y Z}
   (hf: f.bijective) (hg: g.bijective) :
     (g ○ f).inverse (Function.comp_bijective hf hg) = (f.inverse hf) ○ (g.inverse hg) := by sorry