diff --git a/Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean b/Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean
index 3dc126fd80ccf7..e5ce11bde6ccaa 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean
@@ -12,7 +12,7 @@ public import Mathlib.Order.Filter.AtTopBot.Finset
 /-!
 # Infinite sum and products that converge uniformly
 
-# Main definitions
+## Main definitions
 - `HasProdUniformlyOn f g s` : `∏ i, f i b` converges uniformly on `s` to `g`.
 - `HasProdLocallyUniformlyOn f g s` : `∏ i, f i b` converges locally uniformly on `s` to `g`.
 - `HasProdUniformly f g` : `∏ i, f i b` converges uniformly to `g`.
diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean
index 5873e98710296f..d144b57a3c7670 100644
--- a/Mathlib/Topology/Bases.lean
+++ b/Mathlib/Topology/Bases.lean
@@ -45,7 +45,7 @@ conditions are equivalent in this case).
   the space.
 
 ## Implementation Notes
-For our applications we are interested that there exists a countable basis, but we do not need the
+For our applications we are interested in the existence of a countable basis, but we do not need the
 concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.
 
 ## TODO
diff --git a/Mathlib/Topology/EMetricSpace/PairReduction.lean b/Mathlib/Topology/EMetricSpace/PairReduction.lean
index 0a0d104f691aa3..d6497e5cdc934e 100644
--- a/Mathlib/Topology/EMetricSpace/PairReduction.lean
+++ b/Mathlib/Topology/EMetricSpace/PairReduction.lean
@@ -57,9 +57,9 @@ natural number `k` greater than zero such that `|{x ∈ V | d(t, x) ≤ kc}| ≤
 We construct a sequence `Vᵢ` of subsets of `J`, a sequence `tᵢ ∈ Vᵢ` and a sequence of `rᵢ : ℕ`
 inductively as follows (see `logSizeBallSeq`):
 
-* `V₀ = J`, `tₒ` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
-* `Vᵢ₊ᵢ = Vᵢ \ Bᵢ` where `Bᵢ := {x ∈ V | d(t, x) ≤ (rᵢ - 1) c}`, `tᵢ₊₁` is chosen arbitrarily in
-  `Vᵢ₊₁` (if it is nonempty), `rᵢ₊₁` is the log-size radius of `tᵢ₊₁` in `Vᵢ₊ᵢ`.
+* `V₀ = J`, `t₀` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
+* `Vᵢ₊₁ = Vᵢ \ Bᵢ` where `Bᵢ := {x ∈ V | d(t, x) ≤ (rᵢ - 1) c}`, `tᵢ₊₁` is chosen arbitrarily in
+  `Vᵢ₊₁` (if it is nonempty), `rᵢ₊₁` is the log-size radius of `tᵢ₊₁` in `Vᵢ₊₁`.
 
 Then `Vᵢ` is a strictly decreasing sequence (see `card_finset_logSizeBallSeq_add_one_lt`) until
 `Vᵢ` is empty. In particular `Vᵢ = ∅` for `i ≥ |J|`
@@ -176,9 +176,9 @@ def logSizeBallStruct.ball (struct : logSizeBallStruct T) (c : ℝ≥0∞) :
 variable [DecidableEq T]
 
 /-- We recursively define a log-size ball sequence `(Vᵢ, tᵢ, rᵢ)` by
-  * `V₀ = J`, `tₒ` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
-  * `Vᵢ₊ᵢ = Vᵢ \ {x ∈ V | d(t, x) ≤ (rᵢ - 1)c}`, `tᵢ₊₁` is chosen arbitrarily in `Vᵢ₊₁, rᵢ₊₁` is
-    the log-size radius of `tᵢ₊₁` in `Vᵢ₊ᵢ`. -/
+  * `V₀ = J`, `t₀` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
+  * `Vᵢ₊₁ = Vᵢ \ {x ∈ V | d(t, x) ≤ (rᵢ - 1)c}`, `tᵢ₊₁` is chosen arbitrarily in `Vᵢ₊₁`, `rᵢ₊₁` is
+    the log-size radius of `tᵢ₊₁` in `Vᵢ₊₁`. -/
 noncomputable
 def logSizeBallSeq (J : Finset T) (hJ : J.Nonempty) (a c : ℝ≥0∞) : ℕ → logSizeBallStruct T
   | 0 => {finset := J, point := hJ.choose, radius := logSizeRadius hJ.choose J a c}
diff --git a/Mathlib/Topology/Homotopy/HSpaces.lean b/Mathlib/Topology/Homotopy/HSpaces.lean
index 4fde8b7dc2f1cf..b90168462645fa 100644
--- a/Mathlib/Topology/Homotopy/HSpaces.lean
+++ b/Mathlib/Topology/Homotopy/HSpaces.lean
@@ -14,16 +14,16 @@ public import Mathlib.Topology.Path
 
 This file defines H-spaces mainly following the approach proposed by Serre in his paper
 *Homologie singulière des espaces fibrés*. The idea beneath `H-spaces` is that they are topological
-spaces with a binary operation `⋀ : X → X → X` that is a homotopic-theoretic weakening of an
-operation what would make `X` into a topological monoid.
-In particular, there exists a "neutral element" `e : X` such that `fun x ↦e ⋀ x` and
+spaces with a binary operation `⋀ : X → X → X` that is a homotopy-theoretic weakening of an
+operation that would make `X` into a topological monoid.
+In particular, there exists a "neutral element" `e : X` such that `fun x ↦ e ⋀ x` and
 `fun x ↦ x ⋀ e` are homotopic to the identity on `X`, see
 [the Wikipedia page of H-spaces](https://en.wikipedia.org/wiki/H-space).
 
 Some notable properties of `H-spaces` are
 * Their fundamental group is always abelian (by the same argument for topological groups);
 * Their cohomology ring comes equipped with a structure of a Hopf-algebra;
-* The loop space based at every `x : X` carries a structure of an `H-spaces`.
+* The loop space based at every `x : X` carries a structure of an `H-space`.
 
 ## Main Results
 
@@ -32,14 +32,14 @@ Some notable properties of `H-spaces` are
 * Given two `H-spaces` `X` and `Y`, their product is again an `H`-space. We show in an example that
   starting with two topological groups `G, G'`, the `H`-space structure on `G × G'` is
   definitionally equal to the product of `H-space` structures on `G` and `G'`.
