diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean
index 0bd81eb12360e..60365a2970fc2 100644
--- a/Mathlib/Algebra/Group/Prod.lean
+++ b/Mathlib/Algebra/Group/Prod.lean
@@ -22,7 +22,7 @@ trivial `simp` lemmas, and define the following operations on `MonoidHom`s:
   as `MonoidHom`s;
 * `inl M N : M →* M × N`, `inr M N : N →* M × N`: inclusions of first/second monoid
   into the product;
-* `f.prod g : `M →* N × P`: sends `x` to `(f x, g x)`;
+* `f.prod g` : `M →* N × P`: sends `x` to `(f x, g x)`;
 * `f.coprod g : M × N →* P`: sends `(x, y)` to `f x * g y`;
 * `f.prodMap g : M × N → M' × N'`: `prod.map f g` as a `MonoidHom`,
   sends `(x, y)` to `(f x, g y)`.
diff --git a/Mathlib/Algebra/Module/Bimodule.lean b/Mathlib/Algebra/Module/Bimodule.lean
index 0d1c3f1e0d9af..62103c8aa0b40 100644
--- a/Mathlib/Algebra/Module/Bimodule.lean
+++ b/Mathlib/Algebra/Module/Bimodule.lean
@@ -32,8 +32,8 @@ Note that the corresponding result holds for the canonically isomorphic ring `R
 preferable to use the `R ⊗[ℕ] Sᵐᵒᵖ` instance since it works without additive inverses.
 
 Bimodules are thus just a special case of `Module`s and most of their properties follow from the
-theory of `Module`s`. In particular a two-sided Submodule of a bimodule is simply a term of type
-`submodule (R ⊗[ℕ] Sᵐᵒᵖ) M`.
+theory of `Module`s. In particular a two-sided Submodule of a bimodule is simply a term of type
+`Submodule (R ⊗[ℕ] Sᵐᵒᵖ) M`.
 
 This file is a place to collect results which are specific to bimodules.
 
diff --git a/Mathlib/Algebra/Order/Group/Defs.lean b/Mathlib/Algebra/Order/Group/Defs.lean
index a83dace3fb4ee..d69bcf7da84c4 100644
--- a/Mathlib/Algebra/Order/Group/Defs.lean
+++ b/Mathlib/Algebra/Order/Group/Defs.lean
@@ -1090,7 +1090,7 @@ class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, Li
 #align linear_ordered_add_comm_group LinearOrderedAddCommGroup
 
 /-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
-  Instances should include number systems with an infinite element adjoined.` -/
+  Instances should include number systems with an infinite element adjoined. -/
 class LinearOrderedAddCommGroupWithTop (α : Type _) extends LinearOrderedAddCommMonoidWithTop α,
   SubNegMonoid α, Nontrivial α where
   protected neg_top : -(⊤ : α) = ⊤
diff --git a/Mathlib/Algebra/Order/Monoid/Defs.lean b/Mathlib/Algebra/Order/Monoid/Defs.lean
index 789f6075c883a..390431a8b0657 100644
--- a/Mathlib/Algebra/Order/Monoid/Defs.lean
+++ b/Mathlib/Algebra/Order/Monoid/Defs.lean
@@ -103,7 +103,7 @@ class LinearOrderedCommMonoid (α : Type _) extends LinearOrder α, OrderedCommM
 attribute [to_additive existing] LinearOrderedCommMonoid.toOrderedCommMonoid
 
 /-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
-  Instances should include number systems with an infinite element adjoined.` -/
+  Instances should include number systems with an infinite element adjoined. -/
 class LinearOrderedAddCommMonoidWithTop (α : Type _) extends LinearOrderedAddCommMonoid α,
     Top α where
   /-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is larger than any other element.-/
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
index 81c76c912f110..fbb9fa412d6a1 100644
--- a/Mathlib/Algebra/Quaternion.lean
+++ b/Mathlib/Algebra/Quaternion.lean
@@ -315,7 +315,7 @@ theorem sub_self_re : a - a.re = a.im :=
 * `j * j = c₂`;
 * `i * j = k`, `j * i = -k`;
 * `k * k = -c₁ * c₂`;
-* `i * k = c₁ * j`, `k * i = `-c₁ * j`;
+* `i * k = c₁ * j`, `k * i = -c₁ * j`;
 * `j * k = -c₂ * i`, `k * j = c₂ * i`.  -/
 instance : Mul ℍ[R,c₁,c₂] :=
   ⟨fun a b =>
diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean
index 38794fbd63b33..14ae48fe2bbb1 100644
--- a/Mathlib/Analysis/BoxIntegral/Basic.lean
+++ b/Mathlib/Analysis/BoxIntegral/Basic.lean
@@ -15,7 +15,7 @@ import Mathlib.Topology.UniformSpace.Compact
 /-!
 # Integrals of Riemann, Henstock-Kurzweil, and McShane
 
