diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean b/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
index 0e43c28af0e901..7d5edfc81f0a1c 100644
--- a/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
+++ b/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
@@ -754,7 +754,7 @@ theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃φ₁ φ₂ :
     (hs : s.EqOn φ₁ φ₂) : φ₁ = φ₂ :=
   ext fun _x => adjoin_le_equalizer φ₁ φ₂ hs <| h.symm ▸ trivial
 
-/-- Two algebra morphisms are equal on `Algebra.span s`iff they are equal on s -/
+/-- Two algebra morphisms are equal on `Algebra.span s` iff they are equal on `s`. -/
 theorem eqOn_adjoin_iff {φ ψ : A →ₐ[R] B} {s : Set A} :
     Set.EqOn φ ψ (adjoin R s) ↔ Set.EqOn φ ψ s := by
   have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.rfl
diff --git a/Mathlib/Algebra/Homology/Embedding/Connect.lean b/Mathlib/Algebra/Homology/Embedding/Connect.lean
index dfb240beb4d0ff..7c32acb0ac0995 100644
--- a/Mathlib/Algebra/Homology/Embedding/Connect.lean
+++ b/Mathlib/Algebra/Homology/Embedding/Connect.lean
@@ -177,7 +177,7 @@ noncomputable def homologyIsoPos (n : ℕ) [NeZero n] (m : ℤ) (hm : m = n)
       (by simp; cutsat) (by simp; cutsat) (by simp) (by simp)).symm ≪≫
     HomologicalComplex.homologyMapIso h.restrictionGEIso n
 