-* The loop space based at every `x : X` carries a structure of an `H-spaces`.
+* The loop space based at every `x : X` carries a structure of an `H-space`.
 
 ## To Do
 * Prove that for every `NormedAddTorsor Z` and every `z : Z`, the operation
   `fun x y ↦ midpoint x y` defines an `H-space` structure with `z` as a "neutral element".
 * Prove that `S^0`, `S^1`, `S^3` and `S^7` are the unique spheres that are `H-spaces`, where the
   first three inherit the structure because they are topological groups (they are Lie groups,
-  actually), isomorphic to the invertible elements in `ℤ`, in `ℂ` and in the quaternion; and the
+  actually), isomorphic to the invertible elements in `ℤ`, in `ℂ` and in the quaternions; and the
   fourth from the fact that `S^7` coincides with the octonions of norm 1 (it is not a group, in
   particular, only has an instance of `MulOneClass`).
 
diff --git a/Mathlib/Topology/MetricSpace/Bounded.lean b/Mathlib/Topology/MetricSpace/Bounded.lean
index 7eb5e76f3719f6..2c98fdb1ea9832 100644
--- a/Mathlib/Topology/MetricSpace/Bounded.lean
+++ b/Mathlib/Topology/MetricSpace/Bounded.lean
@@ -336,7 +336,7 @@ theorem isBounded_Ioc (a b : α) : IsBounded (Ioc a b) :=
 theorem isBounded_Ioo (a b : α) : IsBounded (Ioo a b) :=
   (totallyBounded_Ioo a b).isBounded
 
