leanprover-community · int-y1 · Oct 10, 2023
diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean
@@ -13,7 +13,7 @@ import Mathlib.Algebra.Category.ModuleCat.Basic
 /-!
 # Category instance for algebras over a commutative ring
 
-We introduce the bundled category `AlgebraCat` of algebras over a fixed commutative ring `R ` along
+We introduce the bundled category `AlgebraCat` of algebras over a fixed commutative ring `R` along
 with the forgetful functors to `RingCat` and `ModuleCat`. We furthermore show that the functor
 associating to a type the free `R`-algebra on that type is left adjoint to the forgetful functor.
 -/

diff --git a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@@ -54,11 +54,11 @@ structure LeftHomologyData where
   π : K ⟶ H
   /-- the kernel condition for `i` -/
   wi : i ≫ S.g = 0
-  /-- `i : K ⟶ S.X₂ ` is a kernel of `g : S.X₂ ⟶ S.X₃` -/
+  /-- `i : K ⟶ S.X₂` is a kernel of `g : S.X₂ ⟶ S.X₃` -/
   hi : IsLimit (KernelFork.ofι i wi)
   /-- the cokernel condition for `π` -/
   wπ : hi.lift (KernelFork.ofι _ S.zero) ≫ π = 0
-  /-- `π : K ⟶ H ` is a cokernel of the induced morphism `S.f' : S.X₁ ⟶ K` -/
+  /-- `π : K ⟶ H` is a cokernel of the induced morphism `S.f' : S.X₁ ⟶ K` -/
   hπ : IsColimit (CokernelCofork.ofπ π wπ)
 
 initialize_simps_projections LeftHomologyData (-hi, -hπ)

diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@@ -116,7 +116,7 @@ lemma ι_descQ_eq_zero_of_boundary (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k
   congr 1
   simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]
 
-/-- For `h : S.RightHomologyData`, this is a restatement of `h.hι `, saying that
+/-- For `h : S.RightHomologyData`, this is a restatement of `h.hι`, saying that
 `ι : h.H ⟶ h.Q` is a kernel of `h.g' : h.Q ⟶ S.X₃`. -/
 def hι' : IsLimit (KernelFork.ofι h.ι h.ι_g') := h.hι
 

diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -156,7 +156,7 @@ See note [reducible non-instances]. -/
 @[reducible]
 def Module.compHom [Semiring S] (f : S →+* R) : Module S M :=
   { MulActionWithZero.compHom M f.toMonoidWithZeroHom, DistribMulAction.compHom M (f : S →* R) with
-    -- Porting note: the `show f (r + s) • x = f r • x + f s • x ` wasn't needed in mathlib3.
+    -- Porting note: the `show f (r + s) • x = f r • x + f s • x` wasn't needed in mathlib3.
     -- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for
     -- use in later fields.  See
     -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication

diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean
@@ -95,7 +95,7 @@ class SemilinearEquivClass (F : Type*) {R S : outParam (Type*)} [Semiring R] [Se
   (σ : outParam <| R →+* S) {σ' : outParam <| S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
   (M M₂ : outParam (Type*)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends
   AddEquivClass F M M₂ where
-  /-- Applying a semilinear equivalence `f` over `σ` to `r • x ` equals `σ r • f x`. -/
+  /-- Applying a semilinear equivalence `f` over `σ` to `r • x` equals `σ r • f x`. -/
   map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x
 #align semilinear_equiv_class SemilinearEquivClass
 

diff --git a/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean b/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
@@ -100,7 +100,7 @@ namespace MorphComponents
 
 variable {X} {n : ℕ} {Z Z' : C} (f : MorphComponents X n Z) (g : X' ⟶ X) (h : Z ⟶ Z')
 
-/-- The morphism `X _[n+1] ⟶ Z ` associated to `f : MorphComponents X n Z`. -/
+/-- The morphism `X _[n+1] ⟶ Z` associated to `f : MorphComponents X n Z`. -/
 def φ {Z : C} (f : MorphComponents X n Z) : X _[n + 1] ⟶ Z :=
   PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P i).f (n + 1) ≫ X.δ i.rev.succ ≫
     f.b (Fin.rev i)

diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
@@ -38,12 +38,12 @@ theorem atImInfty_mem (S : Set ℍ) : S ∈ atImInfty ↔ ∃ A : ℝ, ∀ z :
   simp only [atImInfty_basis.mem_iff, true_and]; rfl
 #align upper_half_plane.at_im_infty_mem UpperHalfPlane.atImInfty_mem
 
-/-- A function ` f : ℍ → α` is bounded at infinity if it is bounded along `atImInfty`. -/
+/-- A function `f : ℍ → α` is bounded at infinity if it is bounded along `atImInfty`. -/
 def IsBoundedAtImInfty {α : Type*} [Norm α] (f : ℍ → α) : Prop :=
   BoundedAtFilter atImInfty f
 #align upper_half_plane.is_bounded_at_im_infty UpperHalfPlane.IsBoundedAtImInfty
 
-/-- A function ` f : ℍ → α` is zero at infinity it is zero along `atImInfty`. -/
+/-- A function `f : ℍ → α` is zero at infinity it is zero along `atImInfty`. -/
 def IsZeroAtImInfty {α : Type*} [Zero α] [TopologicalSpace α] (f : ℍ → α) : Prop :=
   ZeroAtFilter atImInfty f
 #align upper_half_plane.is_zero_at_im_infty UpperHalfPlane.IsZeroAtImInfty

diff --git a/Mathlib/Analysis/Convex/Jensen.lean b/Mathlib/Analysis/Convex/Jensen.lean
@@ -23,7 +23,7 @@ Jensen's inequalities:
 * `ConcaveOn.le_map_centerMass`, `ConcaveOn.le_map_sum`: Concave Jensen's inequality.
 
 As corollaries, we get:
-* `ConvexOn.exists_ge_of_mem_convexHull `: Maximum principle for convex functions.
+* `ConvexOn.exists_ge_of_mem_convexHull`: Maximum principle for convex functions.
 * `ConcaveOn.exists_le_of_mem_convexHull`: Minimum principle for concave functions.
 -/
 

diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -28,7 +28,7 @@ open Finset Set
 
 namespace NNReal
 
-/-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ ` as the
+/-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ` as the
 restriction of the real power function. For `x > 0`, it is equal to `exp (y log x)`. For `x = 0`,
 one sets `0 ^ 0 = 1` and `0 ^ y = 0` for `y ≠ 0`. -/
 noncomputable def rpow (x : ℝ≥0) (y : ℝ) : ℝ≥0 :=

diff --git a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
@@ -40,7 +40,7 @@ open scoped Polynomial
 for `x ≤ 0`. It is a basic building block to construct smooth partitions of unity. Its main property
 is that it vanishes for `x ≤ 0`, it is positive for `x > 0`, and the junction between the two
 behaviors is flat enough to retain smoothness. The fact that this function is `C^∞` is proved in
-`expNegInvGlue.contDiff `. -/
+`expNegInvGlue.contDiff`. -/
 def expNegInvGlue (x : ℝ) : ℝ :=
   if x ≤ 0 then 0 else exp (-x⁻¹)
 #align exp_neg_inv_glue expNegInvGlue

diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -205,7 +205,7 @@ class HasForget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory
 #align category_theory.has_forget₂ CategoryTheory.HasForget₂
 
 /-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance
-`HasForget₂ C `. -/
+`HasForget₂ C`. -/
 @[reducible]
 def forget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C]
     [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] : C ⥤ D :=

diff --git a/Mathlib/CategoryTheory/Endomorphism.lean b/Mathlib/CategoryTheory/Endomorphism.lean
@@ -17,7 +17,7 @@ import Mathlib.GroupTheory.GroupAction.Defs
 Definition and basic properties of endomorphisms and automorphisms of an object in a category.
 
 For each `X : C`, we provide `CategoryTheory.End X := X ⟶ X` with a monoid structure,
-and `CategoryTheory.Aut X := X ≅ X ` with a group structure.
+and `CategoryTheory.Aut X := X ≅ X` with a group structure.
 -/
 
 

diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
@@ -197,7 +197,7 @@ def preservesInitialOfIsIso (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : IsIso f] :
   exact PreservesInitial.ofIsoComparison G
 #align category_theory.limits.preserves_initial_of_is_iso CategoryTheory.Limits.preservesInitialOfIsIso
 
-/-- If there is any isomorphism `⊥ ≅ G.obj ⊥ `, then `G` preserves initial objects. -/
+/-- If there is any isomorphism `⊥ ≅ G.obj ⊥`, then `G` preserves initial objects. -/
 def preservesInitialOfIso (f : ⊥_ D ≅ G.obj (⊥_ C)) : PreservesColimit (Functor.empty C) G :=
   preservesInitialOfIsIso G f.hom
 #align category_theory.limits.preserves_initial_of_iso CategoryTheory.Limits.preservesInitialOfIso

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -532,7 +532,7 @@ abbrev prod (X Y : C) [HasBinaryProduct X Y] :=
   limit (pair X Y)
 #align category_theory.limits.prod CategoryTheory.Limits.prod
 
-/-- If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y ` or
+/-- If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y` or
     `X ⨿ Y`. -/
 abbrev coprod (X Y : C) [HasBinaryCoproduct X Y] :=
   colimit (pair X Y)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -1361,7 +1361,7 @@ def getBinaryBiproductData (P Q : C) [HasBinaryBiproduct P Q] : BinaryBiproductD
   Classical.choice HasBinaryBiproduct.exists_binary_biproduct
 #align category_theory.limits.get_binary_biproduct_data CategoryTheory.Limits.getBinaryBiproductData
 
-/-- A bicone for `P Q ` which is both a limit cone and a colimit cocone. -/
+/-- A bicone for `P Q` which is both a limit cone and a colimit cocone. -/
 def BinaryBiproduct.bicone (P Q : C) [HasBinaryBiproduct P Q] : BinaryBicone P Q :=
   (getBinaryBiproductData P Q).bicone
 #align category_theory.limits.binary_biproduct.bicone CategoryTheory.Limits.BinaryBiproduct.bicone

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean
@@ -1329,7 +1329,7 @@ instance pushout.inr_of_epi {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout
   PushoutCocone.epi_inr_of_is_pushout_of_epi (colimit.isColimit _)
 #align category_theory.limits.pushout.inr_of_epi CategoryTheory.Limits.pushout.inr_of_epi
 
-/-- The map ` X ⨿ Y ⟶ X ⨿[Z] Y` is epi. -/
+/-- The map `X ⨿ Y ⟶ X ⨿[Z] Y` is epi. -/
 instance epi_coprod_to_pushout {C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
     [HasPushout f g] [HasBinaryCoproduct Y Z] :
     Epi (coprod.desc pushout.inl pushout.inr : _ ⟶ pushout f g) :=

diff --git a/Mathlib/CategoryTheory/Subobject/Comma.lean b/Mathlib/CategoryTheory/Subobject/Comma.lean
@@ -17,7 +17,7 @@ and `S : D` as a subtype of the subobjects of `A.right`. We deduce that `Structu
 well-powered if `C` is.
 
 ## Main declarations
-* `StructuredArrow.subobjectEquiv `: the order-equivalence between `Subobject A` and a subtype of
+* `StructuredArrow.subobjectEquiv`: the order-equivalence between `Subobject A` and a subtype of
   `Subobject A.right`.
 
 ## Implementation notes

diff --git a/Mathlib/Combinatorics/Catalan.lean b/Mathlib/Combinatorics/Catalan.lean
@@ -27,7 +27,7 @@ triangulations of convex polygons.
 
 ## Main results
 
-* `catalan_eq_centralBinom_div `: The explicit formula for the Catalan number using the central
+* `catalan_eq_centralBinom_div`: The explicit formula for the Catalan number using the central
   binomial coefficient, `catalan n = Nat.centralBinom n / (n + 1)`.
 
 * `treesOfNodesEq_card_eq_catalan`: The number of binary trees with `n` internal nodes

diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -1682,7 +1682,7 @@ abbrev Hom :=
 #align simple_graph.hom SimpleGraph.Hom
 
 /-- A graph embedding is an embedding `f` such that for vertices `v w : V`,
-`G.Adj (f v) (f w) ↔ G.Adj v w `. Its image is an induced subgraph of G'.
+`G.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'.
 
 The notation `G ↪g G'` represents the type of graph embeddings. -/
 abbrev Embedding :=

diff --git a/Mathlib/Data/Finsupp/ToDFinsupp.lean b/Mathlib/Data/Finsupp/ToDFinsupp.lean
@@ -255,7 +255,7 @@ def finsuppLequivDFinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M]
     map_add' := Finsupp.toDFinsupp_add }
 #align finsupp_lequiv_dfinsupp finsuppLequivDFinsupp
 
--- porting note: `simps` generated as ` ↑(finsuppLequivDFinsupp R).toLinearMap = Finsupp.toDFinsupp`
+-- porting note: `simps` generated as `↑(finsuppLequivDFinsupp R).toLinearMap = Finsupp.toDFinsupp`
 @[simp]
 theorem finsuppLequivDFinsupp_apply_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]
     [∀ m : M, Decidable (m ≠ 0)] [Module R M] :

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
@@ -166,7 +166,7 @@ theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get?
   exacts [id, fun h2 => al (IH h2)]
 #align stream.seq.le_stable Stream'.Seq.le_stable
 
-/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n `. -/
+/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n`. -/
 theorem terminated_stable : ∀ (s : Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n :=
   le_stable
 #align stream.seq.terminated_stable Stream'.Seq.terminated_stable

diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean
@@ -395,7 +395,7 @@ theorem unique_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : 0
 
 end CharP
 
-/-- If `n ≠ 0` in `F`, then ` X ^ n - a` is separable for any `a ≠ 0`. -/
+/-- If `n ≠ 0` in `F`, then `X ^ n - a` is separable for any `a ≠ 0`. -/
 theorem separable_X_pow_sub_C {n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) :
     Separable (X ^ n - C a) :=
   separable_X_pow_sub_C_unit (Units.mk0 a ha) (IsUnit.mk0 (n : F) hn)

diff --git a/Mathlib/Geometry/Manifold/ContMDiff.lean b/Mathlib/Geometry/Manifold/ContMDiff.lean
@@ -16,7 +16,7 @@ basic properties of these notions.
 
 ## Main definitions and statements
 
-Let `M ` and `M'` be two smooth manifolds, with respect to model with corners `I` and `I'`. Let
+Let `M` and `M'` be two smooth manifolds, with respect to model with corners `I` and `I'`. Let
 `f : M → M'`.
 
 * `ContMDiffWithinAt I I' n f s x` states that the function `f` is `Cⁿ` within the set `s`

diff --git a/Mathlib/GroupTheory/GroupAction/Prod.lean b/Mathlib/GroupTheory/GroupAction/Prod.lean
@@ -13,7 +13,7 @@ import Mathlib.GroupTheory.GroupAction.Defs
 This file defines instances for binary product of additive and multiplicative actions and provides
 scalar multiplication as a homomorphism from `α × β` to `β`.
 ## Main declarations
-* `smulMulHom `/`smulMonoidHom `: Scalar multiplication bundled as a multiplicative/monoid
+* `smulMulHom`/`smulMonoidHom`: Scalar multiplication bundled as a multiplicative/monoid
   homomorphism.
 ## See also
 * `Mathlib.GroupTheory.GroupAction.Option`

diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean
@@ -1519,7 +1519,7 @@ theorem map_subtype_le (p' : Submodule R p) : map p.subtype p' ≤ p := by
 #align submodule.map_subtype_le Submodule.map_subtype_le
 
 /-- Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the
-maximal submodule of `p` is just `p `. -/
+maximal submodule of `p` is just `p`. -/
 -- @[simp] -- Porting note: simp can prove this
 theorem map_subtype_top : map p.subtype (⊤ : Submodule R p) = p := by simp
 #align submodule.map_subtype_top Submodule.map_subtype_top

diff --git a/Mathlib/LinearAlgebra/Dimension.lean b/Mathlib/LinearAlgebra/Dimension.lean
@@ -566,7 +566,7 @@ theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) :
 #align mk_eq_mk_of_basis mk_eq_mk_of_basis
 
 /-- Given two bases indexed by `ι` and `ι'` of an `R`-module, where `R` satisfies the invariant
-basis number property, an equiv `ι ≃ ι' `. -/
+basis number property, an equiv `ι ≃ ι'`. -/
 def Basis.indexEquiv (v : Basis ι R M) (v' : Basis ι' R M) : ι ≃ ι' :=
   (Cardinal.lift_mk_eq'.1 <| mk_eq_mk_of_basis v v').some
 #align basis.index_equiv Basis.indexEquiv

diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
@@ -1276,7 +1276,7 @@ variable (R M M₂)
 
 /-- The space of multilinear maps on `∀ (i : Fin (n+1)), M i` is canonically isomorphic to
 the space of linear maps from `M 0` to the space of multilinear maps on
-`∀ (i : Fin n), M i.succ `, by separating the first variable. We register this isomorphism as a
+`∀ (i : Fin n), M i.succ`, by separating the first variable. We register this isomorphism as a
 linear isomorphism in `multilinearCurryLeftEquiv R M M₂`.
 
 The direct and inverse maps are given by `f.uncurryLeft` and `f.curryLeft`. Use these

diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean
@@ -1082,7 +1082,7 @@ namespace ContinuousLinearMap
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F]
 
-/-- Composing `f : Lp ` with `L : E →L[𝕜] F`. -/
+/-- Composing `f : Lp` with `L : E →L[𝕜] F`. -/
 def compLp (L : E →L[𝕜] F) (f : Lp E p μ) : Lp F p μ :=
   L.lipschitz.compLp (map_zero L) f
 #align continuous_linear_map.comp_Lp ContinuousLinearMap.compLp

diff --git a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
@@ -17,12 +17,12 @@ subgroup of a group `G` on `G` itself.
 
 ## Main results
 
-* `MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map `: given a subgroup `Γ` of a
+* `MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_map`: given a subgroup `Γ` of a
   topological group `G`, the pushforward to the coset space `G ⧸ Γ` of the restriction of a both
   left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure
   on `G ⧸ Γ`.
 
-* `MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map `: given a normal subgroup `Γ` of
+* `MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_map`: given a normal subgroup `Γ` of
   a topological group `G`, the pushforward to the quotient group `G ⧸ Γ` of the restriction of
   a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a left-invariant
   measure on `G ⧸ Γ`.

diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
@@ -171,7 +171,7 @@ theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S =
 #align is_cyclotomic_extension.subsingleton_iff IsCyclotomicExtension.subsingleton_iff
 
 /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B`
-is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } ` given by
+is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }` given by
 roots of unity of order in `T`. -/
 theorem union_right [h : IsCyclotomicExtension (S ∪ T) A B] :
     IsCyclotomicExtension T (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}) B := by

diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -181,7 +181,7 @@ distinguished (arbitrary) infinite place, prove that its kernel is the torsion s
 follows that `unitLattice` is a free `ℤ`-module (see `unitLattice_moduleFree `) of rank
 `card (InfinitePlaces K) - 1` (see `unitLattice_rank`). To prove that the `unitLattice` is a full
 `ℤ`-lattice, we need to prove that it is discrete (see `unitLattice_inter_ball_finite`) and that it
-spans the full space over `ℝ` (see ` unitLattice_span_eq_top`); this is the main part of the proof,
+spans the full space over `ℝ` (see `unitLattice_span_eq_top`); this is the main part of the proof,
 see the section `span_top` below for more details.
 -/
 

diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean
@@ -59,7 +59,7 @@ and consequences are derived.
 * `isCountablyGenerated_iff_exists_antitone_basis` : proves a filter is countably generated if and
   only if it admits a basis parametrized by a decreasing sequence of sets indexed by `ℕ`.
 
-* `tendsto_iff_seq_tendsto ` : an abstract version of "sequentially continuous implies continuous".
+* `tendsto_iff_seq_tendsto` : an abstract version of "sequentially continuous implies continuous".
 
 ## Implementation notes
 

diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean
@@ -13,7 +13,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Finset
 # The monotone sequence of partial supremums of a sequence
 
 We define `partialSups : (ℕ → α) → ℕ →o α` inductively. For `f : ℕ → α`, `partialSups f` is
-the sequence `f 0 `, `f 0 ⊔ f 1`, `f 0 ⊔ f 1 ⊔ f 2`, ... The point of this definition is that
+the sequence `f 0`, `f 0 ⊔ f 1`, `f 0 ⊔ f 1 ⊔ f 2`, ... The point of this definition is that
 * it doesn't need a `⨆`, as opposed to `⨆ (i ≤ n), f i` (which also means the wrong thing on
   `ConditionallyCompleteLattice`s).
 * it doesn't need a `⊥`, as opposed to `(Finset.range (n + 1)).sup f`.

diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean
@@ -12,7 +12,7 @@ import Mathlib.Probability.Independence.Kernel
 
 * A family of sets of sets `π : ι → Set (Set Ω)` is independent with respect to a measure `μ` if for
   any finite set of indices `s = {i_1, ..., i_n}`, for any sets `f i_1 ∈ π i_1, ..., f i_n ∈ π i_n`,
-  `μ (⋂ i in s, f i) = ∏ i in s, μ (f i) `. It will be used for families of π-systems.
+  `μ (⋂ i in s, f i) = ∏ i in s, μ (f i)`. It will be used for families of π-systems.
 * A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a
   measure `μ` (typically defined on a finer σ-algebra) if the family of sets of measurable sets they
   define is independent. I.e., `m : ι → MeasurableSpace Ω` is independent with respect to a
@@ -97,7 +97,7 @@ def IndepSets [MeasurableSpace Ω] (s1 s2 : Set (Set Ω)) (μ : Measure Ω := by
 measure `μ` (typically defined on a finer σ-algebra) if the family of sets of measurable sets they
 define is independent. `m : ι → MeasurableSpace Ω` is independent with respect to measure `μ` if
 for any finite set of indices `s = {i_1, ..., i_n}`, for any sets
-`f i_1 ∈ m i_1, ..., f i_n ∈ m i_n`, then `μ (⋂ i in s, f i) = ∏ i in s, μ (f i) `. -/
+`f i_1 ∈ m i_1, ..., f i_n ∈ m i_n`, then `μ (⋂ i in s, f i) = ∏ i in s, μ (f i)`. -/
 def iIndep (m : ι → MeasurableSpace Ω) [MeasurableSpace Ω] (μ : Measure Ω := by volume_tac) :
     Prop :=
   kernel.iIndep m (kernel.const Unit μ) (Measure.dirac () : Measure Unit)