doc(Topology): fix more mathlib3 names in doc comments (#11948)

Mathlib/Topology/Algebra/InfiniteSum/Module.lean

@@ -211,7 +211,7 @@ noncomputable def MulAction.automorphize [Group α] [MulAction α β] (f : β 
   congr 1
   simp only [mul_smul]
 
-/-- Automorphization of a function into an `R`-`module` distributes, that is, commutes with the
+/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
 `R`-scalar multiplication. -/
 lemma MulAction.automorphize_smul_left [Group α] [MulAction α β] (f : β → M)
     (g : Quotient (MulAction.orbitRel α β) → R) :
@@ -230,7 +230,7 @@ lemma MulAction.automorphize_smul_left [Group α] [MulAction α β] (f : β →
   simp_rw [H₁]
   exact tsum_const_smul'' _
 
-/-- Automorphization of a function into an `R`-`module` distributes, that is, commutes with the
+/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
 `R`-scalar multiplication. -/
 lemma AddAction.automorphize_smul_left [AddGroup α] [AddAction α β]  (f : β → M)
     (g : Quotient (AddAction.orbitRel α β) → R) :
@@ -262,7 +262,7 @@ variable {G : Type*} [Group G] {Γ : Subgroup G}
   `g ↦ ∑' (γ : Γ), f(γ • g)`."]
 noncomputable def QuotientGroup.automorphize  (f : G → M) : G ⧸ Γ → M := MulAction.automorphize f
 
-/-- Automorphization of a function into an `R`-`module` distributes, that is, commutes with the
+/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
 `R`-scalar multiplication. -/
 lemma QuotientGroup.automorphize_smul_left (f : G → M) (g : G ⧸ Γ → R) :
     (QuotientGroup.automorphize ((g ∘ (@Quotient.mk' _ (_)) : G → R) • f) : G ⧸ Γ → M)
@@ -275,7 +275,7 @@ section
 
 variable {G : Type*} [AddGroup G] {Γ : AddSubgroup G}
 
-/-- Automorphization of a function into an `R`-`module` distributes, that is, commutes with the
+/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
 `R`-scalar multiplication. -/
 lemma QuotientAddGroup.automorphize_smul_left (f : G → M) (g : G ⧸ Γ → R) :
     QuotientAddGroup.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f)

Mathlib/Topology/Category/CompHaus/Projective.lean

@@ -19,7 +19,7 @@ In this file we show that `CompHaus` has enough projectives.
 Let `X` be a compact Hausdorff space.
 
 * `CompHaus.projective_ultrafilter`: the space `Ultrafilter X` is a projective object
-* `CompHaus.projective_presentation`: the natural map `Ultrafilter X → X`
+* `CompHaus.projectivePresentation`: the natural map `Ultrafilter X → X`
   is a projective presentation
 
 ## Reference

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -71,7 +71,7 @@ In this section we define the relevant projection maps and prove some compatibil
 ### Main definitions
 
 * Let `J : I → Prop`. Then `Proj J : (I → Bool) → (I → Bool)` is the projection mapping everything
-  that satisfies `J i` to itself, and everything else to `false`.
+  that satisfies `J i` to itself, and everything else to `False`.
 
 * The image of `C` under `Proj J` is denoted `π C J` and the corresponding map `C → π C J` is called
   `ProjRestrict`. If `J` implies `K` we have a map `ProjRestricts : π C K → π C J`.
@@ -83,7 +83,7 @@ In this section we define the relevant projection maps and prove some compatibil
 variable (J K L : I → Prop) [∀ i, Decidable (J i)] [∀ i, Decidable (K i)] [∀ i, Decidable (L i)]
 
 /--
-The projection mapping everything that satisfies `J i` to itself, and everything else to `false`
+The projection mapping everything that satisfies `J i` to itself, and everything else to `False`
 -/
 def Proj : (I → Bool) → (I → Bool) :=
   fun c i ↦ if J i then c i else false
@@ -1161,10 +1161,10 @@ variable {o : Ordinal} (hC : IsClosed C) (hsC : contained C (Order.succ o))
 
 section ExactSequence
 
-/-- The subset of `C` consisting of those elements whose `o`-th entry is `false`. -/
+/-- The subset of `C` consisting of those elements whose `o`-th entry is `False`. -/
 def C0 := C ∩ {f | f (term I ho) = false}
 
-/-- The subset of `C` consisting of those elements whose `o`-th entry is `true`. -/
+/-- The subset of `C` consisting of those elements whose `o`-th entry is `True`. -/
 def C1 := C ∩ {f | f (term I ho) = true}
 
 theorem isClosed_C0 : IsClosed (C0 C ho) := by
@@ -1198,7 +1198,7 @@ theorem contained_C' : contained (C' C ho) o := fun f hf i hi ↦ contained_C1 C
 
 variable (o)
 
-/-- Swapping the `o`-th coordinate to `true`. -/
+/-- Swapping the `o`-th coordinate to `True`. -/
 noncomputable
 def SwapTrue : (I → Bool) → I → Bool :=
   fun f i ↦ if ord I i = o then true else f i

Mathlib/Topology/Category/TopCommRingCat.lean

@@ -21,7 +21,7 @@ universe u
 
 open CategoryTheory
 
-set_option linter.uppercaseLean3 false -- `TopCommRing`
+set_option linter.uppercaseLean3 false -- `TopCommRingCat`
 
 /-- A bundled topological commutative ring. -/
 structure TopCommRingCat where

Mathlib/Topology/Compactness/Compact.lean

@@ -419,7 +419,7 @@ theorem IsCompact.mem_prod_nhdsSet_of_forall {K : Set Y} {l : Filter X} {s : Set
     (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y) : s ∈ l ×ˢ 𝓝ˢ K :=
   (hK.prod_nhdsSet_eq_biSup l).symm ▸ by simpa using hs
 
--- TODO: Is there a way to prove directly the `inf` version and then deduce the `prod` one ?
+-- TODO: Is there a way to prove directly the `inf` version and then deduce the `Prod` one ?
 -- That would seem a bit more natural.
 theorem IsCompact.nhdsSet_inf_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) :
     (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l := by

Mathlib/Topology/Homotopy/HSpaces.lean

@@ -48,7 +48,7 @@ particular, only has an instance of `MulOneClass`).
 * [J.-P. Serre, *Homologie singulière des espaces fibrés. Applications*,
   Ann. of Math (2) 1951, 54, 425–505][serre1951]
 -/
--- Porting note: `H_space` already contains an upper case letter
+-- Porting note: `HSpace` already contains an upper case letter
 set_option linter.uppercaseLean3 false
 universe u v
 

Mathlib/Topology/Separation.lean

@@ -49,7 +49,7 @@ This file defines the predicate `SeparatedNhds`, and common separation axioms
 
 * `IsClosed.exists_closed_singleton`: Given a closed set `S` in a compact T₀ space,
   there is some `x ∈ S` such that `{x}` is closed.
-* `exists_open_singleton_of_open_finite`: Given an open finite set `S` in a T₀ space,
+* `exists_isOpen_singleton_of_isOpen_finite`: Given an open finite set `S` in a T₀ space,
   there is some `x ∈ S` such that `{x}` is open.
 
 ### T₁ spaces

Mathlib/Topology/TietzeExtension.lean

@@ -502,7 +502,7 @@ attribute [deprecated] exists_extension_of_closedEmbedding -- deprecated since 2
 
 /-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
 `s` be a closed set in a normal topological space `Y`. Let `f` be a continuous real-valued function
-on `s`. Let `t` be a nonempty convex set of real numbers (we use `ord_connected` instead of `convex`
+on `s`. Let `t` be a nonempty convex set of real numbers (we use `ord_connected` instead of `Convex`
 to automatically deduce this argument by typeclass search) such that `f x ∈ t` for all `x : s`. Then
 there exists a continuous real-valued function `g : C(Y, ℝ)` such that `g y ∈ t` for all `y` and
 `g.restrict s = f`. -/

Mathlib/Topology/UniformSpace/Basic.lean

@@ -1667,7 +1667,7 @@ theorem uniformContinuous_sInf_dom₂ {α β γ} {f : α → β → γ} {uas : S
     (ha : ua ∈ uas) (hb : ub ∈ ubs) (hf : UniformContinuous fun p : α × β => f p.1 p.2) : by
       haveI := sInf uas; haveI := sInf ubs;
         exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2 := by
-  -- proof essentially copied from `continuous_Inf_dom`
+  -- proof essentially copied from `continuous_sInf_dom`
   let _ : UniformSpace (α × β) := instUniformSpaceProd
   have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
   have hb := uniformContinuous_sInf_dom hb uniformContinuous_id