-In this file we define the integral of a function over a box in `ℝⁿ. The same definition works for
+In this file we define the integral of a function over a box in `ℝⁿ`. The same definition works for
 Riemann, Henstock-Kurzweil, and McShane integrals.
 
 As usual, we represent `ℝⁿ` as the type of functions `ι → ℝ` for some finite type `ι`. A rectangular
@@ -812,7 +812,7 @@ box `J ≤ I` such that
 the distance between the term `vol J (f x)` of an integral sum corresponding to `J` and `g J` is
 less than or equal to `ε` if `x ∈ s` and is less than or equal to `ε * B J` otherwise.
 
-Then `f` is integrable on `I along `l` with integral `g I`. -/
+Then `f` is integrable on `I` along `l` with integral `g I`. -/
 theorem HasIntegral.of_le_Henstock_of_forall_isLittleO (hl : l ≤ Henstock) (B : ι →ᵇᵃ[I] ℝ)
     (hB0 : ∀ J, 0 ≤ B J) (g : ι →ᵇᵃ[I] F) (s : Set ℝⁿ) (hs : s.Countable)
     (H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > (0 : ℝ),
diff --git a/Mathlib/Analysis/Calculus/ContDiff.lean b/Mathlib/Analysis/Calculus/ContDiff.lean
index 4f03253836a8e..7c4224d9a2020 100644
--- a/Mathlib/Analysis/Calculus/ContDiff.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff.lean
@@ -932,12 +932,12 @@ theorem contDiff_prodAssoc_symm : ContDiff 𝕜 ⊤ <| (Equiv.prodAssoc E F G).s
 /-! ### Bundled derivatives are smooth -/
 
 /-- One direction of `contDiffWithinAt_succ_iff_hasFDerivWithinAt`, but where all derivatives
-taken within the same set. Version for partial derivatives / functions with parameters.  f x` is a
+taken within the same set. Version for partial derivatives / functions with parameters.  `f x` is a
 `C^n+1` family of functions and `g x` is a `C^n` family of points, then the derivative of `f x` at
 `g x` depends in a `C^n` way on `x`. We give a general version of this fact relative to sets which
-may not have unique derivatives, in the following form.  If `f : E × F → G` is `C^n+1` at `(x₀,
-g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is `C^n` at `x₀` within some set `s ⊆ E`, then
-there is a function `f' : E → F →L[𝕜] G` that is `C^n` at `x₀` within `s` such that for all `x`
+may not have unique derivatives, in the following form.  If `f : E × F → G` is `C^n+1` at
+`(x₀, g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is `C^n` at `x₀` within some set `s ⊆ E`,
+then there is a function `f' : E → F →L[𝕜] G` that is `C^n` at `x₀` within `s` such that for all `x`
 sufficiently close to `x₀` within `s ∪ {x₀}` the function `y ↦ f x y` has derivative `f' x` at `g x`
 within `t ⊆ F`.  For convenience, we return an explicit set of `x`'s where this holds that is a
 subset of `s ∪ {x₀}`.  We need one additional condition, namely that `t` is a neighborhood of
diff --git a/Mathlib/Analysis/Calculus/FDerivMeasurable.lean b/Mathlib/Analysis/Calculus/FDerivMeasurable.lean
index c24ee2ba89ac3..80b95927215fd 100644
--- a/Mathlib/Analysis/Calculus/FDerivMeasurable.lean
+++ b/Mathlib/Analysis/Calculus/FDerivMeasurable.lean
@@ -18,14 +18,14 @@ import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
 In this file we prove that the derivative of any function with complete codomain is a measurable
 function. Namely, we prove:
 
-* `measurable_set_of_differentiable_at`: the set `{x | differentiable_at 𝕜 f x}` is measurable;
+* `measurableSet_of_differentiableAt`: the set `{x | DifferentiableAt 𝕜 f x}` is measurable;
 * `measurable_fderiv`: the function `fderiv 𝕜 f` is measurable;
 * `measurable_fderiv_apply_const`: for a fixed vector `y`, the function `fun x ↦ fderiv 𝕜 f x y`
   is measurable;
 * `measurable_deriv`: the function `deriv f` is measurable (for `f : 𝕜 → F`).
 
 We also show the same results for the right derivative on the real line
-(see `measurable_deriv_within_Ici` and ``measurable_deriv_within_Ioi`), following the same
+(see `measurable_derivWithin_Ici` and `measurable_derivWithin_Ioi`), following the same
 proof strategy.
 
 ## Implementation
diff --git a/Mathlib/Analysis/Calculus/LocalExtr.lean b/Mathlib/Analysis/Calculus/LocalExtr.lean
index c889e56c18128..afd84a1503e97 100644
--- a/Mathlib/Analysis/Calculus/LocalExtr.lean
+++ b/Mathlib/Analysis/Calculus/LocalExtr.lean
@@ -26,7 +26,7 @@ This set is used in the proof of Fermat's Theorem (see below), and can be used t
 ## Main statements
 
 For each theorem name listed below,
-we also prove similar theorems for `min`, `extr` (if applicable)`,
+we also prove similar theorems for `min`, `extr` (if applicable),
 and `(f)deriv` instead of `has_fderiv`.
 
 * `IsLocalMaxOn.hasFDerivWithinAt_nonpos` : `f' y ≤ 0` whenever `a` is a local maximum
diff --git a/Mathlib/Analysis/Complex/CauchyIntegral.lean b/Mathlib/Analysis/Complex/CauchyIntegral.lean
index 9c08748420642..ec58117cb24f4 100644
--- a/Mathlib/Analysis/Complex/CauchyIntegral.lean
+++ b/Mathlib/Analysis/Complex/CauchyIntegral.lean
@@ -352,7 +352,7 @@ theorem circleIntegral_eq_of_differentiable_on_annulus_off_countable {c : ℂ} {
 /-- **Cauchy integral formula** for the value at the center of a disc. If `f` is continuous on a
 punctured closed disc of radius `R`, is differentiable at all but countably many points of the
 interior of this disc, and has a limit `y` at the center of the disc, then the integral
-$\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
+$\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to `2πiy`. -/
 theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto {c : ℂ}
     {R : ℝ} (h0 : 0 < R) {f : ℂ → E} {y : E} {s : Set ℂ} (hs : s.Countable)
     (hc : ContinuousOn f (closedBall c R \ {c}))
@@ -400,7 +400,7 @@ theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of
 
 /-- **Cauchy integral formula** for the value at the center of a disc. If `f : ℂ → E` is continuous
 on a closed disc of radius `R` and is complex differentiable at all but countably many points of its
-interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
+interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to `2πiy`. -/
 theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 < R)
     {f : ℂ → E} {c : ℂ} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (closedBall c R))
     (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
@@ -620,4 +620,3 @@ protected theorem _root_.Differentiable.hasFPowerSeriesOnBall {f : ℂ → E} (h
 #align differentiable.has_fpower_series_on_ball Differentiable.hasFPowerSeriesOnBall
 
 end Complex
-
diff --git a/Mathlib/Analysis/Convex/Normed.lean b/Mathlib/Analysis/Convex/Normed.lean
index c1ed4c70ce1d3..b73ca9168330b 100644
--- a/Mathlib/Analysis/Convex/Normed.lean
+++ b/Mathlib/Analysis/Convex/Normed.lean
@@ -100,7 +100,7 @@ theorem convexHull_exists_dist_ge2 {s t : Set E} {x y : E} (hx : x ∈ convexHul
   exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')
 #align convex_hull_exists_dist_ge2 convexHull_exists_dist_ge2
 
-/-- Emetric diameter of the convex hull of a set `s` equals the emetric diameter of `s. -/
+/-- Emetric diameter of the convex hull of a set `s` equals the emetric diameter of `s`. -/
 @[simp]
 theorem convexHull_ediam (s : Set E) : EMetric.diam (convexHull ℝ s) = EMetric.diam s := by
   refine' (EMetric.diam_le fun x hx y hy => _).antisymm (EMetric.diam_mono <| subset_convexHull ℝ s)
@@ -111,7 +111,7 @@ theorem convexHull_ediam (s : Set E) : EMetric.diam (convexHull ℝ s) = EMetric
   exact EMetric.edist_le_diam_of_mem hx' hy'
 #align convex_hull_ediam convexHull_ediam
 
-/-- Diameter of the convex hull of a set `s` equals the emetric diameter of `s. -/
+/-- Diameter of the convex hull of a set `s` equals the emetric diameter of `s`. -/
 @[simp]
 theorem convexHull_diam (s : Set E) : Metric.diam (convexHull ℝ s) = Metric.diam s := by
   simp only [Metric.diam, convexHull_ediam]
diff --git a/Mathlib/Analysis/Convex/StrictConvexSpace.lean b/Mathlib/Analysis/Convex/StrictConvexSpace.lean
index 861bcf0c371ca..79a378f5423fb 100644
--- a/Mathlib/Analysis/Convex/StrictConvexSpace.lean
+++ b/Mathlib/Analysis/Convex/StrictConvexSpace.lean
@@ -178,8 +178,8 @@ theorem norm_combo_lt_of_ne (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r) (hne : x 
   exact combo_mem_ball_of_ne hx hy hne ha hb hab
 #align norm_combo_lt_of_ne norm_combo_lt_of_ne
 
-/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `‖x + y‖ < ‖x‖ +
-‖y‖`. -/
+/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `‖x + y‖ < ‖x‖ + ‖y‖`.
+-/
 theorem norm_add_lt_of_not_sameRay (h : ¬SameRay ℝ x y) : ‖x + y‖ < ‖x‖ + ‖y‖ := by
   simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.def] at h
   rcases h with ⟨hx, hy, hne⟩
diff --git a/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean b/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean
index e4722c82cdaef..a3c5d4f0b0c68 100644
--- a/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean
+++ b/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean
@@ -29,8 +29,8 @@ open LinearIsometry ContinuousLinearMap
 open RealInnerProductSpace
 
 /-- A map between two inner product spaces is a conformal map if and only if it preserves inner
-products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that `⟪f u, f v⟫ = c *
-⟪u, v⟫` for all `u`, `v`. -/
+products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that
+`⟪f u, f v⟫ = c * ⟪u, v⟫` for all `u`, `v`. -/
 theorem isConformalMap_iff (f : E →L[ℝ] F) :
     IsConformalMap f ↔ ∃ c : ℝ, 0 < c ∧ ∀ u v : E, ⟪f u, f v⟫ = c * ⟪u, v⟫ := by
   constructor
diff --git a/Mathlib/Analysis/Normed/Group/AddTorsor.lean b/Mathlib/Analysis/Normed/Group/AddTorsor.lean
index c0791cf8a3feb..51e8fde9090a4 100644
--- a/Mathlib/Analysis/Normed/Group/AddTorsor.lean
+++ b/Mathlib/Analysis/Normed/Group/AddTorsor.lean
@@ -207,8 +207,7 @@ theorem edist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
 #align edist_vsub_vsub_le edist_vsub_vsub_le
 
 /-- The pseudodistance defines a pseudometric space structure on the torsor. This
-is not an instance because it depends on `V` to define a `MetricSpace
-P`. -/
+is not an instance because it depends on `V` to define a `MetricSpace P`. -/
 def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [SeminormedAddCommGroup V]
     [AddTorsor V P] : PseudoMetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
@@ -223,8 +222,7 @@ def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [SeminormedA
 #align pseudo_metric_space_of_normed_add_comm_group_of_add_torsor pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor
 
 /-- The distance defines a metric space structure on the torsor. This
-is not an instance because it depends on `V` to define a `MetricSpace
-P`. -/
+is not an instance because it depends on `V` to define a `MetricSpace P`. -/
 def metricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [NormedAddCommGroup V]
     [AddTorsor V P] : MetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
diff --git a/Mathlib/Analysis/NormedSpace/MazurUlam.lean b/Mathlib/Analysis/NormedSpace/MazurUlam.lean
index a2d159742b7a1..53bc7b2a46145 100644
--- a/Mathlib/Analysis/NormedSpace/MazurUlam.lean
+++ b/Mathlib/Analysis/NormedSpace/MazurUlam.lean
@@ -65,7 +65,7 @@ theorem midpoint_fixed {x y : PE} :
   -- midpoint `z` of `[x, y]`.
   set R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
   set f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
-  -- Note that `f` doubles the value of ``dist (e z) z`
+  -- Note that `f` doubles the value of `dist (e z) z`
   have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z := by
     intro e
     dsimp
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
index 2b542963fac2a..f5d1ae09d0066 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
@@ -119,7 +119,7 @@ theorem coe_int_mul_eq_zsmul (x : ℝ) (n : ℤ) : ↑((n : ℝ) * x : ℝ) = n
 theorem angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} : (θ : Angle) = ψ ↔ ∃ k : ℤ, θ - ψ = 2 * π * k := by
   simp only [QuotientAddGroup.eq, AddSubgroup.zmultiples_eq_closure,
     AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]
-  -- Porting note: added `rw`, `simp [Angle.coe, QuotientAddGroup.eq] doesn't fire otherwise
+  -- Porting note: added `rw`, `simp [Angle.coe, QuotientAddGroup.eq]` doesn't fire otherwise
   rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]
   simp only [AddSubgroup.zmultiples_eq_closure,
     AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]
diff --git a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
index ad8d3cf16ea0c..03d9720c928a3 100644
--- a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
+++ b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@@ -162,7 +162,7 @@ def leftDerivedZeroToSelfAppIso [EnoughProjectives C] [PreservesFiniteColimits F
 #align category_theory.abelian.functor.left_derived_zero_to_self_app_iso CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppIso
 
 /-- Given `P : ProjectiveResolution X` and `Q : ProjectiveResolution Y` and a morphism `f : X ⟶ Y`,
-naturality of the square given by `left_derived_zero_to_self_obj_hom. -/
+naturality of the square given by `leftDerived_zero_to_self_obj_hom`. -/
 theorem leftDerived_zero_to_self_natural [EnoughProjectives C] {X : C} {Y : C} (f : X ⟶ Y)
     (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) :
     (F.leftDerived 0).map f ≫ leftDerivedZeroToSelfApp F Q =
diff --git a/Mathlib/CategoryTheory/Action.lean b/Mathlib/CategoryTheory/Action.lean
index 09805e5a8350d..a12472db64e36 100644
--- a/Mathlib/CategoryTheory/Action.lean
+++ b/Mathlib/CategoryTheory/Action.lean
@@ -22,7 +22,7 @@ types, mapping the single object of M to X and an element `m : M` to map `X →
 multiplication by `m`.
   This functor induces a category structure on X -- a special case of the category of elements.
 A morphism `x ⟶ y` in this category is simply a scalar `m : M` such that `m • x = y`. In the case
-where M is a group, this category is a groupoid -- the `action groupoid'.
+where M is a group, this category is a groupoid -- the *action groupoid*.
 -/
 
 
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
index c15abdedf4b82..51bcc2e0e5936 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -16,8 +16,8 @@ import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 # Concrete categories
 
 A concrete category is a category `C` with a fixed faithful functor
-`forget : C ⥤ Type _`.  We define concrete categories using `class
-concrete_category`.  In particular, we impose no restrictions on the
+`forget : C ⥤ Type _`.  We define concrete categories using `class ConcreteCategory`.
+In particular, we impose no restrictions on the
 carrier type `C`, so `Type` is a concrete category with the identity
 forgetful functor.
 
diff --git a/Mathlib/CategoryTheory/Limits/Fubini.lean b/Mathlib/CategoryTheory/Limits/Fubini.lean
index 789f3bb5f21a3..4bb19a08a9dac 100644
--- a/Mathlib/CategoryTheory/Limits/Fubini.lean
+++ b/Mathlib/CategoryTheory/Limits/Fubini.lean
@@ -321,7 +321,7 @@ theorem limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {j} {k} :
   simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_hom_π,
     Iso.refl_inv, limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc]
   erw [NatTrans.id_app]
-  -- Why can't `simp` do this`?
+  -- Why can't `simp` do this?
   dsimp
   -- porting note: the original proof only had `simp`.
   -- However, now `CategoryTheory.Bifunctor.map_id` does not get used by `simp`
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
index ea8ac867285b2..6a9047f6ac9fd 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
@@ -135,7 +135,7 @@ def compNatIso {D : Type u'} [Category.{v} D] [HasZeroMorphisms D] (F : C ⥤ D)
 
 end
 
-/-- If `s` is a limit kernel fork and `k : W ⟶ X` satisfies ``k ≫ f = 0`, then there is some
+/-- If `s` is a limit kernel fork and `k : W ⟶ X` satisfies `k ≫ f = 0`, then there is some
     `l : W ⟶ s.X` such that `l ≫ fork.ι s = k`. -/
 def KernelFork.IsLimit.lift' {s : KernelFork f} (hs : IsLimit s) {W : C} (k : W ⟶ X)
     (h : k ≫ f = 0) : { l : W ⟶ s.pt // l ≫ Fork.ι s = k } :=
diff --git a/Mathlib/CategoryTheory/Preadditive/Projective.lean b/Mathlib/CategoryTheory/Preadditive/Projective.lean
index 663dcd21a4068..b0b4b1bf4993a 100644
--- a/Mathlib/CategoryTheory/Preadditive/Projective.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Projective.lean
@@ -26,8 +26,8 @@ projective object.
 epimorphism.
 
 Given a morphism `f : X ⟶ Y`, `CategoryTheory.Projective.left f` is a projective object over
-`CategoryTheory.Limits.kernel f`, and `projective.d f : projective.left f ⟶ X` is the morphism `π
-(kernel f) ≫ kernel.ι f`.
+`CategoryTheory.Limits.kernel f`, and `projective.d f : projective.left f ⟶ X` is the morphism
+`π (kernel f) ≫ kernel.ι f`.
 
 -/
 
diff --git a/Mathlib/Combinatorics/Quiver/Symmetric.lean b/Mathlib/Combinatorics/Quiver/Symmetric.lean
index 7a9d26630cf8e..3bd92736771b7 100644
--- a/Mathlib/Combinatorics/Quiver/Symmetric.lean
+++ b/Mathlib/Combinatorics/Quiver/Symmetric.lean
@@ -54,7 +54,7 @@ def reverse {V} [Quiver.{v + 1} V] [HasReverse V] {a b : V} : (a ⟶ b) → (b 
   HasReverse.reverse'
 #align quiver.reverse Quiver.reverse
 
-/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity.`-/
+/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity. -/
 class HasInvolutiveReverse extends HasReverse V where
   /-- `reverse` is involutive -/
   inv' : ∀ {a b : V} (f : a ⟶ b), reverse (reverse f) = f
diff --git a/Mathlib/Control/Monad/Basic.lean b/Mathlib/Control/Monad/Basic.lean
index fa1b4e3ac828e..93cabd0c01c76 100644
--- a/Mathlib/Control/Monad/Basic.lean
+++ b/Mathlib/Control/Monad/Basic.lean
@@ -27,8 +27,8 @@ import Mathlib.Tactic.Common
 Set of rewrite rules and automation for monads in general and
 `ReaderT`, `StateT`, `ExceptT` and `OptionT` in particular.
 
-The rewrite rules for monads are carefully chosen so that `simp with
-functor_norm` will not introduce monadic vocabulary in a context where
+The rewrite rules for monads are carefully chosen so that `simp with functor_norm`
+will not introduce monadic vocabulary in a context where
 applicatives would do just fine but will handle monadic notation
 already present in an expression.
 
diff --git a/Mathlib/Data/Finset/NoncommProd.lean b/Mathlib/Data/Finset/NoncommProd.lean
index 4330a7ba1382b..99b53e76123dc 100644
--- a/Mathlib/Data/Finset/NoncommProd.lean
+++ b/Mathlib/Data/Finset/NoncommProd.lean
@@ -228,7 +228,7 @@ namespace Finset
 variable [Monoid β] [Monoid γ]
 
 
-/-- Proof used in definition of `Finset.noncommProd -/
+/-- Proof used in definition of `Finset.noncommProd` -/
 @[to_additive]
 theorem noncommProd_lemma (s : Finset α) (f : α → β)
     (comm : (s : Set α).Pairwise fun a b => Commute (f a) (f b)) :
diff --git a/Mathlib/Data/Fintype/Sort.lean b/Mathlib/Data/Fintype/Sort.lean
index 5e66b00bd4903..4da45c3457c86 100644
--- a/Mathlib/Data/Fintype/Sort.lean
+++ b/Mathlib/Data/Fintype/Sort.lean
@@ -35,7 +35,7 @@ def monoEquivOfFin (α : Type _) [Fintype α] [LinearOrder α] {k : ℕ} (h : Fi
 variable {α : Type _} [DecidableEq α] [Fintype α] [LinearOrder α] {m n : ℕ} {s : Finset α}
 
 /-- If `α` is a linearly ordered fintype, `s : Finset α` has cardinality `m` and its complement has
-cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of Fin m` to
+cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of `Fin m` to
 elements of `s` and elements of `Fin n` to elements of `sᶜ` while preserving order on each
 "half" of `Fin m ⊕ Fin n` (using `Set.orderIsoOfFin`). -/
 def finSumEquivOfFinset (hm : s.card = m) (hn : sᶜ.card = n) : Sum (Fin m) (Fin n) ≃ α :=
diff --git a/Mathlib/Data/List/MinMax.lean b/Mathlib/Data/List/MinMax.lean
index 3e7ff40c31450..a6f9b0f47d8e9 100644
--- a/Mathlib/Data/List/MinMax.lean
+++ b/Mathlib/Data/List/MinMax.lean
@@ -19,7 +19,7 @@ The main definitions are `argmax`, `argmin`, `minimum` and `maximum` for lists.
 
 `argmax f l` returns `some a`, where `a` of `l` that maximises `f a`. If there are `a b` such that
   `f a = f b`, it returns whichever of `a` or `b` comes first in the list.
-  `argmax f []` = none`
+  `argmax f [] = none`
 
 `minimum l` returns a `WithTop α`, the smallest element of `l` for nonempty lists, and `⊤` for
 `[]`
@@ -95,14 +95,14 @@ variable [Preorder β] [@DecidableRel β (· < ·)] {f : α → β} {l : List α
 
 /-- `argmax f l` returns `some a`, where `f a` is maximal among the elements of `l`, in the sense
 that there is no `b ∈ l` with `f a < f b`. If `a`, `b` are such that `f a = f b`, it returns
-whichever of `a` or `b` comes first in the list. `argmax f []` = none`. -/
+whichever of `a` or `b` comes first in the list. `argmax f [] = none`. -/
 def argmax (f : α → β) (l : List α) : Option α :=
   l.foldl (argAux fun b c => f c < f b) none
 #align list.argmax List.argmax
 
 /-- `argmin f l` returns `some a`, where `f a` is minimal among the elements of `l`, in the sense
 that there is no `b ∈ l` with `f b < f a`. If `a`, `b` are such that `f a = f b`, it returns
-whichever of `a` or `b` comes first in the list. `argmin f []` = none`. -/
+whichever of `a` or `b` comes first in the list. `argmin f [] = none`. -/
 def argmin (f : α → β) (l : List α) :=
   l.foldl (argAux fun b c => f b < f c) none
 #align list.argmin List.argmin
diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean
index b80224bee00c1..6188102a12ca6 100644
--- a/Mathlib/Data/Real/ENNReal.lean
+++ b/Mathlib/Data/Real/ENNReal.lean
@@ -33,8 +33,8 @@ and prove basic properties of these operations, order, and conversions to/from `
 
   - `a + b` is defined so that `↑p + ↑q = ↑(p + q)` for `(p q : ℝ≥0)` and `a + ∞ = ∞ + a = ∞`;
 
-  - `a * b` is defined so that `↑p * ↑q = ↑(p * q)` for `(p q : ℝ≥0)`, `0 * ∞ = ∞ * 0 = 0`, and `a *
-    ∞ = ∞ * a = ∞` for `a ≠ 0`;
+  - `a * b` is defined so that `↑p * ↑q = ↑(p * q)` for `(p q : ℝ≥0)`, `0 * ∞ = ∞ * 0 = 0`, and
+    `a * ∞ = ∞ * a = ∞` for `a ≠ 0`;
 
   - `a - b` is defined as the minimal `d` such that `a ≤ d + b`; this way we have
     `↑p - ↑q = ↑(p - q)`, `∞ - ↑p = ∞`, `↑p - ∞ = ∞ - ∞ = 0`; note that there is no negation, only
diff --git a/Mathlib/Data/Real/Pi/Bounds.lean b/Mathlib/Data/Real/Pi/Bounds.lean
index 1b7dd17a9774a..9f4746cad7c7f 100644
--- a/Mathlib/Data/Real/Pi/Bounds.lean
+++ b/Mathlib/Data/Real/Pi/Bounds.lean
@@ -96,7 +96,7 @@ section Tactic
 open Lean Elab Tactic
 
 /-- `numDen stx` takes a syntax expression `stx` and
-* if it is of the form `a / b`, then it returns `some (a, b);
+* if it is of the form `a / b`, then it returns `some (a, b)`;
 * otherwise it returns `none`.
 -/
 private def numDen : Syntax → Option (Syntax.Term × Syntax.Term)
diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
index 9f42d105c1a5a..a3152d832bee1 100644
--- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
+++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
@@ -74,8 +74,8 @@ We prove the following properties of `CircleDeg1Lift.translationNumber`.
 * `CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq`: let `f₁` and `f₂` be
   two actions of a group `G` on the circle by degree 1 maps (formally, `f₁` and `f₂` are two
   homomorphisms from `G →* CircleDeg1Lift`). If the translation numbers of `f₁ g` and `f₂ g` are
-  equal to each other for all `g : G`, then these two actions are semiconjugate by some `F :
-  CircleDeg1Lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
+  equal to each other for all `g : G`, then these two actions are semiconjugate by some
+  `F : CircleDeg1Lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
   d'homeomorphismes du cercle et cohomologie bornee][ghys87:groupes].
 
 ## Notation
@@ -104,8 +104,8 @@ preserving circle homeomorphisms for two reasons:
 
 Here are some short-term goals.
 
-* Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use `Units
-  CircleDeg1Lift` for now, but it's better to have a dedicated type (or a typeclass?).
+* Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use
+  `Units CircleDeg1Lift` for now, but it's better to have a dedicated type (or a typeclass?).
 
 * Prove that the `SemiconjBy` relation on circle homeomorphisms is an equivalence relation.
 
diff --git a/Mathlib/Dynamics/OmegaLimit.lean b/Mathlib/Dynamics/OmegaLimit.lean
index 2bf85745b8360..cb2fe4b5143d8 100644
--- a/Mathlib/Dynamics/OmegaLimit.lean
+++ b/Mathlib/Dynamics/OmegaLimit.lean
@@ -226,7 +226,7 @@ theorem omegaLimit_subset_closure_fw_image {u : Set τ} (hu : u ∈ f) :
 #align omega_limit_subset_closure_fw_image omegaLimit_subset_closure_fw_image
 
 /-!
-### `ω-limits and compactness
+### ω-limits and compactness
 -/
 
 
diff --git a/Mathlib/GroupTheory/Congruence.lean b/Mathlib/GroupTheory/Congruence.lean
index e2c4fe7a81e7a..f08b7777546fc 100644
--- a/Mathlib/GroupTheory/Congruence.lean
+++ b/Mathlib/GroupTheory/Congruence.lean
@@ -959,7 +959,7 @@ theorem lift_apply_mk' (f : c.Quotient →* P) :
 
 /-- Homomorphisms on the quotient of a monoid by a congruence relation are equal if they
     are equal on elements that are coercions from the monoid. -/
-@[to_additive "Homomorphisms on the quotient of an AddMonoid` by an additive congruence relation
+@[to_additive "Homomorphisms on the quotient of an `AddMonoid` by an additive congruence relation
 are equal if they are equal on elements that are coercions from the `AddMonoid`."]
 theorem lift_funext (f g : c.Quotient →* P) (h : ∀ a : M, f a = g a) : f = g := by
   rw [← lift_apply_mk' f, ← lift_apply_mk' g]
diff --git a/Mathlib/GroupTheory/DoubleCoset.lean b/Mathlib/GroupTheory/DoubleCoset.lean
index 74cb3b2188f7b..879774fbd3837 100644
--- a/Mathlib/GroupTheory/DoubleCoset.lean
+++ b/Mathlib/GroupTheory/DoubleCoset.lean
@@ -25,7 +25,7 @@ this is the usual left or right quotient of a group by a subgroup.
 ## Main definitions
 
 * `rel`: The double coset relation defined by two subgroups `H K` of `G`.
-* `Doset.quotient`: The quotient of `G` by the double coset relation, i.e, ``H \ G / K`.
+* `Doset.quotient`: The quotient of `G` by the double coset relation, i.e, `H \ G / K`.
 -/
 -- porting note: removed import
 -- import Mathlib.Tactic.Group
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index c5e50f9621e0a..67171d3b68776 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -698,7 +698,7 @@ theorem exists_pow_eq_one [Finite G] (x : G) : IsOfFinOrder x := by
 
 /-- This is the same as `orderOf_pos'` but with one fewer explicit assumption since this is
   automatic in case of a finite cancellative monoid.-/
-@[to_additive "This is the same as `addOrderOf_pos' but with one fewer explicit
+@[to_additive "This is the same as `addOrderOf_pos'` but with one fewer explicit
 assumption since this is automatic in case of a finite cancellative additive monoid."]
 theorem orderOf_pos [Finite G] (x : G) : 0 < orderOf x :=
   orderOf_pos' (exists_pow_eq_one x)
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean b/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
index d923247d2ea43..0df1a4224b629 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
@@ -178,7 +178,7 @@ Given an interval `[a, b]` and a point `c ∈ (a, b)`, `c = lineMap a b r`, ther
 say that the point `(c, f c)` is above/below the segment `[(a, f a), (b, f b)]`:
 
 * compare `f c` to `lineMap (f a) (f b) r`;
-* compare `slope f a c` to `slope `f a b`;
+* compare `slope f a c` to `slope f a b`;
 * compare `slope f c b` to `slope f a b`;
 * compare `slope f a c` to `slope f c b`.
 
diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean
index fd0fbd1dc4fcc..dc921fcf862a9 100644
--- a/Mathlib/LinearAlgebra/Finsupp.lean
+++ b/Mathlib/LinearAlgebra/Finsupp.lean
@@ -37,8 +37,8 @@ interpreted as a submodule of `α →₀ M`. We also define `LinearMap` versions
 * `Finsupp.domLCongr`: a `LinearEquiv` version of `Finsupp.domCongr`;
 * `Finsupp.congr`: if the sets `s` and `t` are equivalent, then `supported M R s` is equivalent to
   `supported M R t`;
-* `Finsupp.lcongr`: a `LinearEquiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃
-  β` and `e' : M ≃ₗ[R] N`.
+* `Finsupp.lcongr`: a `LinearEquiv`alence between `α →₀ M` and `β →₀ N` constructed using
+  `e : α ≃ β` and `e' : M ≃ₗ[R] N`.
 
 ## Tags
 
diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
index 950453117a925..a73c5718fc172 100644
--- a/Mathlib/LinearAlgebra/LinearIndependent.lean
+++ b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -48,7 +48,7 @@ vectors.
 * `linearIndependent_empty_type`: a family indexed by an empty type is linearly independent;
 * `linearIndependent_unique_iff`: if `ι` is a singleton, then `LinearIndependent K v` is
   equivalent to `v default ≠ 0`;
-* linearIndependent_option`, `linearIndependent_sum`, `linearIndependent_fin_cons`,
+* `linearIndependent_option`, `linearIndependent_sum`, `linearIndependent_fin_cons`,
   `linearIndependent_fin_succ`: type-specific tests for linear independence of families of vector
   fields;
 * `linearIndependent_insert`, `linearIndependent_union`, `linearIndependent_pair`,
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index cff8cf6d92b5b..4b397c3eebeb5 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -62,7 +62,7 @@ def pprodEquivProd : PProd α β ≃ α × β where
 
 /-- Product of two equivalences, in terms of `PProd`. If `α ≃ β` and `γ ≃ δ`, then
 `PProd α γ ≃ PProd β δ`. -/
--- porting note: in Lean 3 this had @[congr]`
+-- porting note: in Lean 3 this had `@[congr]`
 @[simps apply]
 def pprodCongr (e₁ : α ≃ β) (e₂ : γ ≃ δ) : PProd α γ ≃ PProd β δ where
   toFun x := ⟨e₁ x.1, e₂ x.2⟩
@@ -1430,7 +1430,7 @@ where `p : β → Prop`, permuting only the `b : β` that satisfy `p b`.
 This can be used to extend the domain across a function `f : α → β`,
 keeping everything outside of `Set.range f` fixed. For this use-case `Equiv` given by `f` can
 be constructed by `Equiv.of_leftInverse'` or `Equiv.of_leftInverse` when there is a known
-inverse, or `Equiv.ofInjective` in the general case.`.
+inverse, or `Equiv.ofInjective` in the general case.
 -/
 def Perm.extendDomain : Perm β' :=
   (permCongr f e).subtypeCongr (Equiv.refl _)
diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean
index a4183cf0f6f00..95a0e8381bf66 100644
--- a/Mathlib/Logic/Equiv/Defs.lean
+++ b/Mathlib/Logic/Equiv/Defs.lean
@@ -926,7 +926,7 @@ end Equiv
 namespace Quot
 
 /-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
-if `ra a₁ a₂ ↔ rb (e a₁) (e a₂). -/
+if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
 protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β)
     (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quot ra ≃ Quot rb where
   toFun := Quot.map e fun a₁ a₂ => (eq a₁ a₂).1
@@ -960,7 +960,7 @@ end Quot
 namespace Quotient
 
 /-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
-if `ra a₁ a₂ ↔ rb (e a₁) (e a₂). -/
+if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
 protected def congr {ra : Setoid α} {rb : Setoid β} (e : α ≃ β)
     (eq : ∀ a₁ a₂, @Setoid.r α ra a₁ a₂ ↔ @Setoid.r β rb (e a₁) (e a₂)) :
     Quotient ra ≃ Quotient rb := Quot.congr e eq
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 6e7b1ad3bbec5..49e26ad40b541 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -1000,7 +1000,7 @@ theorem eq_rec_on_bijective {α : Sort _} {C : α → Sort _} :
 
 theorem eq_mp_bijective {α β : Sort _} (h : α = β) : Function.Bijective (Eq.mp h) := by
   -- TODO: mathlib3 uses `eq_rec_on_bijective`, difference in elaboration here
-  -- due to `@[macro_inline] possibly?
+  -- due to `@[macro_inline]` possibly?
   cases h
   refine ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩
 #align eq_mp_bijective eq_mp_bijective
diff --git a/Mathlib/Logic/Relator.lean b/Mathlib/Logic/Relator.lean
index 62e72f5e1274b..2367e362d7bda 100644
--- a/Mathlib/Logic/Relator.lean
+++ b/Mathlib/Logic/Relator.lean
@@ -32,7 +32,7 @@ variable {α : Sort u₁} {β : Sort u₂} {γ : Sort v₁} {δ : Sort v₂}
 variable (R : α → β → Prop) (S : γ → δ → Prop)
 
 /-- The binary relations `R : α → β → Prop` and `S : γ → δ → Prop` induce a binary
-    relation on functions `LiftFun : (f : α → γ) (g : β → δ) : Prop'. -/
+    relation on functions `LiftFun : (f : α → γ) (g : β → δ) : Prop`. -/
 def LiftFun (f : α → γ) (g : β → δ) : Prop :=
   ∀⦃a b⦄, R a b → S (f a) (g b)
 #align relator.lift_fun Relator.LiftFun
diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean
index daa690dcb5966..47b4dfc8916b0 100644
--- a/Mathlib/MeasureTheory/Function/Jacobian.lean
+++ b/Mathlib/MeasureTheory/Function/Jacobian.lean
@@ -1234,7 +1234,7 @@ theorem det_one_smulRight {𝕜 : Type _} [NormedField 𝕜] (v : 𝕜) :
 #align measure_theory.det_one_smul_right MeasureTheory.det_one_smulRight
 
 /-- Integrability in the change of variable formula for differentiable functions (one-variable
-version): if a function `f` is injective and differentiable on a measurable set ``s ⊆ ℝ`, then a
+version): if a function `f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then a
 function `g : ℝ → F` is integrable on `f '' s` if and only if `|(f' x)| • g ∘ f` is integrable on
 `s`. -/
 theorem integrableOn_image_iff_integrableOn_abs_deriv_smul {s : Set ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ}
diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean
index 089942cc3d0ba..c135351e29fb4 100644
--- a/Mathlib/MeasureTheory/Function/L1Space.lean
+++ b/Mathlib/MeasureTheory/Function/L1Space.lean
@@ -329,7 +329,7 @@ theorem tendsto_lintegral_norm_of_dominated_convergence {F : ℕ → α → β}
     aestronglyMeasurable_of_tendsto_ae _ F_measurable h_lim
   let b a := 2 * ENNReal.ofReal (bound a)
   /- `‖F n a‖ ≤ bound a` and `F n a --> f a` implies `‖f a‖ ≤ bound a`, and thus by the
-    triangle inequality, have `‖F n a - f a‖ ≤ 2 * (bound a). -/
+    triangle inequality, have `‖F n a - f a‖ ≤ 2 * (bound a)`. -/
   have hb : ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a := by
     intro n
     filter_upwards [all_ae_ofReal_F_le_bound h_bound n,
diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
index 29c9e5d08ab66..05633f6260d6b 100644
--- a/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -509,7 +509,7 @@ instance instIsScalarTower [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsSc
   smul_assoc k k' f := Subtype.ext <| smul_assoc k k' (f : α →ₘ[μ] E)
 
 instance instBoundedSMul [Fact (1 ≤ p)] : BoundedSMul 𝕜 (Lp E p μ) :=
-  -- TODO: add `BoundedSMul.of_nnnorm_smul_le
+  -- TODO: add `BoundedSMul.of_nnnorm_smul_le`
   BoundedSMul.of_norm_smul_le fun r f => by
     suffices (‖r • f‖₊ : ℝ≥0∞) ≤ ‖r‖₊ * ‖f‖₊ by exact_mod_cast this
     rw [nnnorm_def, nnnorm_def, ENNReal.coe_toNNReal (Lp.snorm_ne_top _),
diff --git a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
index fb30de1e66fcb..7c47f290a0ff3 100644
--- a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
+++ b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
@@ -39,8 +39,8 @@ Porting note (Yury Kudryashov): I disabled some of these notations because I fai
 work with Lean 4.
 
 * `ℝⁿ`, `ℝⁿ⁺¹`, `Eⁿ⁺¹`: `Fin n → ℝ`, `Fin (n + 1) → ℝ`, `Fin (n + 1) → E`;
-* `face i`: the `i`-th face of the box `[a, b]` as a closed segment in `ℝⁿ`, namely `[a ∘
-  Fin.succAbove i, b ∘ Fin.succAbove i]`;
+* `face i`: the `i`-th face of the box `[a, b]` as a closed segment in `ℝⁿ`, namely
+  `[a ∘ Fin.succAbove i, b ∘ Fin.succAbove i]`;
 * `e i` : `i`-th basis vector `Pi.single i 1`;
 * `frontFace i`, `backFace i`: embeddings `ℝⁿ → ℝⁿ⁺¹` corresponding to the front face
   `{x | x i = b i}` and back face `{x | x i = a i}` of the box `[a, b]`, respectively.
diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
index f100caac85c53..e09724216c8b9 100644
--- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
+++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
@@ -133,9 +133,9 @@ atom at one of the endpoints.
 ### Combining one-sided and two-sided derivatives
 
 There are some `intervalIntegral.FTCFilter` instances where the fact that it is one-sided or
-two-sided depends on the point, namely `(x, 𝓝[Set.Icc a b] x, 𝓝[Set.Icc a b] x)` (resp. `(x,
-𝓝[Set.uIcc a b] x, 𝓝[Set.uIcc a b] x), with `x ∈ Icc a b` (resp. `x ∈ uIcc a b`).  This results in a
-two-sided derivatives for `x ∈ Set.Ioo a b` and one-sided derivatives for `x ∈ {a, b}`. Other
+two-sided depends on the point, namely `(x, 𝓝[Set.Icc a b] x, 𝓝[Set.Icc a b] x)` (resp.
+`(x, 𝓝[Set.uIcc a b] x, 𝓝[Set.uIcc a b] x)`, with `x ∈ Icc a b` (resp. `x ∈ uIcc a b`). This results
+in a two-sided derivatives for `x ∈ Set.Ioo a b` and one-sided derivatives for `x ∈ {a, b}`. Other
 instances could be added when needed (in that case, one also needs to add instances for
 `Filter.IsMeasurablyGenerated` and `Filter.TendstoIxxClass`).
 
diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
index 2ea6d2d6cf6d0..5c56e126f9c50 100644
--- a/Mathlib/MeasureTheory/Integral/SetIntegral.lean
+++ b/Mathlib/MeasureTheory/Integral/SetIntegral.lean
@@ -959,7 +959,7 @@ s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that `s
 along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).toReal` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).toReal`, so the formalization can take an optional
-argument `m` with this formula and a proof `of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
+argument `m` with this formula and a proof of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
 arguments, `m i = (μ (s i)).toReal` is used in the output. -/
 theorem Filter.Tendsto.integral_sub_linear_isLittleO_ae [NormedSpace ℝ E] [CompleteSpace E]
     {μ : Measure α} {l : Filter α} [l.IsMeasurablyGenerated] {f : α → E} {b : E}
@@ -990,7 +990,7 @@ provided that `s i` tends to `(𝓝[t] a).smallSets` along `li`.  Since `μ (s i
 number, we use `(μ (s i)).toReal` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).toReal`, so the formalization can take an optional
-argument `m` with this formula and a proof `of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
+argument `m` with this formula and a proof of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
 arguments, `m i = (μ (s i)).toReal` is used in the output. -/
 theorem ContinuousWithinAt.integral_sub_linear_isLittleO_ae [TopologicalSpace α]
     [OpensMeasurableSpace α] [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α}
@@ -1007,11 +1007,11 @@ theorem ContinuousWithinAt.integral_sub_linear_isLittleO_ae [TopologicalSpace α
 /-- Fundamental theorem of calculus for set integrals, `nhds` version: if `μ` is a locally finite
 measure and `f` is an almost everywhere measurable function that is continuous at a point `a`, then
 `∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at `li` provided that `s` tends to
-`(𝓝 a).smallSets` along `li.  Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).toReal` in
+`(𝓝 a).smallSets` along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).toReal` in
 the actual statement.
 
 Often there is a good formula for `(μ (s i)).toReal`, so the formalization can take an optional
-argument `m` with this formula and a proof `of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
+argument `m` with this formula and a proof of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
 arguments, `m i = (μ (s i)).toReal` is used in the output. -/
 theorem ContinuousAt.integral_sub_linear_isLittleO_ae [TopologicalSpace α] [OpensMeasurableSpace α]
     [NormedSpace ℝ E] [CompleteSpace E] {μ : Measure α} [IsLocallyFiniteMeasure μ] {a : α}
@@ -1028,7 +1028,7 @@ finite measure, `f` is continuous on a measurable set `t`, and `a ∈ t`, then `
 Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).toReal` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).toReal`, so the formalization can take an optional
-argument `m` with this formula and a proof `of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
+argument `m` with this formula and a proof of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
 arguments, `m i = (μ (s i)).toReal` is used in the output. -/
 theorem ContinuousOn.integral_sub_linear_isLittleO_ae [TopologicalSpace α] [OpensMeasurableSpace α]
     [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopologyEither α E] {μ : Measure α}
diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
index 0ef1dce85e592..4563a1b2918e2 100644
--- a/Mathlib/ModelTheory/Semantics.lean
+++ b/Mathlib/ModelTheory/Semantics.lean
@@ -184,7 +184,7 @@ theorem realize_varsToConstants [L[[α]].Structure M] [(lhomWithConstants L α).
     t.varsToConstants.realize v = t.realize (Sum.elim (fun a => ↑(L.con a)) v) := by
   induction' t with ab n f ts ih
   · cases' ab with a b
-    --Porting note: both cases were `simp [Language.con]
+    --Porting note: both cases were `simp [Language.con]`
     . simp [Language.con, realize, constantMap, funMap_eq_coe_constants]
     . simp [realize, constantMap]
   · simp only [realize, constantsOn, mk₂_Functions, ih]
diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
index d982fe88d4ae6..aeaa0f5a7cdd0 100644
--- a/Mathlib/Order/Filter/Basic.lean
+++ b/Mathlib/Order/Filter/Basic.lean
@@ -2005,7 +2005,7 @@ theorem pure_bind (a : α) (m : α → Filter β) : bind (pure a) m = m a := by
 
 In this section we define `Filter.monad`, a `Monad` structure on `Filter`s. This definition is not
 an instance because its `Seq` projection is not equal to the `Filter.seq` function we use in the
-`Applicative` instance on `Filter.
+`Applicative` instance on `Filter`.
 -/
 
 section
diff --git a/Mathlib/Order/Filter/Prod.lean b/Mathlib/Order/Filter/Prod.lean
index 2af8eb93a9145..65b2c7a32923b 100644
--- a/Mathlib/Order/Filter/Prod.lean
+++ b/Mathlib/Order/Filter/Prod.lean
@@ -14,8 +14,8 @@ import Mathlib.Order.Filter.Basic
 # Product and coproduct filters
 
 In this file we define `Filter.prod f g` (notation: `f ×ˢ g`) and `Filter.coprod f g`. The product
-of two filters is the largest filter `l` such that `Filter.Tendsto Prod.fst l f` and `Filter.Tendsto
-Prod.snd l g`.
+of two filters is the largest filter `l` such that `Filter.Tendsto Prod.fst l f` and
+`Filter.Tendsto Prod.snd l g`.
 
 ## Implementation details
 
diff --git a/Mathlib/Order/Hom/Lattice.lean b/Mathlib/Order/Hom/Lattice.lean
index 0d5213cf838a2..7c6d94e3b1264 100644
--- a/Mathlib/Order/Hom/Lattice.lean
+++ b/Mathlib/Order/Hom/Lattice.lean
@@ -1697,7 +1697,7 @@ theorem withTop_comp (f : InfHom β γ) (g : InfHom α β) :
   FunLike.coe_injective $ Eq.symm $ Option.map_comp_map _ _
 #align inf_hom.with_top_comp InfHom.withTop_comp
 
-/-- Adjoins a `⊥ to the domain and codomain of an `InfHom`. -/
+/-- Adjoins a `⊥` to the domain and codomain of an `InfHom`. -/
 @[simps]
 protected def withBot (f : InfHom α β) : InfHom (WithBot α) (WithBot β) where
   toFun := Option.map f
diff --git a/Mathlib/RingTheory/FinitePresentation.lean b/Mathlib/RingTheory/FinitePresentation.lean
index dc8d9a27425cd..492606c5b8d41 100644
--- a/Mathlib/RingTheory/FinitePresentation.lean
+++ b/Mathlib/RingTheory/FinitePresentation.lean
@@ -518,7 +518,7 @@ theorem comp_surjective {f : A →ₐ[R] B} {g : B →ₐ[R] C} (hf : f.FinitePr
 
 theorem of_surjective (f : A →ₐ[R] B) (hf : Surjective f) (hker : f.toRingHom.ker.FG) :
     f.FinitePresentation := by
-  -- Porting note: added `convert
+  -- Porting note: added `convert`
   convert RingHom.FinitePresentation.of_surjective f hf hker
 #align alg_hom.finite_presentation.of_surjective AlgHom.FinitePresentation.of_surjective
 
diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
index 644363f243180..abfc4a8d3ae05 100644
--- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean
+++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
@@ -690,7 +690,7 @@ theorem coe_quotLeftToQuotSupₐ : ⇑(quotLeftToQuotSupₐ R I J) = quotLeftToQ
   rfl
 #align double_quot.coe_quot_left_to_quot_supₐ DoubleQuot.coe_quotLeftToQuotSupₐ
 
-/-- The algebra homomorphism `(A / I) / J' -> A / (I ⊔ J) induced by `quotQuotToQuotSup`,
+/-- The algebra homomorphism `(A / I) / J' -> A / (I ⊔ J)` induced by `quotQuotToQuotSup`,
   where `J'` is the projection of `J` in `A / I`. -/
 def quotQuotToQuotSupₐ : (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) →ₐ[R] A ⧸ I ⊔ J :=
   AlgHom.mk (quotQuotToQuotSup I J) fun _ => rfl
diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
index b15f343a04aa7..1bd7494de7e4f 100644
--- a/Mathlib/RingTheory/IntegralDomain.lean
+++ b/Mathlib/RingTheory/IntegralDomain.lean
@@ -232,7 +232,7 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : (∑ g : G, f g) =
       cases' hx ⟨f.toHomUnits g, g, rfl⟩ with n hn
       rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow,
         eq_comm] at hn
-    replace hx1 : (x.val : R) - 1 ≠ 0  -- porting note: was `(x : R)
+    replace hx1 : (x.val : R) - 1 ≠ 0  -- porting note: was `(x : R)`
     exact fun h => hx1 (Subtype.eq (Units.ext (sub_eq_zero.1 h)))
     let c := (univ.filter fun g => f.toHomUnits g = 1).card
     calc
diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
index 45f65eefd50b0..91857f8260958 100644
--- a/Mathlib/RingTheory/OreLocalization/Basic.lean
+++ b/Mathlib/RingTheory/OreLocalization/Basic.lean
@@ -168,7 +168,7 @@ theorem liftExpand_of {C : Sort _} {P : R → S → C}
 #align ore_localization.lift_expand_of OreLocalization.liftExpand_of
 
 /-- A version of `liftExpand` used to simultaneously lift functions with two arguments
-in ``R[S⁻¹]`.-/
+in `R[S⁻¹]`. -/
 def lift₂Expand {C : Sort _} (P : R → S → R → S → C)
     (hP :
       ∀ (r₁ t₁ : R) (s₁ : S) (ht₁ : (s₁ : R) * t₁ ∈ S) (r₂ t₂ : R) (s₂ : S)
diff --git a/Mathlib/Tactic/Linarith/Parsing.lean b/Mathlib/Tactic/Linarith/Parsing.lean
index cdfd2d1f5462b..cff32c1c5f7c6 100644
--- a/Mathlib/Tactic/Linarith/Parsing.lean
+++ b/Mathlib/Tactic/Linarith/Parsing.lean
@@ -87,7 +87,7 @@ def Sum.one : Sum := RBMap.empty.insert Monom.one 1
 def Sum.scaleByMonom (s : Sum) (m : Monom) : Sum :=
   s.foldr (fun m' coeff sm => sm.insert (m + m') coeff) RBMap.empty
 
-/-- `sum.mul s1 s2` distributes the multiplication of two sums.` -/
+/-- `sum.mul s1 s2` distributes the multiplication of two sums. -/
 def Sum.mul (s1 s2 : Sum) : Sum :=
   s1.foldr (fun mn coeff sm => sm + ((s2.scaleByMonom mn).mapVal (fun _ v => v * coeff)))
     RBMap.empty
diff --git a/Mathlib/Tactic/MkIffOfInductiveProp.lean b/Mathlib/Tactic/MkIffOfInductiveProp.lean
index 70221be2983ce..aeb7412376cc5 100644
--- a/Mathlib/Tactic/MkIffOfInductiveProp.lean
+++ b/Mathlib/Tactic/MkIffOfInductiveProp.lean
@@ -102,7 +102,7 @@ structure Shape : Type where
     ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []`
   ```
   and the first two variables `α` and `R` are "params", while the `a : α` gets
-  eliminated in a `compactRelation`, so `variablesKept = [false].
+  eliminated in a `compactRelation`, so `variablesKept = [false]`.
 
   `List.Chain.cons` has type
   ```lean
diff --git a/Mathlib/Tactic/Simps/NotationClass.lean b/Mathlib/Tactic/Simps/NotationClass.lean
index 2432de8cc3e83..e9445ea45d7b0 100644
--- a/Mathlib/Tactic/Simps/NotationClass.lean
+++ b/Mathlib/Tactic/Simps/NotationClass.lean
@@ -93,7 +93,7 @@ structure AutomaticProjectionData where
   /-- `className` is the name of the class we are looking for. -/
   className : Name
   /-- `isNotation` is a boolean that specifies whether this is notation
-    (false for the coercions `FunLike` and SetLike`). If this is set to true, we add the current
+    (false for the coercions `FunLike` and `SetLike`). If this is set to true, we add the current
     class as hypothesis during type-class synthesis. -/
   isNotation := true
   /-- The method to find the arguments of the class. -/
diff --git a/Mathlib/Testing/SlimCheck/Sampleable.lean b/Mathlib/Testing/SlimCheck/Sampleable.lean
index 109fb44a01934..8271a210b7be8 100644
--- a/Mathlib/Testing/SlimCheck/Sampleable.lean
+++ b/Mathlib/Testing/SlimCheck/Sampleable.lean
@@ -9,7 +9,7 @@ import Qq
 /-!
 # `SampleableExt` Class
 This class permits the creation samples of a given type
-controlling the size of those values using the `Gen` monad`.
+controlling the size of those values using the `Gen` monad.
 
 # `Shrinkable` Class
 This class helps minimize examples by creating smaller versions of
@@ -21,9 +21,9 @@ When testing a proposition like `∀ n : ℕ, prime n → n ≤ 100`,
 `SampleableExt` to generate small examples of ℕ and progressively increase
 in size. For each example `n`, `prime n` is tested. If it is false,
 the example will be rejected (not a test success nor a failure) and
-`SlimCheck` will move on to other examples. If `prime n` is true, `n
-≤ 100` will be tested. If it is false, `n` is a counter-example of `∀
-n : ℕ, prime n → n ≤ 100` and the test fails. If `n ≤ 100` is true,
+`SlimCheck` will move on to other examples. If `prime n` is true,
+`n ≤ 100` will be tested. If it is false, `n` is a counter-example of
+`∀ n : ℕ, prime n → n ≤ 100` and the test fails. If `n ≤ 100` is true,
 the test passes and `SlimCheck` moves on to trying more examples.
 
 This is a port of the Haskell QuickCheck library.
@@ -48,7 +48,7 @@ as interpreted (using `interp`) as an object of the right type. If you
 are using it in the first way, this proxy type will simply be the type
 itself and the `interp` function `id`.
 
-### `Shrinkable
+### `Shrinkable`
 Given an example `x : α`, `Shrinkable α` gives us a way to shrink it
 and suggest simpler examples.
 
diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean
index 8b4ec807c318f..787ef6e76e810 100644
--- a/Mathlib/Topology/Algebra/Monoid.lean
+++ b/Mathlib/Topology/Algebra/Monoid.lean
@@ -870,7 +870,7 @@ namespace ContinuousMap
 variable [Mul X] [ContinuousMul X]
 
 /-- The continuous map `fun y => y * x` -/
-@[to_additive "The continuous map `fun y => y + x"]
+@[to_additive "The continuous map `fun y => y + x`"]
 protected def mulRight (x : X) : C(X, X) :=
   mk _ (continuous_mul_right x)
 #align continuous_map.mul_right ContinuousMap.mulRight
@@ -883,7 +883,7 @@ theorem coe_mulRight (x : X) : ⇑(ContinuousMap.mulRight x) = fun y => y * x :=
 #align continuous_map.coe_add_right ContinuousMap.coe_addRight
 
 /-- The continuous map `fun y => x * y` -/
-@[to_additive "The continuous map `fun y => x + y"]
+@[to_additive "The continuous map `fun y => x + y`"]
 protected def mulLeft (x : X) : C(X, X) :=
   mk _ (continuous_mul_left x)
 #align continuous_map.mul_left ContinuousMap.mulLeft
diff --git a/Mathlib/Topology/Algebra/Polynomial.lean b/Mathlib/Topology/Algebra/Polynomial.lean
index bddb00806e4ca..2cf736414a3c0 100644
--- a/Mathlib/Topology/Algebra/Polynomial.lean
+++ b/Mathlib/Topology/Algebra/Polynomial.lean
@@ -19,8 +19,8 @@ import Mathlib.Analysis.Normed.Field.Basic
 
 In this file we prove the following lemmas.
 
-* `Polynomial.continuous_eval₂: `Polynomial.eval₂` defines a continuous function.
-* `Polynomial.continuous_aeval: `Polynomial.aeval` defines a continuous function;
+* `Polynomial.continuous_eval₂`: `Polynomial.eval₂` defines a continuous function.
+* `Polynomial.continuous_aeval`: `Polynomial.aeval` defines a continuous function;
   we also prove convenience lemmas `Polynomial.continuousAt_aeval`,
   `Polynomial.continuousWithinAt_aeval`, `Polynomial.continuousOn_aeval`.
 * `Polynomial.continuous`:  `Polynomial.eval` defines a continuous functions;
diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean
index 5a85761837570..53d8b3cde1400 100644
--- a/Mathlib/Topology/Basic.lean
+++ b/Mathlib/Topology/Basic.lean
@@ -1192,7 +1192,7 @@ theorem accPt_iff_frequently (x : α) (C : Set α) : AccPt x (𝓟 C) ↔ ∃ᶠ
 #align acc_pt_iff_frequently accPt_iff_frequently
 
 /-- If `x` is an accumulation point of `F` and `F ≤ G`, then
-`x` is an accumulation point of `D. -/
+`x` is an accumulation point of `D`. -/
 theorem AccPt.mono {x : α} {F G : Filter α} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G :=
   NeBot.mono h (inf_le_inf_left _ hFG)
 #align acc_pt.mono AccPt.mono
diff --git a/Mathlib/Topology/DiscreteQuotient.lean b/Mathlib/Topology/DiscreteQuotient.lean
index 822305a770cc2..0fc76be136400 100644
--- a/Mathlib/Topology/DiscreteQuotient.lean
+++ b/Mathlib/Topology/DiscreteQuotient.lean
@@ -43,8 +43,8 @@ i.e., `x ~ y` means that `x` and `y` belong to the same connected component. In
 is a discrete topological space, then `x ~ y` is equivalent (propositionally, not definitionally) to
 `x = y`.
 
-Given `f : C(X, Y)`, we define a predicate `DiscreteQuotient.LEComap f A B` for `A :
-DiscreteQuotient X` and `B : DiscreteQuotient Y`, asserting that `f` descends to `A → B`.  If
+Given `f : C(X, Y)`, we define a predicate `DiscreteQuotient.LEComap f A B` for
+`A : DiscreteQuotient X` and `B : DiscreteQuotient Y`, asserting that `f` descends to `A → B`. If
 `cond : DiscreteQuotient.LEComap h A B`, the function `A → B` is obtained by
 `DiscreteQuotient.map f cond`.
 
diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean
index d0d8aed15c4a6..05301f0792d26 100644
--- a/Mathlib/Topology/FiberBundle/Trivialization.lean
+++ b/Mathlib/Topology/FiberBundle/Trivialization.lean
@@ -729,7 +729,7 @@ theorem isImage_preimage_prod (e : Trivialization F proj) (s : Set B) :
     e.toLocalHomeomorph.IsImage (proj ⁻¹' s) (s ×ˢ univ) := fun x hx => by simp [e.coe_fst', hx]
 #align trivialization.is_image_preimage_prod Trivialization.isImage_preimage_prod
 
-/-- Restrict a `Trivialization` to an open set in the base. `-/
+/-- Restrict a `Trivialization` to an open set in the base. -/
 protected def restrOpen (e : Trivialization F proj) (s : Set B) (hs : IsOpen s) :
     Trivialization F proj where
   toLocalHomeomorph :=
@@ -791,7 +791,7 @@ noncomputable def piecewiseLeOfEq [LinearOrder B] [OrderTopology B] (e e' : Triv
 linearly ordered base `B` and a point `a ∈ e.baseSet ∩ e'.baseSet`, `e.piecewise_le e' a He He'`
 is the bundle trivialization over `Set.ite (Iic a) e.baseSet e'.baseSet` that is equal to `e` on
 points `p` such that `proj p ≤ a` and is equal to `((e' p).1, h (e' p).2)` otherwise, where
-`h = `e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
+`h = e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
 `h (e' p).2 = (e p).2` whenever `e p = a`. -/
 noncomputable def piecewiseLe [LinearOrder B] [OrderTopology B] (e e' : Trivialization F proj)
     (a : B) (He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) : Trivialization F proj :=
diff --git a/Mathlib/Topology/MetricSpace/EMetricParacompact.lean b/Mathlib/Topology/MetricSpace/EMetricParacompact.lean
index 7fe669a659e17..14f0deeab1b9f 100644
--- a/Mathlib/Topology/MetricSpace/EMetricParacompact.lean
+++ b/Mathlib/Topology/MetricSpace/EMetricParacompact.lean
@@ -53,7 +53,7 @@ instance (priority := 100) [PseudoEMetricSpace α] : ParacompactSpace α := by
   refine' ⟨fun ι s ho hcov => _⟩
   simp only [iUnion_eq_univ_iff] at hcov
   -- choose a well founded order on `S`
-  -- porting note: todo: add lemma that claims `∃ i : LinearOrder ι, WellFoundedLT ι
+  -- porting note: todo: add lemma that claims `∃ i : LinearOrder ι, WellFoundedLT ι`
   let _ : LinearOrder ι := by classical exact linearOrderOfSTO WellOrderingRel
   have wf : WellFounded ((· < ·) : ι → ι → Prop) := @IsWellFounded.wf ι WellOrderingRel _
   -- Let `ind x` be the minimal index `s : S` such that `x ∈ s`.
diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean
index 25e956030eaf3..6662fc0a8398f 100644
--- a/Mathlib/Topology/Order/Basic.lean
+++ b/Mathlib/Topology/Order/Basic.lean
@@ -57,7 +57,7 @@ see their statements.
 * `le_of_tendsto_of_tendsto` : if `f` converges to `a`, `g` converges to `b`, and eventually
   `f x ≤ g x`, then `a ≤ b`
 * `le_of_tendsto`, `ge_of_tendsto` : if `f` converges to `a` and eventually `f x ≤ b`
-  (resp., `b ≤ f x`), then `a ≤ b` (resp., `b ≤ a); we also provide primed versions
+  (resp., `b ≤ f x`), then `a ≤ b` (resp., `b ≤ a`); we also provide primed versions
   that assume the inequalities to hold for all `x`.
 
 ### Min, max, `sSup` and `sInf`
diff --git a/Mathlib/Topology/Paracompact.lean b/Mathlib/Topology/Paracompact.lean
index aa44edafdc101..061b60c069b72 100644
--- a/Mathlib/Topology/Paracompact.lean
+++ b/Mathlib/Topology/Paracompact.lean
@@ -30,7 +30,7 @@ We also prove the following facts.
 
 * A locally compact sigma compact Hausdorff space is paracompact, see instance
   `paracompact_of_locallyCompact_sigmaCompact`. Moreover, we can choose a locally finite
-  refinement with sets in a given collection of filter bases of `𝓝 x, `x : X`, see
+  refinement with sets in a given collection of filter bases of `𝓝 x`, `x : X`, see
   `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`. For example, in a proper metric space
   every open covering `⋃ i, s i` admits a refinement `⋃ i, Metric.ball (c i) (r i)`.
 
diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
index c490963ab983f..ffabf6629caaf 100644
--- a/Mathlib/Topology/UniformSpace/Basic.lean
+++ b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -1652,7 +1652,7 @@ theorem uniformContinuous_inf_dom_left₂ {α β γ} {f : α → β → γ} {ua1
     (h : by haveI := ua1; haveI := ub1; exact UniformContinuous fun p : α × β => f p.1 p.2) : by
       haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2;
         exact UniformContinuous fun p : α × β => f p.1 p.2 := by
-  -- proof essentially copied from ``continuous_inf_dom_left₂`
+  -- proof essentially copied from `continuous_inf_dom_left₂`
   have ha := @UniformContinuous.inf_dom_left _ _ id ua1 ua2 ua1 (@uniformContinuous_id _ (id _))
   have hb := @UniformContinuous.inf_dom_left _ _ id ub1 ub2 ub1 (@uniformContinuous_id _ (id _))
   have h_unif_cont_id :=
@@ -1666,7 +1666,7 @@ theorem uniformContinuous_inf_dom_right₂ {α β γ} {f : α → β → γ} {ua
     (h : by haveI := ua2; haveI := ub2; exact UniformContinuous fun p : α × β => f p.1 p.2) : by
       haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2;
         exact UniformContinuous fun p : α × β => f p.1 p.2 := by
-  -- proof essentially copied from ``continuous_inf_dom_right₂`
+  -- proof essentially copied from `continuous_inf_dom_right₂`
   have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
   have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
   have h_unif_cont_id :=
@@ -1680,7 +1680,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_Inf_dom`
   let _ : UniformSpace (α × β) := instUniformSpaceProd
   have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
   have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
diff --git a/test/nontriviality.lean b/test/nontriviality.lean
index 5bd4784336a79..398faa538c6b8 100644
--- a/test/nontriviality.lean
+++ b/test/nontriviality.lean
@@ -40,7 +40,7 @@ example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 2 ∣ 4 := by
   rename_i inst; guard_hyp inst : Nontrivial R
   decide
 
-/-! Test using `@[nontriviality]` lemmas in `nontriviality and custom `simp` lemmas -/
+/-! Test using `@[nontriviality]` lemmas in `nontriviality` and custom `simp` lemmas -/
 
 
 def EmptyOrUniv {α : Type _} (s : Set α) : Prop :=