-/-- Given `h : ConnectData K L` and `n : ℕ`non-zero, the homology
+/-- Given `h : ConnectData K L` and `n : ℕ` non-zero, the homology
 of `h.cochainComplex` in degree `-(n + 1)` identifies to the homology of `K` in degree `n`. -/
 noncomputable def homologyIsoNeg (n : ℕ) [NeZero n] (m : ℤ) (hm : m = -(n + 1 : ℕ))
     [h.cochainComplex.HasHomology m] [K.HasHomology n] :
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
index fb58ff5d4587ad..045ca85fc1eb7e 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
@@ -183,7 +183,7 @@ theorem ContDiffAt.add {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDi
     ContDiffAt 𝕜 n (fun x => f x + g x) x := by
   rw [← contDiffWithinAt_univ] at *; exact hf.add hg
 
-/-- The sum of two `C^n`functions is `C^n`. -/
+/-- The sum of two `C^n` functions is `C^n`. -/
 @[fun_prop]
 theorem ContDiff.add {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
     ContDiff 𝕜 n fun x => f x + g x :=
@@ -264,7 +264,7 @@ theorem ContDiffWithinAt.neg {s : Set E} {f : E → F} (hf : ContDiffWithinAt 
 theorem ContDiffAt.neg {f : E → F} (hf : ContDiffAt 𝕜 n f x) :
     ContDiffAt 𝕜 n (fun x => -f x) x := by rw [← contDiffWithinAt_univ] at *; exact hf.neg
 
-/-- The negative of a `C^n`function is `C^n`. -/
+/-- The negative of a `C^n` function is `C^n`. -/
 @[fun_prop]
 theorem ContDiff.neg {f : E → F} (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => -f x :=
   contDiff_neg.comp hf
@@ -409,7 +409,7 @@ nonrec theorem ContDiffAt.mul {f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (h
 theorem ContDiffOn.mul {f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
     ContDiffOn 𝕜 n (fun x => f x * g x) s := fun x hx => (hf x hx).mul (hg x hx)
 
-/-- The product of two `C^n`functions is `C^n`. -/
+/-- The product of two `C^n` functions is `C^n`. -/
 @[fun_prop]
 theorem ContDiff.mul {f g : E → 𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
     ContDiff 𝕜 n fun x => f x * g x :=
diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
index 700838fb33d910..26122c9b9c7da8 100644
--- a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
+++ b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
@@ -46,7 +46,7 @@ linear maps are continuous. Moreover, a finite-dimensional subspace is always co
 The fact that all norms are equivalent is not written explicitly, as it would mean having two norms
 on a single space, which is not the way type classes work. However, if one has a
 finite-dimensional vector space `E` with a norm, and a copy `E'` of this type with another norm,
-then the identities from `E` to `E'` and from `E'`to `E` are continuous thanks to
+then the identities from `E` to `E'` and from `E'` to `E` are continuous thanks to
 `LinearMap.continuous_of_finiteDimensional`. This gives the desired norm equivalence.
 -/
 
diff --git a/Mathlib/Analysis/RCLike/Inner.lean b/Mathlib/Analysis/RCLike/Inner.lean
index 884407b3dd4ede..dca9a3f8d98164 100644
--- a/Mathlib/Analysis/RCLike/Inner.lean
+++ b/Mathlib/Analysis/RCLike/Inner.lean
@@ -18,7 +18,7 @@ from `RCLike.innerProductSpace`.
 
 * Build a non-instance `InnerProductSpace` from `wInner`.
 * `cWeight` is a poor name. Can we find better? It doesn't hugely matter for typing, since it's
-  hidden behind the `⟪f, g⟫ₙ_[𝕝] `notation, but it does show up in lemma names
+  hidden behind the `⟪f, g⟫ₙ_[𝕝]` notation, but it does show up in lemma names
   `⟪f, g⟫_[𝕝, cWeight]` is called `wInner_cWeight`. Maybe we should introduce some naming
   convention, similarly to `MeasureTheory.average`?
 -/
diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean
index 06b575eb7a19ec..8dd063ab52d010 100644
--- a/Mathlib/Analysis/SpecialFunctions/Exponential.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Exponential.lean
@@ -91,7 +91,7 @@ variable {𝕂 𝔸 : Type*} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸
 
 /-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of
 characteristic zero has Fréchet derivative `NormedSpace.exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸`
-at any point `x`in the disk of convergence. -/
+at any point `x` in the disk of convergence. -/
 theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸}
     (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
     HasFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x := by
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
index 52a62cab745584..285d091c4da118 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
@@ -106,7 +106,7 @@ def LeftExtension.IsPointwiseLeftKanExtension.postcompose
     LeftExtension.postcompose₂ L F G |>.obj E |>.IsPointwiseLeftKanExtension := fun c ↦
   (hE c).postcompose G
 
-/-- The cocone at a point of the whiskering right by `G`of an extension is isomorphic to the
+/-- The cocone at a point of the whiskering right by `G` of an extension is isomorphic to the
 action of `G` on the cocone at that point for the original extension. -/
 @[simps!]
 def LeftExtension.coconeAtWhiskerRightIso (E : LeftExtension L F) (c : C) :
@@ -358,7 +358,7 @@ def RightExtension.IsPointwiseRightKanExtension.postcompose
     RightExtension.postcompose₂ L F G |>.obj E |>.IsPointwiseRightKanExtension := fun c ↦
   (hE c).postcompose G
 
-/-- The cone at a point of the whiskering right by `G`of an extension is isomorphic to the
+/-- The cone at a point of the whiskering right by `G` of an extension is isomorphic to the
 action of `G` on the cone at that point for the original extension. -/
 @[simps!]
 def RightExtension.coneAtWhiskerRightIso (E : RightExtension L F) (c : C) :
diff --git a/Mathlib/CategoryTheory/InducedCategory.lean b/Mathlib/CategoryTheory/InducedCategory.lean
index 065b1664f5b1ed..8d074a3b1925bb 100644
--- a/Mathlib/CategoryTheory/InducedCategory.lean
+++ b/Mathlib/CategoryTheory/InducedCategory.lean
@@ -10,7 +10,7 @@ public import Mathlib.CategoryTheory.Functor.FullyFaithful
 /-!
 # Induced categories and full subcategories
 
-Given a category `D` and a function `F : C → D `from a type `C` to the
+Given a category `D` and a function `F : C → D` from a type `C` to the
 objects of `D`, there is an essentially unique way to give `C` a
 category structure such that `F` becomes a fully faithful functor,
 namely by taking $$ Hom_C(X, Y) = Hom_D(FX, FY) $$. We call this the
diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean
index 8a0632ee8c11e6..fdff69482ce181 100644
--- a/Mathlib/CategoryTheory/Sites/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean
@@ -152,7 +152,7 @@ theorem isLimit_iff_isSheafFor :
 
 /-- Given sieve `S` and presheaf `P : Cᵒᵖ ⥤ A`, their natural associated cone admits at most one
     morphism from every cone in the same category (i.e. over the same diagram),
-    iff `Hom (E, P -)`is separated for the sieve `S` and all `E : A`. -/
+    iff `Hom (E, P -)` is separated for the sieve `S` and all `E : A`. -/
 theorem subsingleton_iff_isSeparatedFor :
     (∀ c, Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
       ∀ E : Aᵒᵖ, IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows := by
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
index faeb27814164d9..fd689177987267 100644
--- a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
+++ b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@@ -186,7 +186,7 @@ it suffices to prove it for
 * the finset family which only contains the empty finset.
 * `{s ∪ {a} | s ∈ 𝒜}` assuming the property for `𝒜` a family of finsets not containing `a`.
 * `ℬ ∪ 𝒞` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the ground type and
-  `ℬ`is a family of finsets not containing `a` and `𝒞` a family of finsets containing `a`.
+  `ℬ` is a family of finsets not containing `a` and `𝒞` a family of finsets containing `a`.
   Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you `𝒜 = ℬ ∪ 𝒞`, so that
   `ℬ = {s ∈ 𝒜 | a ∉ s}` and `𝒞 = {s ∈ 𝒜 | a ∈ s}`.
 
diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index dcd5c7bbcc9af3..5a9895b577eae0 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -45,7 +45,7 @@ library_note2 «specialised high priority simp lemma» /--
 It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
 using later, more general simp lemmas. In that case, the following reasons might be arguments for
 the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
-un``@[simp]``ed):
+un-`@[simp]`ed):
 1. There is a significant portion of the library which needs the early lemma to be available via
   `simp` and which doesn't have access to the more general lemmas.
 2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them
diff --git a/Mathlib/Data/PFun.lean b/Mathlib/Data/PFun.lean
index 72e5fcf912b173..9959e8916b6fb4 100644
--- a/Mathlib/Data/PFun.lean
+++ b/Mathlib/Data/PFun.lean
@@ -42,8 +42,8 @@ Partial functions can be considered as relations, so we specialize some `Rel` de
 * `PFun.ran`: Range of a partial function.
 * `PFun.preimage`: Preimage of a set under a partial function.
 * `PFun.core`: Core of a set under a partial function.
-* `PFun.graph`: Graph of a partial function `a →. β`as a `Set (α × β)`.
-* `PFun.graph'`: Graph of a partial function `a →. β`as a `Rel α β`.
+* `PFun.graph`: Graph of a partial function `a →. β` as a `Set (α × β)`.
+* `PFun.graph'`: Graph of a partial function `a →. β` as a `Rel α β`.
 
 ### `PFun α` as a monad
 
diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean
index 1f9b1d595066a8..113b512057feaf 100644
--- a/Mathlib/Data/Set/Lattice.lean
+++ b/Mathlib/Data/Set/Lattice.lean
@@ -181,12 +181,12 @@ theorem subset_iUnion₂ {s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : s i
 theorem iInter₂_subset {s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : ⋂ (i) (j), s i j ⊆ s i j :=
   iInf₂_le i j
 
-/-- This rather trivial consequence of `subset_iUnion`is convenient with `apply`, and has `i`
+/-- This rather trivial consequence of `subset_iUnion` is convenient with `apply`, and has `i`
 explicit for this purpose. -/
 theorem subset_iUnion_of_subset {s : Set α} {t : ι → Set α} (i : ι) (h : s ⊆ t i) : s ⊆ ⋃ i, t i :=
   le_iSup_of_le i h
 
-/-- This rather trivial consequence of `iInter_subset`is convenient with `apply`, and has `i`
+/-- This rather trivial consequence of `iInter_subset` is convenient with `apply`, and has `i`
 explicit for this purpose. -/
 theorem iInter_subset_of_subset {s : ι → Set α} {t : Set α} (i : ι) (h : s i ⊆ t) :
     ⋂ i, s i ⊆ t :=
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
index ce4ed20820a9d5..a16c989ddd3522 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
@@ -663,7 +663,7 @@ theorem eq_of_root {x y : L} (hx : IsAlgebraic K x)
     (h_ev : Polynomial.aeval y (minpoly K x) = 0) : minpoly K y = minpoly K x :=
   ((eq_iff_aeval_minpoly_eq_zero hx.isIntegral).mpr h_ev).symm
 
-/-- The canonical `algEquiv` between `K⟮x⟯`and `K⟮y⟯`, sending `x` to `y`, where `x` and `y` have
+/-- The canonical `algEquiv` between `K⟮x⟯` and `K⟮y⟯`, sending `x` to `y`, where `x` and `y` have
   the same minimal polynomial over `K`. -/
 noncomputable def algEquiv {x y : L} (hx : IsAlgebraic K x)
     (h_mp : minpoly K x = minpoly K y) : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := by
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
index 905f41e43ad95a..df314818d27b03 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
@@ -622,7 +622,7 @@ theorem contMDiffWithinAt_iff_le_ne_infty :
   | coe n =>
     exact contMDiffWithinAt_iff_nat.2 (fun m hm ↦ h _ (mod_cast hm) (by simp))
 
-/-- A function is `C^n`at a point iff it is `C^m`at this point, for
+/-- A function is `C^n` at a point iff it is `C^m` at this point, for
 any `m ≤ n` which is different from `∞`. This result is useful because, when `m ≠ ∞`, being
 `C^m` extends locally to a neighborhood, giving flexibility for local proofs. -/
 theorem contMDiffAt_iff_le_ne_infty :
diff --git a/Mathlib/GroupTheory/GroupAction/Hom.lean b/Mathlib/GroupTheory/GroupAction/Hom.lean
index 5e67c575023603..0d30e9a2e8de11 100644
--- a/Mathlib/GroupTheory/GroupAction/Hom.lean
+++ b/Mathlib/GroupTheory/GroupAction/Hom.lean
@@ -801,7 +801,7 @@ class MulSemiringActionSemiHomClass (F : Type*)
     extends DistribMulActionSemiHomClass F φ R S, RingHomClass F R S
 
 /-- `MulSemiringActionHomClass F M R S` states that `F` is a type of morphisms preserving
-the ring structure and equivariant with respect to a `DistribMulAction`of `M` on `R` and `S` .
+the ring structure and equivariant with respect to a `DistribMulAction` of `M` on `R` and `S`.
 -/
 abbrev MulSemiringActionHomClass
     (F : Type*)
diff --git a/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean b/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
index ccb96f08e1edfa..50fcc5571410f1 100644
--- a/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
+++ b/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
@@ -158,7 +158,7 @@ theorem isMultiplyPreprimitive_ofStabilizer
       aesop
     exact IsPreprimitive.of_surjective ofFixingSubgroup_insert_map_bijective.surjective
 
-/-- A pretransitive action is `n.succ-`preprimitive iff
+/-- A pretransitive action is `n.succ`-preprimitive iff
   the action of stabilizers is `n`-preprimitive. -/
 @[to_additive]
 theorem isMultiplyPreprimitive_succ_iff_ofStabilizer
diff --git a/Mathlib/GroupTheory/GroupAction/Pointwise.lean b/Mathlib/GroupTheory/GroupAction/Pointwise.lean
index 94f536d5a6c7bb..08930ab36886a5 100644
--- a/Mathlib/GroupTheory/GroupAction/Pointwise.lean
+++ b/Mathlib/GroupTheory/GroupAction/Pointwise.lean
@@ -22,7 +22,7 @@ public import Mathlib.Algebra.Group.Units.Hom
   It requires that `c` acts surjectively and `σ c` acts injectively and
   is provided with specific versions:
   - `preimage_smul_setₛₗ_of_isUnit_isUnit` when `c` and `σ c` are units
-  - `IsUnit.preimage_smul_setₛₗ` when `σ` belongs to a `MonoidHomClass`and `c` is a unit
+  - `IsUnit.preimage_smul_setₛₗ` when `σ` belongs to a `MonoidHomClass` and `c` is a unit
   - `MonoidHom.preimage_smul_setₛₗ` when `σ` is a `MonoidHom` and `c` is a unit
   - `Group.preimage_smul_setₛₗ` : when the types of `c` and `σ c` are groups.
 
diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean
index d52a0f72595493..35bc8db580ab34 100644
--- a/Mathlib/GroupTheory/GroupAction/Quotient.lean
+++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean
@@ -232,7 +232,7 @@ noncomputable def selfEquivSigmaOrbitsQuotientStabilizer : β ≃ Σ ω : Ω, α
 @[to_additive AddAction.sigmaFixedByEquivOrbitsProdAddGroup
       /-- **Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
       `{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × X/G`, where `G` is an additive group
-      acting on `X` and `X/G`denotes the quotient of `X` by the relation `orbitRel G X`. -/]
+      acting on `X` and `X/G` denotes the quotient of `X` by the relation `orbitRel G X`. -/]
 noncomputable def sigmaFixedByEquivOrbitsProdGroup : (Σ a : α, fixedBy β a) ≃ Ω × α :=
   calc
     (Σ a : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
diff --git a/Mathlib/GroupTheory/Perm/Centralizer.lean b/Mathlib/GroupTheory/Perm/Centralizer.lean
index b8badee243bca8..ff8ac2b5381ff2 100644
--- a/Mathlib/GroupTheory/Perm/Centralizer.lean
+++ b/Mathlib/GroupTheory/Perm/Centralizer.lean
@@ -85,7 +85,7 @@ injectivity `Equiv.Perm.OnCycleFactors.kerParam_injective`, its range
 * `Equiv.Perm.nat_card_centralizer g` computes the cardinality
   of the centralizer of `g`.
 
-* `Equiv.Perm.card_isConj_mul_eq g`computes the cardinality
+* `Equiv.Perm.card_isConj_mul_eq g` computes the cardinality
   of the conjugacy class of `g`.
 
 * We now can compute the cardinality of the set of permutations with given cycle type.
diff --git a/Mathlib/LinearAlgebra/PerfectPairing/Basic.lean b/Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
index 75111352e283fc..7e31fe8752f413 100644
--- a/Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
+++ b/Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@@ -41,14 +41,14 @@ class IsPerfPair (p : M →ₗ[R] N →ₗ[R] R) where
   bijective_left (p) : Bijective p
   bijective_right (p) : Bijective p.flip
 
-/-- Given a perfect pairing between `M`and `N`, we may interchange the roles of `M` and `N`. -/
+/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`. -/
 protected lemma IsPerfPair.flip (hp : p.IsPerfPair) : p.flip.IsPerfPair where
   bijective_left := IsPerfPair.bijective_right p
   bijective_right := IsPerfPair.bijective_left p
 
 variable [p.IsPerfPair]
 
-/-- Given a perfect pairing between `M`and `N`, we may interchange the roles of `M` and `N`. -/
+/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`. -/
 instance flip.instIsPerfPair : p.flip.IsPerfPair := .flip ‹_›
 
 variable (p)
diff --git a/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean b/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
index 7ddb0876cbb075..34f8a4a3192537 100644
--- a/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
@@ -35,7 +35,7 @@ stronger assumptions on the coefficients than here.
 * `RootPairing.EmbeddedG2.threeShortAddTwoLong`: the long root `3α + 2β`
 * `RootPairing.EmbeddedG2.span_eq_top`: a crystallographic reduced irreducible root pairing
   containing two roots with pairing `-3` is spanned by this pair (thus two-dimensional).
-* `RootPairing.EmbeddedG2.card_index_eq_twelve`: the `𝔤₂`root pairing has twelve roots.
+* `RootPairing.EmbeddedG2.card_index_eq_twelve`: the `𝔤₂` root pairing has twelve roots.
 
 ## TODO
 Once sufficient API for `RootPairing.Base` has been developed:
diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 6499dd23a8421b..405a1f0b605ebb 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -36,8 +36,8 @@ the bundled version, see `Rel`.
 * `Relation.EqvGen`: Equivalence closure. `EqvGen r` relates everything `ReflTransGen r` relates,
   plus for all related pairs it relates them in the opposite order.
 * `Relation.Comp`:  Relation composition. We provide notation `∘r`. For `r : α → β → Prop` and
-  `s : β → γ → Prop`, `r ∘r s`relates `a : α` and `c : γ` iff there exists `b : β` that's related to
-  both.
+  `s : β → γ → Prop`, `r ∘r s` relates `a : α` and `c : γ` iff there exists `b : β` that's related
+  to both.
 * `Relation.Map`: Image of a relation under a pair of maps. For `r : α → β → Prop`, `f : α → γ`,
   `g : β → δ`, `Map r f g` is the relation `γ → δ → Prop` relating `f a` and `g b` for all `a`, `b`
   related by `r`.
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean
index b50ecb49685da4..96c648d7617d5d 100644
--- a/Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean
+++ b/Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean
@@ -14,7 +14,7 @@ public import Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
 
 The main Result is `ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable`:
 Let `A` be a StarSubalgebra of `C(E, 𝕜)` that separates points and whose elements are bounded. If
-the integrals of all elements of `A` with respect to two finite measures `P, P'`coincide, then the
+the integrals of all elements of `A` with respect to two finite measures `P, P'` coincide, then the
 measures coincide. In other words: If a Subalgebra separates points, it separates finite measures.
 -/
 
diff --git a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
index d402c0b4316961..fd95230cba75f5 100644
--- a/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
+++ b/Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
@@ -27,7 +27,7 @@ quadratic character, zmod
 /-!
 ### Quadratic characters mod 4 and 8
 
-We define the primitive quadratic characters `χ₄`on `ZMod 4`
+We define the primitive quadratic characters `χ₄` on `ZMod 4`
 and `χ₈`, `χ₈'` on `ZMod 8`.
 -/
 
diff --git a/Mathlib/RepresentationTheory/FiniteIndex.lean b/Mathlib/RepresentationTheory/FiniteIndex.lean
index ea689a2dd72eff..c44047dcd2288b 100644
--- a/Mathlib/RepresentationTheory/FiniteIndex.lean
+++ b/Mathlib/RepresentationTheory/FiniteIndex.lean
@@ -14,7 +14,7 @@ public import Mathlib.RepresentationTheory.Induced
 
 Given a commutative ring `k`, a finite index subgroup `S ≤ G`, and a `k`-linear `S`-representation
 `A`, this file defines an isomorphism $Ind_S^G(A) ≅ Coind_S^G(A)$. Given `g : G` and `a : A`, the
-forward map sends `⟦g ⊗ₜ[k] a⟧` to the function `G → A`supported at `sg` by `ρ(s)(a)` for `s : S`
+forward map sends `⟦g ⊗ₜ[k] a⟧` to the function `G → A` supported at `sg` by `ρ(s)(a)` for `s : S`
 and which is 0 elsewhere. Meanwhile, the inverse sends `f : G → A` to `∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧` for
 `1 ≤ i ≤ n`, where `g₁, ..., gₙ` is a set of right coset representatives of `S`.
 
diff --git a/Mathlib/RingTheory/Conductor.lean b/Mathlib/RingTheory/Conductor.lean
index 44946af9f19b71..effa4800387022 100644
--- a/Mathlib/RingTheory/Conductor.lean
+++ b/Mathlib/RingTheory/Conductor.lean
@@ -12,7 +12,7 @@ public import Mathlib.RingTheory.PowerBasis
 # The conductor ideal
 This file defines the conductor ideal of an element `x` of `R`-algebra `S`. This is the ideal of
 `S` consisting of all elements `a` such that for all `b` in `S`, the product `a * b` lies in the
-`R`subalgebra of `S` generated by `x`.
+`R`-subalgebra of `S` generated by `x`.
 
 -/
 
diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
index fe2d713499baf0..8128b4bfa63e7c 100644
--- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
+++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
@@ -28,8 +28,8 @@ We define the completion of `K` with respect to the `v`-adic valuation, denoted
   to its `v`-adic valuation.
 - `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers v` is the ring of integers of
   `v.adicCompletion`.
-- `IsDedekindDomain.HeightOneSpectrum.adicAbv v`is the `v`-adic absolute value on `K` defined as `b`
-  raised to negative `v`-adic valuation, for some `b` in `ℝ≥0`.
+- `IsDedekindDomain.HeightOneSpectrum.adicAbv v` is the `v`-adic absolute value on `K` defined as
+  `b` raised to negative `v`-adic valuation, for some `b` in `ℝ≥0`.
 
 ## Main results
 - `IsDedekindDomain.HeightOneSpectrum.intValuation_le_one` : The `v`-adic valuation on `R` is
diff --git a/Mathlib/RingTheory/Ideal/Quotient/Operations.lean b/Mathlib/RingTheory/Ideal/Quotient/Operations.lean
index 56e8f8639114f7..bc3e34b9546f41 100644
--- a/Mathlib/RingTheory/Ideal/Quotient/Operations.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient/Operations.lean
@@ -813,7 +813,7 @@ theorem ker_quotQuotMk : RingHom.ker (quotQuotMk I J) = I ⊔ J := by
     comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective, ← RingHom.ker,
     mk_ker, sup_comm]
 
-/-- The ring homomorphism `R/(I ⊔ J) → (R/I)/J' `induced by `quotQuotMk` -/
+/-- The ring homomorphism `R/(I ⊔ J) → (R/I)/J'` induced by `quotQuotMk` -/
 def liftSupQuotQuotMk (I J : Ideal R) : R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) :=
   Ideal.Quotient.lift (I ⊔ J) (quotQuotMk I J) (ker_quotQuotMk I J).symm.le
 
@@ -954,7 +954,7 @@ theorem quotQuotMkₐ_toRingHom :
 theorem coe_quotQuotMkₐ : ⇑(quotQuotMkₐ R I J) = quotQuotMk I J :=
   rfl
 
-/-- The injective algebra homomorphism `A / (I ⊔ J) → (A / I) / J'`induced by `quot_quot_mk`,
+/-- The injective algebra homomorphism `A / (I ⊔ J) → (A / I) / J'` induced by `quotQuotMk`,
   where `J'` is the projection `J` in `A / I`. -/
 def liftSupQuotQuotMkₐ (I J : Ideal A) : A ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) :=
   AlgHom.mk (liftSupQuotQuotMk I J) fun _ => rfl
diff --git a/Mathlib/RingTheory/Localization/Pi.lean b/Mathlib/RingTheory/Localization/Pi.lean
index 356dacc59775e1..4b0af0032b116d 100644
--- a/Mathlib/RingTheory/Localization/Pi.lean
+++ b/Mathlib/RingTheory/Localization/Pi.lean
@@ -20,7 +20,7 @@ public import Mathlib.RingTheory.KrullDimension.Zero
 ## Main Result
 
 * `bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom`: the canonical map from a
-    localization of a finite product of rings `R i `at a monoid `M` to the direct product of
+    localization of a finite product of rings `R i` at a monoid `M` to the direct product of
     localizations `R i` at the projection of `M` onto each corresponding factor is bijective.
 
 ## Implementation notes
diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean
index 44c77e51acffe8..ded26d481b61d1 100644
--- a/Mathlib/Topology/Algebra/Module/Equiv.lean
+++ b/Mathlib/Topology/Algebra/Module/Equiv.lean
@@ -788,7 +788,7 @@ section Aut
 /-!
 ### Automorphisms as continuous linear equivalences and as units of the ring of endomorphisms
 
-The next theorems cover the identification between `M ≃L[R] M`and the group of units of the ring
+The next theorems cover the identification between `M ≃L[R] M` and the group of units of the ring
 `M →L[R] M`.
 -/
 
diff --git a/Mathlib/Topology/Algebra/Module/PerfectPairing.lean b/Mathlib/Topology/Algebra/Module/PerfectPairing.lean
index 0f94315132e208..81d5811fc97513 100644
--- a/Mathlib/Topology/Algebra/Module/PerfectPairing.lean
+++ b/Mathlib/Topology/Algebra/Module/PerfectPairing.lean
@@ -54,7 +54,7 @@ variable [p.IsContPerfPair]
 alias continuous_uncurry_of_isContPerfPair :=
   IsContPerfPair.continuous_uncurry
 
-/-- Given a perfect pairing between `M`and `N`, we may interchange the roles of `M` and `N`. -/
+/-- Given a perfect pairing between `M` and `N`, we may interchange the roles of `M` and `N`. -/
 instance flip.instIsContPerfPair : p.flip.IsContPerfPair where
   continuous_uncurry := p.continuous_uncurry_of_isContPerfPair.comp continuous_swap
   bijective_left := IsContPerfPair.bijective_right p
diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
index a6021efb8bdd67..699098a04c362f 100644
--- a/Mathlib/Topology/Constructions.lean
+++ b/Mathlib/Topology/Constructions.lean
@@ -565,7 +565,7 @@ protected lemma Topology.IsClosedEmbedding.inclusion (hst : s ⊆ t) (hs : IsClo
   isClosed_range := by rwa [range_inclusion]
 
 /-- Let `s, t ⊆ X` be two subsets of a topological space `X`.  If `t ⊆ s` and the topology induced
-by `X`on `s` is discrete, then also the topology induces on `t` is discrete. -/
+by `X` on `s` is discrete, then also the topology induces on `t` is discrete. -/
 theorem DiscreteTopology.of_subset {X : Type*} [TopologicalSpace X] {s t : Set X}
     (_ : DiscreteTopology s) (ts : t ⊆ s) : DiscreteTopology t :=
   (IsEmbedding.inclusion ts).discreteTopology
diff --git a/Mathlib/Topology/ContinuousMap/Lattice.lean b/Mathlib/Topology/ContinuousMap/Lattice.lean
index a173655c219cf5..714651a91c624d 100644
--- a/Mathlib/Topology/ContinuousMap/Lattice.lean
+++ b/Mathlib/Topology/ContinuousMap/Lattice.lean
@@ -29,7 +29,7 @@ variable {β : Type*} [TopologicalSpace β]
 
 section Lattice
 
-/-! `C(α, β)`is a lattice ordered group -/
+/-! `C(α, β)` is a lattice ordered group. -/
 
 @[to_additive]
 instance [PartialOrder β] [CommMonoid β] [IsOrderedMonoid β] [ContinuousMul β] :
diff --git a/Mathlib/Topology/NhdsSet.lean b/Mathlib/Topology/NhdsSet.lean
index 4ccc148feb23de..48b5ac80326950 100644
--- a/Mathlib/Topology/NhdsSet.lean
+++ b/Mathlib/Topology/NhdsSet.lean
@@ -22,7 +22,7 @@ There are a couple different notions equivalent to `s ∈ 𝓝ˢ t`:
 
 Furthermore, we have the following results:
 * `monotone_nhdsSet`: `𝓝ˢ` is monotone
-* In T₁-spaces, `𝓝ˢ`is strictly monotone and hence injective:
+* In T₁-spaces, `𝓝ˢ` is strictly monotone and hence injective:
   `strict_mono_nhdsSet`/`injective_nhdsSet`. These results are in
   `Mathlib/Topology/Separation/Basic.lean`.
 -/