-/-- In a pseudo metric space with a conditionally complete linear order such that the order and the
+/-- In a pseudometric space with a conditionally complete linear order such that the order and the
 metric structure give the same topology, any order-bounded set is metric-bounded. -/
 theorem isBounded_of_bddAbove_of_bddBelow {s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) :
     IsBounded s :=
diff --git a/Mathlib/Topology/MetricSpace/Gluing.lean b/Mathlib/Topology/MetricSpace/Gluing.lean
index 62a284a4dee032..18b15289e2bb75 100644
--- a/Mathlib/Topology/MetricSpace/Gluing.lean
+++ b/Mathlib/Topology/MetricSpace/Gluing.lean
@@ -450,7 +450,7 @@ variable {X : Type u} {Y : Type v} {Z : Type w}
 variable [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y}
   {ε : ℝ}
 
-/-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a pseudo metric space
+/-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a pseudometric space
 structure on `X ⊕ Y` by declaring that `Φ x` and `Ψ x` are at distance `0`. -/
 def gluePremetric (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : PseudoMetricSpace (X ⊕ Y) where
   dist := glueDist Φ Ψ 0
diff --git a/Mathlib/Topology/MetricSpace/PiNat.lean b/Mathlib/Topology/MetricSpace/PiNat.lean
index d0de2720eb7036..e10687a0bfc404 100644
--- a/Mathlib/Topology/MetricSpace/PiNat.lean
+++ b/Mathlib/Topology/MetricSpace/PiNat.lean
@@ -810,7 +810,7 @@ attribute [scoped instance] PiCountable.edist
 section PseudoEMetricSpace
 variable [∀ i, PseudoEMetricSpace (F i)]
 
-/-- Given a countable family of extended pseudo metric spaces,
+/-- Given a countable family of extended pseudometric spaces,
 one may put an extended distance on their product `Π i, E i`.
 
 It is highly non-canonical, though, and therefore not registered as a global instance.
diff --git a/Mathlib/Topology/MetricSpace/ProperSpace.lean b/Mathlib/Topology/MetricSpace/ProperSpace.lean
index c221ae71206835..92444b225d87a8 100644
--- a/Mathlib/Topology/MetricSpace/ProperSpace.lean
+++ b/Mathlib/Topology/MetricSpace/ProperSpace.lean
@@ -60,7 +60,7 @@ instance Metric.sphere.compactSpace {α : Type*} [PseudoMetricSpace α] [ProperS
 variable [PseudoMetricSpace α]
 
 -- see Note [lower instance priority]
-/-- A proper pseudo metric space is sigma compact, and therefore second countable. -/
+/-- A proper pseudometric space is sigma compact, and therefore second countable. -/
 instance (priority := 100) secondCountable_of_proper [ProperSpace α] :
     SecondCountableTopology α := by
   -- We already have `sigmaCompactSpace_of_locallyCompact_secondCountable`, so we don't
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean b/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
index fe677d64e105b7..30622e5842b45a 100644
--- a/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
+++ b/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
@@ -133,7 +133,7 @@ class PseudoMetricSpace (α : Type u) : Type u extends Dist α where
   cobounded_sets : (Bornology.cobounded α).sets =
     { s | ∃ C : ℝ, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C } := by intros; rfl
 
-/-- Two pseudo metric space structures with the same distance function coincide. -/
+/-- Two pseudometric space structures with the same distance function coincide. -/
 @[ext]
 theorem PseudoMetricSpace.ext {α : Type*} {m m' : PseudoMetricSpace α}
     (h : m.toDist = m'.toDist) : m = m' := by
@@ -990,7 +990,7 @@ example {α} [U : UniformSpace α] (m : PseudoMetricSpace α)
     (PseudoMetricSpace.replaceUniformity m H).toBornology = m.toBornology := by
   with_reducible_and_instances rfl
 
-/-- Build a new pseudo metric space from an old one where the bundled topological structure is
+/-- Build a new pseudometric space from an old one where the bundled topological structure is
 provably (but typically non-definitionaly) equal to some given topological structure.
 See Note [forgetful inheritance].
 See Note [reducible non-instances].
diff --git a/Mathlib/Topology/Metrizable/Basic.lean b/Mathlib/Topology/Metrizable/Basic.lean
index 4e30257c5734d7..e53fcd179f0b07 100644
--- a/Mathlib/Topology/Metrizable/Basic.lean
+++ b/Mathlib/Topology/Metrizable/Basic.lean
@@ -29,7 +29,7 @@ namespace TopologicalSpace
 variable {ι X Y : Type*} {A : ι → Type*} [TopologicalSpace X] [TopologicalSpace Y] [Finite ι]
   [∀ i, TopologicalSpace (A i)]
 
-/-- A topological space is *pseudo metrizable* if there exists a pseudo metric space structure
+/-- A topological space is *pseudometrizable* if there exists a pseudometric space structure
 compatible with the topology. To minimize imports, we implement this class in terms of the
 existence of a countably generated unifomity inducing the topology, which is mathematically
 equivalent.
@@ -41,7 +41,7 @@ class PseudoMetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop where
   exists_countably_generated :
     ∃ u : UniformSpace X, u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated
 
-/-- A uniform space with countably generated `𝓤 X` is pseudo metrizable. -/
+/-- A uniform space with countably generated `𝓤 X` is pseudometrizable. -/
 instance (priority := 100) _root_.UniformSpace.pseudoMetrizableSpace {X : Type*}
     [u : UniformSpace X] [hu : IsCountablyGenerated (uniformity X)] : PseudoMetrizableSpace X :=
   ⟨⟨u, rfl, hu⟩⟩
@@ -75,8 +75,8 @@ instance pseudoMetrizableSpace_prod [PseudoMetrizableSpace X] [PseudoMetrizableS
     pseudoMetrizableSpaceUniformity_countably_generated Y
   inferInstance
 
-/-- Given an inducing map of a topological space into a pseudo metrizable space, the source space
-is also pseudo metrizable. -/
+/-- Given an inducing map of a topological space into a pseudometrizable space, the source space
+is also pseudometrizable. -/
 theorem _root_.Topology.IsInducing.pseudoMetrizableSpace [PseudoMetrizableSpace Y] {f : X → Y}
     (hf : IsInducing f) : PseudoMetrizableSpace X :=
   let u : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
diff --git a/Mathlib/Topology/Metrizable/Uniformity.lean b/Mathlib/Topology/Metrizable/Uniformity.lean
index cd30d486df7e62..cfbe2e155dd54b 100644
--- a/Mathlib/Topology/Metrizable/Uniformity.lean
+++ b/Mathlib/Topology/Metrizable/Uniformity.lean
@@ -20,7 +20,7 @@ The proof follows [Sergey Melikhov, Metrizable uniform spaces][melikhov2011].
 ## Main definitions
 
 * `PseudoMetricSpace.ofPreNNDist`: given a function `d : X → X → ℝ≥0` such that `d x x = 0` and
-  `d x y = d y x` for all `x y : X`, constructs the maximal pseudo metric space structure such that
+  `d x y = d y x` for all `x y : X`, constructs the maximal pseudometric space structure such that
   `NNDist x y ≤ d x y` for all `x y : X`.
 
 * `UniformSpace.pseudoMetricSpace`: given a uniform space `X` with countably generated `𝓤 X`,
@@ -35,8 +35,8 @@ The proof follows [Sergey Melikhov, Metrizable uniform spaces][melikhov2011].
   then there exists a `PseudoMetricSpace` structure that is compatible with this `UniformSpace`
   structure. Use `UniformSpace.pseudoMetricSpace` or `UniformSpace.metricSpace` instead.
 
-* `UniformSpace.pseudoMetrizableSpace`: a uniform space with countably generated `𝓤 X` is pseudo
-  metrizable.
+* `UniformSpace.pseudoMetrizableSpace`: a uniform space with countably generated `𝓤 X` is
+  pseudometrizable.
 
 * `UniformSpace.metrizableSpace`: a T₀ uniform space with countably generated `𝓤 X` is
   metrizable. This is not an instance to avoid loops.
@@ -56,7 +56,7 @@ variable {X : Type*}
 
 namespace PseudoMetricSpace
 
-/-- The maximal pseudo metric space structure on `X` such that `dist x y ≤ d x y` for all `x y`,
+/-- The maximal pseudometric space structure on `X` such that `dist x y ≤ d x y` for all `x y`,
 where `d : X → X → ℝ≥0` is a function such that `d x x = 0` and `d x y = d y x` for all `x`, `y`. -/
 noncomputable def ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0)
     (dist_comm : ∀ x y, d x y = d y x) : PseudoMetricSpace X where
@@ -186,10 +186,10 @@ protected theorem UniformSpace.metrizable_uniformity (X : Type*) [UniformSpace X
     Define `d x y : ℝ≥0` to be `(1 / 2) ^ n`, where `n` is the minimal index of `U n` that
     separates `x` and `y`: `(x, y) ∉ U n`, or `0` if `x` is not separated from `y`. This function
     satisfies the assumptions of `PseudoMetricSpace.ofPreNNDist` and
-    `PseudoMetricSpace.le_two_mul_dist_ofPreNNDist`, hence the distance given by the former pseudo
-    metric space structure is Lipschitz equivalent to the `d`. Thus the uniformities generated by
-    `d` and `dist` are equal. Since the former uniformity is equal to `𝓤 X`, the latter is equal to
-    `𝓤 X` as well. -/
+    `PseudoMetricSpace.le_two_mul_dist_ofPreNNDist`, hence the distance given by the former
+    pseudometric space structure is Lipschitz equivalent to the `d`. Thus the uniformities generated
+    by `d` and `dist` are equal. Since the former uniformity is equal to `𝓤 X`, the latter is equal
+    to `𝓤 X` as well. -/
   obtain ⟨U, hU_symm, hU_comp, hB⟩ :
     ∃ U : ℕ → SetRel X X,
       (∀ n, (U n).IsSymm) ∧
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean b/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
index 56100e095a375a..50f1bd1961b4e0 100644
--- a/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
+++ b/Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean
@@ -127,7 +127,7 @@ theorem prod_symm_trans_prod
 end Prod
 
 /-!
-# Pi types
+## Pi types
 
 Finite indexed products of partial homeomorphisms
 -/
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean b/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean
index 1cefd7414ade09..24fdd583f6c144 100644
--- a/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean
+++ b/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean
@@ -269,7 +269,7 @@ theorem restr_source_inter (s : Set X) : e.restr (e.source ∩ s) = e.restr s :=
 end restrOpen
 
 /-!
-# ofSet
+## ofSet
 
 The identity on a set `s`
 -/
diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean
index 4b6aa243b78724..45eae18a0d1662 100644
--- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean
+++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean
@@ -12,13 +12,13 @@ public import Mathlib.Topology.UniformSpace.Equiv
 # Abstract theory of Hausdorff completions of uniform spaces
 
 This file characterizes Hausdorff completions of a uniform space α as complete Hausdorff spaces
-equipped with a map from α which has dense image and induce the original uniform structure on α.
+equipped with a map from α which has dense image and induces the original uniform structure on α.
 Assuming these properties we "extend" uniformly continuous maps from α to complete Hausdorff spaces
 to the completions of α. This is the universal property expected from a completion.
 It is then used to extend uniformly continuous maps from α to α' to maps between
 completions of α and α'.
 
-This file does not construct any such completion, it only study consequences of their existence.
+This file does not construct any such completion; it only studies consequences of their existence.
 The first advantage is that formal properties are clearly highlighted without interference from
 construction details. The second advantage is that this framework can then be used to compare
 different completion constructions. See `Topology/UniformSpace/CompareReals` for an example.