fix: insert missing space before Verso docstring closers

Analysis/Appendix_A_4.lean

@@ -51,7 +51,7 @@ example : ∀ (x:ℝ), (x+1)^2 = x^2 + 2*x + 1 := by
 
 end VariableExample2
 
-/-- A dummy statement is in place here for this example.-/
+/-- A dummy statement is in place here for this example. -/
 example : 0 = 0 := by
   set x := 342
   have : x + 155 = 497 := by

Analysis/MeasureTheory/Section_1_2_2.lean

@@ -355,7 +355,7 @@ theorem IsClosed.measurable {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: IsClosed E
 
 abbrev IsNull {d:ℕ} (E: Set (EuclideanSpace' d)) : Prop := Lebesgue_outer_measure E = 0
 
-/-- Lemma 1.2.13(iii) (Every null set is Lebesgue measurable).-/
+/-- Lemma 1.2.13(iii) (Every null set is Lebesgue measurable). -/
 theorem IsNull.measurable {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: IsNull E) : LebesgueMeasurable E := by
   -- Strategy: For any ε > 0, since m*(E) = 0, get a box cover with total volume < ε,
   -- then inflate boxes to open sets. The union is open and contains E.
@@ -518,7 +518,7 @@ lemma IsNull.subset {d:ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsNull E) (hFE
   rw [hE] at this
   exact le_antisymm this (Lebesgue_outer_measure.nonneg F)
 
-/-- Lemma 1.2.13(iv) (Empty set is measurable).-/
+/-- Lemma 1.2.13(iv) (Empty set is measurable). -/
 theorem LebesgueMeasurable.empty {d:ℕ} : LebesgueMeasurable (∅: Set (EuclideanSpace' d)) :=
 -- use (i) directly
   IsOpen.measurable isOpen_empty
@@ -536,7 +536,7 @@ theorem LebesgueMeasurable.empty' {d:ℕ} : LebesgueMeasurable (∅: Set (Euclid
     rw [Lebesgue_outer_measure.of_empty d]
     exact le_of_lt hε
 
-/-- Lemma 1.2.13(vi) (Countable union of measurable sets is measurable).-/
+/-- Lemma 1.2.13(vi) (Countable union of measurable sets is measurable). -/
 theorem LebesgueMeasurable.countable_union {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) : LebesgueMeasurable (⋃ n, E n) := by
   -- Use the ε/2^n trick: let ε > 0 be arbitrary
   intro ε hε
@@ -901,7 +901,7 @@ lemma LebesgueMeasurable.closedBall {d : ℕ} (c : EuclideanSpace' d) (r : ℝ)
     LebesgueMeasurable (Metric.closedBall c r) :=
   Metric.isClosed_closedBall.measurable
 
-/-- Exercise 1.2.7 (Criteria for measurability)-/
+/-- Exercise 1.2.7 (Criteria for measurability) -/
 theorem LebesgueMeasurable.TFAE {d:ℕ} (E: Set (EuclideanSpace' d)) :
     [
       LebesgueMeasurable E,
@@ -932,7 +932,7 @@ theorem CantorSet.uncountable : Uncountable CantorSet := by
 
 theorem CantorSet.null : IsNull (Real.equiv_EuclideanSpace' '' CantorSet) := by sorry
 
-/-- Exercise 1.2.10 (\[0,1) is not the countable union of pairwise disjoint closed intervals)-/
+/-- Exercise 1.2.10 (\[0,1) is not the countable union of pairwise disjoint closed intervals) -/
 example : ¬ ∃ (I: ℕ → BoundedInterval), (∀ n, IsClosed (I n).toSet) ∧ (Set.univ.PairwiseDisjoint (fun n ↦ (I n).toSet) ) ∧ (⋃ n, (I n).toSet = Set.Ico 0 1) := by
   sorry
 
@@ -1636,15 +1636,15 @@ theorem Lebesgue_measure.union {d:ℕ} {E F: Set (EuclideanSpace' d)} (hE: Lebes
   rw [tsum_fintype]
   simp only [S, Fin.sum_univ_two, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one]
 
-/-- Exercise 1.2.11(a) (Upward monotone convergence)-/
+/-- Exercise 1.2.11(a) (Upward monotone convergence) -/
 theorem Lebesgue_measure.upward_monotone_convergence {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) (hmono: ∀ n, E n ⊆ E (n + 1)) : Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure (⋃ n, E n))) := by
   sorry
 
-/-- Exercise 1.2.11(b) (Downward monotone convergence)-/
+/-- Exercise 1.2.11(b) (Downward monotone convergence) -/
 theorem Lebesgue_measure.downward_monotone_convergence {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) (hmono: ∀ n, E (n+1) ⊆ E n) (hfin: ∃ n, Lebesgue_measure (E n) < ⊤) : Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure (⋂ n, E n))) := by
   sorry
 
-/-- Exercise 1.2.11 (c) (counterexample)-/
+/-- Exercise 1.2.11 (c) (counterexample) -/
 example : ∃ (d:ℕ) (E: ℕ → Set (EuclideanSpace' d)) (hE: ∀ n, LebesgueMeasurable (E n)) (hmono: ∀ n, E (n+1) ⊆ E n), ¬ Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure (⋂ n, E n))) := by sorry
 
 /-- Exercise 1.2.12(a) -/
@@ -1679,11 +1679,11 @@ example : ∃ (d:ℕ) (E: ℕ → Set (EuclideanSpace' d)) (E₀ F: Set (Euclide
 /-- Exercise 1.2.14 -/
 example {d:ℕ} (E: Set (EuclideanSpace' d)) : ∃ (F: Set (EuclideanSpace' d)), E ⊆ F ∧ LebesgueMeasurable F ∧ Lebesgue_measure F = Lebesgue_outer_measure E := by sorry
 
-/-- Exercise 1.2.15 (Inner regularity)-/
+/-- Exercise 1.2.15 (Inner regularity) -/
 theorem Lebesgue_measure.eq {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E): Lebesgue_measure E = sSup { M | ∃ K, K ⊆ E ∧ IsCompact K ∧ M = Lebesgue_measure K} := by
   sorry
 
-/-- Exercise 1.2.16 (Criteria for finite measure)-/
+/-- Exercise 1.2.16 (Criteria for finite measure) -/
 theorem LebesgueMeasurable.finite_TFAE {d:ℕ} (E: Set (EuclideanSpace' d)) :
     [
       LebesgueMeasurable E ∧ Lebesgue_measure E < ⊤,
@@ -1698,7 +1698,7 @@ theorem LebesgueMeasurable.finite_TFAE {d:ℕ} (E: Set (EuclideanSpace' d)) :
     ].TFAE
   := by sorry
 
-/-- Exercise 1.2.17 (Caratheodory criterion one direction)-/
+/-- Exercise 1.2.17 (Caratheodory criterion one direction) -/
 theorem LebesgueMeasurable.caratheodory {d:ℕ} (E: Set (EuclideanSpace' d)) :
     [
       LebesgueMeasurable E,
@@ -1711,17 +1711,17 @@ theorem Bornology.IsBounded.inElementary {d:ℕ} {E: Set (EuclideanSpace' d)} (h
 
 noncomputable def inner_measure {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E) : ℝ := (Lebesgue_measure hE.inElementary.choose).toReal - (Lebesgue_measure (hE.inElementary.choose \ E)).toReal
 
-/-- Exercise 1.2.18(i) (Inner measure)-/
+/-- Exercise 1.2.18(i) (Inner measure) -/
 theorem inner_measure.eq {d:ℕ} {E A: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E)
   (hA: IsElementary A) (hsub: E ⊆ A) : inner_measure hE = Lebesgue_measure A - Lebesgue_outer_measure (A \ E) := by
   sorry
 
-/-- Exercise 1.2.18(ii) (Inner measure)-/
+/-- Exercise 1.2.18(ii) (Inner measure) -/
 theorem inner_measure.le {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E)
   : inner_measure hE ≤ Lebesgue_outer_measure E := by
   sorry
 
-/-- Exercise 1.2.18(iii) (Inner measure)-/
+/-- Exercise 1.2.18(iii) (Inner measure) -/
 theorem inner_measure.eq_iff {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E)
   : inner_measure hE = Lebesgue_outer_measure E ↔ LebesgueMeasurable E := by
   sorry
@@ -1780,7 +1780,7 @@ theorem Lebesgue_measure.unique {d:ℕ} (m: Set (EuclideanSpace' d) → EReal)
   (hnorm: m (Box.unit_cube d) = 1)
   : ∀ E, LebesgueMeasurable E → m E = Lebesgue_measure E := by sorry
 
-/-- Exercise 1.2.24(i) (Lebesgue measure as the completion of elementary measure)-/
+/-- Exercise 1.2.24(i) (Lebesgue measure as the completion of elementary measure) -/
 instance IsElementary.ae_equiv {d:ℕ} {A: Set (EuclideanSpace' d)} (hA: IsElementary A):
 Setoid (Set A) := {
    r E F := IsNull (Subtype.val '' (_root_.symmDiff E F))
@@ -1817,7 +1817,7 @@ noncomputable def IsElementary.ae_measure {d:ℕ} {A: Set (EuclideanSpace' d)} (
 
 noncomputable def IsElementary.ae_elem_measure {d:ℕ} {A: Set (EuclideanSpace' d)} (hA: IsElementary A) (E: hA.ae_elem) : ℝ := E.property.choose_spec.1.measure
 
-/-- Exercise 1.2.24(iv) (Lebesgue measure as the completion of elementary measure)-/
+/-- Exercise 1.2.24(iv) (Lebesgue measure as the completion of elementary measure) -/
 theorem IsElementary.ae_measure_eq_completion {d:ℕ} {A: Set (EuclideanSpace' d)} (hA: IsElementary A) (m: hA.ae_subsets → ℝ) :
 ContinuousOn m hA.ae_measurable ∧ (∀ (E:hA.ae_elem), m E.val = hA.ae_elem_measure E)
 ↔ (∀ (E:hA.ae_measurable), m E.val = hA.ae_measure E) := by sorry

Analysis/MeasureTheory/Section_1_3_4.lean

@@ -1024,7 +1024,7 @@ theorem RiemannIntegrableOn.realAbsolutelyIntegrable {I: BoundedInterval} {f: 
 theorem RiemannIntegral.eq_integ {I: BoundedInterval} {f: ℝ → ℝ} (hf: RiemannIntegrableOn f I) :
     riemannIntegral f I  = hf.realAbsolutelyIntegrable.integ := by sorry
 
-/-- Exercise 1.3.21 (Absolute summability is a special case of absolute integrability)-/
+/-- Exercise 1.3.21 (Absolute summability is a special case of absolute integrability) -/
 theorem AbsolutelySummable.realAbsolutelyIntegrable_iff {a: ℤ → ℝ} : ∑' n, |a n|.toEReal < ⊤ ↔ RealAbsolutelyIntegrable (fun x ↦ a ⌊EuclideanSpace'.equiv_Real x⌋) := by sorry
 
 theorem AbsolutelySummable.complexAbsolutelyIntegrable_iff {a: ℤ → ℂ} : ∑' n, ‖a n‖.toEReal < ⊤ ↔ ComplexAbsolutelyIntegrable (fun x ↦ a ⌊EuclideanSpace'.equiv_Real x⌋) := by sorry

Analysis/Misc/UnitsSystem.lean

@@ -300,7 +300,7 @@ theorem Scalar.toFormal_hMul {d₁ d₂:Dimensions} (q₁:Scalar d₁) (q₂:Sca
 not to do this, implementing an inversion relation instead. -/
 noncomputable def Scalar.pow {d:Dimensions} (q: Scalar d) (n:ℕ) : Scalar (n • d) := ⟨ q.val^n ⟩
 
-/-- {given -show}`n : ℕ, d` One cannot use the Mathlib classes {name}`Pow` or {name}`HPow` here because the output type {lean}`Scalar (n • d)` depends on the input {name}`n`.  As the symbol {kw (of := «term_^_»)}`^` is reserved for such classes, we use the symbol `**` instead.-/
+/-- {given -show}`n : ℕ, d` One cannot use the Mathlib classes {name}`Pow` or {name}`HPow` here because the output type {lean}`Scalar (n • d)` depends on the input {name}`n`.  As the symbol {kw (of := «term_^_»)}`^` is reserved for such classes, we use the symbol `**` instead. -/
 infix:80 "**" => Scalar.pow
 
 @[simp]
@@ -346,7 +346,7 @@ theorem Scalar.mul_inv {d₁ d₂:Dimensions} (q₁:Scalar d₁) (q₂:Scalar d
 theorem Scalar.pow_inv {d:Dimensions} (q:Scalar d) (n:ℕ) : (q ** n).inv = (q.inv ** n).cast := by
   simp [←toFormal_inj, toFormal]
 
-/-- Multiplication and inversion combine to give division in the usual fashion.-/
+/-- Multiplication and inversion combine to give division in the usual fashion. -/
 noncomputable instance Scalar.instHDiv {d₁ d₂:Dimensions} : HDiv (Scalar d₁) (Scalar d₂) (Scalar (d₁ - d₂)) where
   hDiv q₁ q₂ := ⟨q₁.val / q₂.val⟩
 

Analysis/Misc/UnitsSystemExamples.lean

@@ -27,6 +27,6 @@ theorem UnitsSystem.Scalar.right_distrib {d₁ d₂:Dimensions} (a b:Scalar d₁
 theorem UnitsSystem.Scalar.sq_add {d:Dimensions} (a b:Scalar d) : (a+b)**2 = a**2 + (2 • a * b).cast + b**2 := by
   simp [←toFormal_inj]; ring
 
-/-- An alternate proof based on working in coordinates-/
+/-- An alternate proof based on working in coordinates -/
 theorem UnitsSystem.Scalar.sq_add' {d:Dimensions} (a b:Scalar d) : (a+b)**2 = a**2 + (2 • a * b).cast + b**2 := by
   simp [←val_inj]; ring

Analysis/Misc/erdos_379.lean

@@ -12,7 +12,7 @@ theorem binom_eq {n k:ℕ} (hk: 1 ≤ k) : (n.choose k) * k = ((n-1).choose (k-1
     all_goals omega
   simp [choose_eq_zero_of_lt hn, choose_eq_zero_iff]; omega
 
-/-- $$`\binom\{n\}\{k\} \cdot k \cdot (k-1) = \binom\{n-2\}\{k-2\} \cdot (n-1) \cdot n`.-/
+/-- $$`\binom\{n\}\{k\} \cdot k \cdot (k-1) = \binom\{n-2\}\{k-2\} \cdot (n-1) \cdot n`. -/
 theorem binom_eq_2 {n k:ℕ} (hk: 2 ≤ k) : (n.choose k) * k * (k-1) = ((n-2).choose (k-2)) * (n-1) * n := calc
   _ = ((n-1).choose (k-1)) * n * (k-1) := by rw [binom_eq]; omega
   _ = ((n-1).choose (k-1)) * (k-1) * n := by ring
@@ -35,7 +35,7 @@ theorem lemma_2 {n k p r:ℕ} (hk: 2 ≤ k) (hn: k ≤ n)
   replace h3 : ¬p∣k-1 := by contrapose! h3; convert dvd_sub h1' h3 using 1; omega
   exact hp.prime.pow_dvd_of_dvd_mul_right _ h2 (hp.prime.pow_dvd_of_dvd_mul_right _ h3 h1)
 
-/-- If $$`n=2^\{\phi(p^R)\}$$ and $$p>2^\{r-1\}$$, then $$2^r \mid \binom\{n\}\{k\}$$ or $$p^R \mid \binom\{n\}\{k\}`.-/
+/-- If $$`n=2^\{\phi(p^R)\}$$ and $$p>2^\{r-1\}$$, then $$2^r \mid \binom\{n\}\{k\}$$ or $$p^R \mid \binom\{n\}\{k\}`. -/
 theorem key_prop {k n p r R:ℕ} (hn: n = 2^((p^R).totient))
   (hk: 1 ≤ k) (hkn: k < n) (hp: p.Prime) (hpr: p > 2^(r-1))
   (hr: 1 < r) (hr' : r ≤ (p^R).totient):
@@ -71,7 +71,7 @@ theorem S_ge {n r:ℕ} (hn: 1 < n) (h: ∀ k ∈ Finset.Ico 1 n, ∃ p, p.Prime
     all_goals grind
   aesop
 
-/-- If $$p>2^\{r-1\}$$, then $$S(2^\{\phi(p^R)\}) \ge r$$.-/
+/-- If $$p>2^\{r-1\}$$, then $$S(2^\{\phi(p^R)\}) \ge r$$. -/
 theorem key_cor {p r:ℕ} (hp: p.Prime) (hpr: p > 2^(r-1)) (hr: 1 < r) :
   r ≤ S (2^((p^r).totient)) := by
   apply S_ge; simp; grind
@@ -86,7 +86,7 @@ theorem key_cor {p r:ℕ} (hp: p.Prime) (hpr: p > 2^(r-1)) (hr: 1 < r) :
   . use 2; simp_all [prime_two]
   use p
 
-/-- A positive resolution to Erdos problem \#379.-/
+/-- A positive resolution to Erdos problem \#379. -/
 theorem erdos_379 : Filter.atTop.limsup (fun n ↦ (S n:ENat)) = ⊤ := by
   rw [Filter.limsup_eq_iInf_iSup_of_nat]
   simp; intro N; rw [iSup₂_eq_top]; intro r hr; lift r to ℕ using (by order)

Analysis/Section_10_5.lean

@@ -20,7 +20,7 @@ Main constructions and results of this section:
 open Chapter9
 namespace Chapter10
 
-/-- Proposition 10.5.1 (L'Hôpital's rule, I) / Exercise 10.5.1-/
+/-- Proposition 10.5.1 (L'Hôpital's rule, I) / Exercise 10.5.1 -/
 theorem _root_.Filter.Tendsto.of_div {X: Set ℝ} {f g: ℝ → ℝ} {x₀ f'x₀ g'x₀:ℝ}
   (hfx₀: f x₀ = 0) (hgx₀: g x₀ = 0) (hg_non: g'x₀ ≠ 0)
   (hf'x₀: HasDerivWithinAt f f'x₀ X x₀) (hg'x₀: HasDerivWithinAt g g'x₀ X x₀) :

Analysis/Section_11_1.lean

@@ -26,7 +26,7 @@ inductive BoundedInterval where
 
 open BoundedInterval
 
-/-- There is a technical issue in that this coercion is not injective: the empty set is represented by multiple bounded intervals.  This causes some of the statements in this section to be a little uglier than necessary.-/
+/-- There is a technical issue in that this coercion is not injective: the empty set is represented by multiple bounded intervals.  This causes some of the statements in this section to be a little uglier than necessary. -/
 @[coe]
 def BoundedInterval.toSet (I: BoundedInterval) : Set ℝ := match I with
   | Ioo a b => .Ioo a b

Analysis/Section_11_10.lean

@@ -125,7 +125,7 @@ theorem RS_integ_eq_integ_of_mul_deriv
     upper_integral (f * α') (Icc a b) := lower_integral_le_upper hfα'_bound
   refine ⟨ ⟨ hfα'_bound, ?_ ⟩, ?_ ⟩ <;> linarith
 
-/-- Lemma 11.10.5 / Exercise 11.10.2-/
+/-- Lemma 11.10.5 / Exercise 11.10.2 -/
 theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ → ℝ}
   (hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hf: PiecewiseConstantOn f (Icc (φ a) (φ b))) :
   PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ =
@@ -218,7 +218,7 @@ theorem integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ}
  have h2 := RS_integ_eq_integ_of_mul_deriv hab hφ_mono hφ_diff hφ_cont hφ' h1.1
  refine ⟨ h2.1, by aesop ⟩
 
-/-- Exercise 11.10.3-/
+/-- Exercise 11.10.3 -/
 example {a b:ℝ} (hab: a < b) {f: ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) :
   IntegrableOn (fun x ↦ f (-x)) (Icc (-b) (-a)) ∧
   integ (fun x ↦ f (-x)) (Icc (-b) (-a)) = integ f (Icc a b) := by

Analysis/Section_11_4.lean

@@ -144,7 +144,7 @@ theorem IntegrableOn.max {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableO
 
 
 
-/-- Theorem 11.4.5 / Exercise 11.4.3.  The objective here is to create a shorter proof than the one above.-/
+/-- Theorem 11.4.5 / Exercise 11.4.3.  The objective here is to create a shorter proof than the one above. -/
 theorem IntegrableOn.min {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I) :
   IntegrableOn (f ⊓ g) I  := by
   sorry

Analysis/Section_11_5.lean

@@ -89,7 +89,7 @@ example : ¬ IntegrableOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry
 
 open PiecewiseConstantOn ConstantOn in
 set_option maxHeartbeats 300000 in
-/-- Proposition 11.5.3-/
+/-- Proposition 11.5.3 -/
 theorem integ_of_bdd_cts {I: BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I)
   (hf: ContinuousOn f I) : IntegrableOn f I := by
   -- This proof is written to follow the structure of the original text.

Analysis/Section_2_1.lean

@@ -63,7 +63,7 @@ lemma Nat.zero_succ : 0++ = 1 := by rfl
 lemma Nat.one_succ : 1++ = 2 := by rfl
 #check (2:Nat)
 
-/-- Proposition 2.1.4 (3 is a natural number)-/
+/-- Proposition 2.1.4 (3 is a natural number) -/
 lemma Nat.two_succ : 2++ = 3 := by rfl
 #check (3:Nat)
 

Analysis/Section_2_2.lean

@@ -126,7 +126,7 @@ instance Nat.addCommMonoid : AddCommMonoid Nat where
     textbook. -/
 example (a b c d:Nat) : (a+b)+(c+0+d) = (b+c)+(d+a) := by abel
 
-/-- Definition 2.2.7 (Positive natural numbers).-/
+/-- Definition 2.2.7 (Positive natural numbers). -/
 def Nat.IsPos (n:Nat) : Prop := n ≠ 0
 
 theorem Nat.isPos_iff (n:Nat) : n.IsPos ↔ n ≠ 0 := by rfl
@@ -269,7 +269,7 @@ theorem Nat.lt_iff_succ_le (a b:Nat) : a < b ↔ a++ ≤ b := by
 theorem Nat.lt_iff_add_pos (a b:Nat) : a < b ↔ ∃ d:Nat, d.IsPos ∧ b = a + d := by
   sorry
 
-/-- If a < b then a ̸= b,-/
+/-- If a < b then a ̸= b, -/
 theorem Nat.ne_of_lt (a b:Nat) : a < b → a ≠ b := by
   intro h; exact h.2
 

Analysis/Section_2_3.lean

@@ -209,7 +209,7 @@ theorem Nat.pow_succ (m n: Nat) : (m:Nat) ^ n++ = m^n * m :=
 theorem Nat.pow_one (m: Nat) : m ^ (1:Nat) = m := by
   rw [←zero_succ, pow_succ]; simp
 
-/-- Exercise 2.3.4-/
+/-- Exercise 2.3.4 -/
 theorem Nat.sq_add_eq (a b: Nat) :
     (a + b) ^ (2 : Nat) = a ^ (2 : Nat) + 2 * a * b + b ^ (2 : Nat) := by
   sorry

Analysis/Section_2_epilogue.lean

@@ -170,7 +170,7 @@ theorem Equiv.uniq {P Q : PeanoAxioms} (equiv1 equiv2 : PeanoAxioms.Equiv P Q) :
   ext n
   sorry
 
-/-- A sample result: recursion is well-defined on any structure obeying the Peano axioms-/
+/-- A sample result: recursion is well-defined on any structure obeying the Peano axioms -/
 theorem Nat.recurse_uniq {P : PeanoAxioms} (f: P.Nat → P.Nat → P.Nat) (c: P.Nat) :
     ∃! (a: P.Nat → P.Nat), a P.zero = c ∧ ∀ n, a (P.succ n) = f n (a n) := by
   sorry

Analysis/Section_3_1.lean

@@ -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. -/
 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. -/
 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. -/
 theorem SetTheory.Set.subset_diff_subset_counter :
     ∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A' \ B') ⊆ (A \ B) := by sorry
 
@@ -869,7 +869,7 @@ theorem SetTheory.Set.coe_subtype (X: Set) :  (X : _root_.Set Object) = X.toSubt
 theorem SetTheory.Set.coe_intersection (X Y: Set) :
     ((X ∩ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) ∩ (Y : _root_.Set Object) := by sorry
 
-/-- Compatibility of set difference-/
+/-- Compatibility of set difference -/
 theorem SetTheory.Set.coe_diff (X Y: Set) :
     ((X \ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) \ (Y : _root_.Set Object) := by sorry
 

Analysis/Section_3_5.lean

@@ -472,7 +472,7 @@ theorem SetTheory.Set.direct_sum {X Y Z:Set} (f: Z → X) (g: Z → Y) :
 theorem SetTheory.Set.iProd_empty_iff {n:ℕ} {X: Fin n → Set} :
     iProd X = ∅ ↔ ∃ i, X i = ∅ := by sorry
 
-/-- Exercise 3.5.9-/
+/-- Exercise 3.5.9 -/
 theorem SetTheory.Set.iUnion_inter_iUnion {I J: Set} (A: I → Set) (B: J → Set) :
     (iUnion I A) ∩ (iUnion J B) = iUnion (I ×ˢ J) (fun p ↦ (A (fst p)) ∩ (B (snd p))) := by sorry
 

Analysis/Section_4_3.lean

@@ -173,12 +173,12 @@ theorem close_mul_mul' {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z
     (ε*|z|+δ*|y|).Close (x * z) (y * w) := by
     sorry
 
-/-- Definition 4.3.9 (exponentiation).  Here we use the Mathlib definition.-/
+/-- Definition 4.3.9 (exponentiation).  Here we use the Mathlib definition. -/
 lemma pow_zero (x:ℚ) : x^0 = 1 := _root_.pow_zero x
 
 example : (0:ℚ)^0 = 1 := pow_zero 0
 
-/-- Definition 4.3.9 (exponentiation).  Here we use the Mathlib definition.-/
+/-- Definition 4.3.9 (exponentiation).  Here we use the Mathlib definition. -/
 lemma pow_succ (x:ℚ) (n:ℕ) : x^(n+1) = x^n * x := _root_.pow_succ x n
 
 /-- Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3 -/