chore: remove unintentionally repeated words and characters (#16147)

Mathlib/Algebra/Homology/ComplexShapeSigns.lean

@@ -33,7 +33,7 @@ variable {I₁ I₂ I₃ I₁₂ I₂₃ J : Type*}
 of a total complex functor `HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂` which
 sends `K` to a complex which in degree `i₁₂ : I₁₂` consists of the coproduct
 of the `(K.X i₁).X i₂` such that `π ⟨i₁, i₂⟩ = i₁₂`. -/
-class TotalComplexShape  where
+class TotalComplexShape where
   /-- a map on indices -/
   π : I₁ × I₂ → I₁₂
   /-- the sign of the horizontal differential in the total complex -/

Mathlib/Algebra/Module/Defs.lean

@@ -571,7 +571,7 @@ theorem NoZeroSMulDivisors.int_of_charZero
     NoZeroSMulDivisors ℤ M :=
   ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩
 
-/-- Only a ring of characteristic zero can can have a non-trivial module without additive or
+/-- Only a ring of characteristic zero can have a non-trivial module without additive or
 scalar torsion. -/
 theorem CharZero.of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R := by
   refine ⟨fun {n m h} ↦ ?_⟩

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -881,7 +881,7 @@ def toAddMonoidHom' : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂ where
   map_zero' := by ext; rfl
   map_add' := by intros; ext; rfl
 
-/-- If `M` is the zero module, then  the identity map of `M` is the zero map. -/
+/-- If `M` is the zero module, then the identity map of `M` is the zero map. -/
 @[simp]
 theorem identityMapOfZeroModuleIsZero [Subsingleton M] : id (R := R₁) (M := M) = 0 :=
   Subsingleton.eq_zero id

Mathlib/Analysis/LocallyConvex/Polar.lean

@@ -153,7 +153,7 @@ theorem polar_subMulAction {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m
     obtain ⟨r, hr⟩ := NormedField.exists_lt_norm 𝕜 ‖B x y‖⁻¹
     contrapose! hr
     rw [← one_div, le_div_iff (norm_pos_iff.2 hr)]
-    simpa using  hy _ (SMulMemClass.smul_mem r hx)
+    simpa using hy _ (SMulMemClass.smul_mem r hx)
   · intro h x hx
     simp [h x hx]
 

Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean

@@ -124,7 +124,7 @@ instance hasLimit_parallelPair {V W : SemiNormedGrp.{u}} (f g : V ⟶ W) :
                 show NormedAddGroupHom.compHom (f - g) c.ι = 0 by
                   rw [AddMonoidHom.map_sub, AddMonoidHom.sub_apply, sub_eq_zero]; exact c.condition)
             (fun c => NormedAddGroupHom.ker.incl_comp_lift _ _ _) fun c g h => by
-        -- Porting note: the `simp_rw` was was `rw [← h]` but motive is not type correct in mathlib4
+        -- Porting note: the `simp_rw` was `rw [← h]` but motive is not type correct in mathlib4
               ext x; dsimp; simp_rw [← h]; rfl}
 
 instance : Limits.HasEqualizers.{u, u + 1} SemiNormedGrp :=

Mathlib/CategoryTheory/Functor/FullyFaithful.lean

@@ -240,7 +240,7 @@ variable {D : Type u₂} [Category.{v₂} D] {E : Type u₃} [Category.{v₃} E]
 variable (F F' : C ⥤ D) (G : D ⥤ E)
 
 instance Faithful.comp [F.Faithful] [G.Faithful] :
-    (F ⋙ G).Faithful  where map_injective p := F.map_injective (G.map_injective p)
+    (F ⋙ G).Faithful where map_injective p := F.map_injective (G.map_injective p)
 
 theorem Faithful.of_comp [(F ⋙ G).Faithful] : F.Faithful :=
   -- Porting note: (F ⋙ G).map_injective.of_comp has the incorrect type

Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

@@ -105,7 +105,7 @@ theorem sequentialFunctor_initial_aux (j : J) : ∃ (n : ℕ), sequentialFunctor
   simpa [h] using leOfHom (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose m)
     (sequentialFunctor_obj J m)).choose_spec.choose
 
-instance sequentialFunctor_initial : (sequentialFunctor J).Initial  where
+instance sequentialFunctor_initial : (sequentialFunctor J).Initial where
   out d := by
     obtain ⟨n, (g : (sequentialFunctor J).obj ⟨n⟩ ≤ d)⟩ := sequentialFunctor_initial_aux J d
     have : Nonempty (CostructuredArrow (sequentialFunctor J) d) :=

Mathlib/CategoryTheory/SingleObj.lean

@@ -242,7 +242,7 @@ def toCat : MonCat ⥤ Cat where
   obj x := Cat.of (SingleObj x)
   map {x y} f := SingleObj.mapHom x y f
 
-instance toCat_full : toCat.Full  where
+instance toCat_full : toCat.Full where
   map_surjective := (SingleObj.mapHom _ _).surjective
 
 instance toCat_faithful : toCat.Faithful where

Mathlib/Data/Matroid/Closure.lean

@@ -50,7 +50,7 @@ Its disadvantage is that the statement `X ⊆ M.closure X` is only true provided
 
 Choice (2) has the reverse property: we would have `X ⊆ M.closure X` for all `X`,
 but the condition `M.closure X ⊆ M.E` requires `X ⊆ M.E` to hold.
-It has a couple of other advantages too: is is actually the closure function of a matroid on `α`
+It has a couple of other advantages too: it is actually the closure function of a matroid on `α`
 with ground set `univ` (specifically, the direct sum of `M` and a free matroid on `M.Eᶜ`),
 and because of this, it is an example of a `ClosureOperator` on `α`, which in turn gives access
 to nice existing API for both `ClosureOperator` and `GaloisInsertion`.

Mathlib/GroupTheory/HNNExtension.lean

@@ -348,7 +348,7 @@ theorem unitsSMulGroup_snd (u : ℤˣ) (g : G) :
 variable {d}
 
 /-- `Cancels u w` is a predicate expressing whether `t^u` cancels with some occurence
-of `t^-u` when when we multiply `t^u` by `w`. -/
+of `t^-u` when we multiply `t^u` by `w`. -/
 def Cancels (u : ℤˣ) (w : NormalWord d) : Prop :=
   (w.head ∈ (toSubgroup A B u : Subgroup G)) ∧ w.toList.head?.map Prod.fst = some (-u)
 

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -797,12 +797,12 @@ theorem lift_id (x) : f.lift f.map_units x = x :=
 /-- Given Localization maps `f : M →* N` for a Submonoid `S ⊆ M` and
 `k : M →* Q` for a Submonoid `T ⊆ M`, such that `S ≤ T`, and we have
 `l : M →* A`, the composition of the induced map `f.lift` for `k` with
-the induced map `k.lift` for `l` is equal to the  induced map `f.lift` for `l`. -/
+the induced map `k.lift` for `l` is equal to the induced map `f.lift` for `l`. -/
 @[to_additive
     "Given Localization maps `f : M →+ N` for a Submonoid `S ⊆ M` and
 `k : M →+ Q` for a Submonoid `T ⊆ M`, such that `S ≤ T`, and we have
 `l : M →+ A`, the composition of the induced map `f.lift` for `k` with
-the induced map `k.lift` for `l` is equal to the  induced map `f.lift` for `l`"]
+the induced map `k.lift` for `l` is equal to the induced map `f.lift` for `l`"]
 theorem lift_comp_lift {T : Submonoid M} (hST : S ≤ T) {Q : Type*} [CommMonoid Q]
     (k : LocalizationMap T Q) {A : Type*} [CommMonoid A] {l : M →* A}
     (hl : ∀ w : T, IsUnit (l w)) :

Mathlib/GroupTheory/Perm/Cycle/Type.lean

@@ -417,7 +417,7 @@ theorem rotate_length : rotate v n = v :=
 
 end VectorsProdEqOne
 
--- TODO: Make make the `Finite` version of this theorem the default
+-- TODO: Make the `Finite` version of this theorem the default
 /-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
 `p` in `G`. This is known as Cauchy's theorem. -/
 theorem _root_.exists_prime_orderOf_dvd_card {G : Type*} [Group G] [Fintype G] (p : ℕ)
@@ -452,7 +452,7 @@ theorem _root_.exists_prime_orderOf_dvd_card {G : Type*} [Group G] [Fintype G] (
   · rw [Subtype.ext_iff_val, Subtype.ext_iff_val, hg, hg', v.1.2]
     simp only [v₀, Vector.replicate]
 
--- TODO: Make make the `Finite` version of this theorem the default
+-- TODO: Make the `Finite` version of this theorem the default
 /-- For every prime `p` dividing the order of a finite additive group `G` there exists an element of
 order `p` in `G`. This is the additive version of Cauchy's theorem. -/
 theorem _root_.exists_prime_addOrderOf_dvd_card {G : Type*} [AddGroup G] [Fintype G] (p : ℕ)
@@ -461,7 +461,7 @@ theorem _root_.exists_prime_addOrderOf_dvd_card {G : Type*} [AddGroup G] [Fintyp
 
 attribute [to_additive existing] exists_prime_orderOf_dvd_card
 
--- TODO: Make make the `Finite` version of this theorem the default
+-- TODO: Make the `Finite` version of this theorem the default
 /-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
 `p` in `G`. This is known as Cauchy's theorem. -/
 @[to_additive]

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -423,7 +423,7 @@ Applying this equiv is nicer than rewriting along the equalities, since the type
 -/
 @[to_additive "Let `A', A, B', B` be subgroups of `G`. If `A' = B'` and `A = B`, then the quotients
 `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic. Applying this equiv is nicer than rewriting along
-the equalities, since the type of `(A'.addSubgroupOf A : AddSubgroup A)` depends on on `A`. "]
+the equalities, since the type of `(A'.addSubgroupOf A : AddSubgroup A)` depends on `A`. "]
 def equivQuotientSubgroupOfOfEq {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal]
     [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) :
     A ⧸ A'.subgroupOf A ≃* B ⧸ B'.subgroupOf B :=

Mathlib/LinearAlgebra/PiTensorProduct.lean

@@ -313,7 +313,7 @@ def lifts (x : ⨂[R] i, s i) : Set (FreeAddMonoid (R × Π i, s i)) :=
   {p | AddCon.toQuotient (c := addConGen (PiTensorProduct.Eqv R s)) p = x}
 
 /-- An element `p` of `FreeAddMonoid (R × Π i, s i)` lifts an element `x` of `⨂[R] i, s i`
-if and only if `x` is equal to to the sum of `a • ⨂ₜ[R] i, m i` over all the entries
+if and only if `x` is equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries
 `(a, m)` of `p`.
 -/
 lemma mem_lifts_iff (x : ⨂[R] i, s i) (p : FreeAddMonoid (R × Π i, s i)) :

Mathlib/LinearAlgebra/RootSystem/Basic.lean

@@ -17,7 +17,7 @@ This file contains basic results for root systems and root data.
  * `RootSystem.ext`: In characteristic zero if there is no torsion, a root system is determined
    entirely by its roots.
  * `RootPairing.mk'`: In characteristic zero if there is no torsion, to check that two finite
-   familes of of roots and coroots form a root pairing, it is sufficient to check that they are
+   families of roots and coroots form a root pairing, it is sufficient to check that they are
    stable under reflections.
  * `RootSystem.mk'`: In characteristic zero if there is no torsion, to check that a finite family of
    roots form a root system, we do not need to check that the coroots are stable under reflections
@@ -173,7 +173,7 @@ private lemma coroot_eq_coreflection_of_root_eq' [CharZero R] [NoZeroSMulDivisor
   rw [comp_apply, hl, hk, hij]
   exact (hr i).comp <| (hr j).comp (hr i)
 
-/-- In characteristic zero if there is no torsion, to check that two finite familes of of roots and
+/-- In characteristic zero if there is no torsion, to check that two finite families of roots and
 coroots form a root pairing, it is sufficient to check that they are stable under reflections. -/
 def mk' [Finite ι] [CharZero R] [NoZeroSMulDivisors R M]
     (p : PerfectPairing R M N)

Mathlib/Logic/Godel/GodelBetaFunction.lean

@@ -13,7 +13,7 @@ import Mathlib.Data.Nat.Pairing
 # Gödel's Beta Function Lemma
 
 This file proves Gödel's Beta Function Lemma, used to prove the First Incompleteness Theorem. It
-permits  quantification over finite sequences of natural numbers in formal theories of arithmetic.
+permits quantification over finite sequences of natural numbers in formal theories of arithmetic.
 This Beta Function has no connection with the unrelated Beta Function defined in analysis. Note
 that `Nat.beta` and `Nat.unbeta` provide similar functionality to `Encodable.encodeList` and
 `Encodable.decodeList`. We define these separately, because it is easier to prove that `Nat.beta`

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -1832,7 +1832,7 @@ theorem exists_measurable_le_forall_setLIntegral_eq [SFinite μ] (f : α → ℝ
   have hφle : φ ≤ f := fun x ↦ iSup_le (hgf · x)
   refine ⟨φ, hφm, hφle, fun s ↦ ?_⟩
   -- Now we show the inequality between set integrals.
-  -- Choose a simple function `ψ ≤ f` with values in `ℝ≥0` and prove  for `ψ`.
+  -- Choose a simple function `ψ ≤ f` with values in `ℝ≥0` and prove for `ψ`.
   rw [lintegral_eq_nnreal]
   refine iSup₂_le fun ψ hψ ↦ ?_
   -- Choose `n` such that `ψ x ≤ n` for all `x`.

Mathlib/MeasureTheory/Measure/ContinuousPreimage.lean

@@ -84,7 +84,7 @@ theorem tendsto_measure_symmDiff_preimage_nhds_zero
   -- This is possible, because `K` is a compact set and `s` is an open set.
   filter_upwards [hf, ContinuousMap.tendsto_nhds_compactOpen.mp hfg K hKco s hso hKg] with a hfa ha
   -- Then each of the sets `g ⁻¹' s ∆ K = g ⁻¹' s \ K` and `f a ⁻¹' s ∆ K = f a ⁻¹' s \ K`
-  -- have measure at most `ε / 2`, thus `f a ⁻¹' s ∆ g ⁻¹' s` has measure at  most `ε`.
+  -- have measure at most `ε / 2`, thus `f a ⁻¹' s ∆ g ⁻¹' s` has measure at most `ε`.
   rw [← ENNReal.add_halves ε]
   refine (measure_symmDiff_le _ K _).trans ?_
   rw [symmDiff_of_ge ha.subset_preimage, symmDiff_of_le hKg.subset_preimage]

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -379,7 +379,7 @@ attribute [-instance] Quotient.instMeasurableSpace
   integral of a function `f` on `G` with respect to a right-invariant measure `μ` is equal to the
   integral over the quotient `G ⧸ Γ` of the automorphization of `f`. -/
 @[to_additive "This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of an
-  additive  group `G`, the integral of a function `f` on `G` with respect to a right-invariant
+  additive group `G`, the integral of a function `f` on `G` with respect to a right-invariant
   measure `μ` is equal to the integral over the quotient `G ⧸ Γ` of the automorphization of `f`."]
 lemma QuotientGroup.integral_eq_integral_automorphize {E : Type*} [NormedAddCommGroup E]
     [NormedSpace ℝ E] [μ.IsMulRightInvariant] {f : G → E}

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1346,7 +1346,7 @@ theorem sum_apply (f : ι → Measure α) {s : Set α} (hs : MeasurableSet s) :
 theorem sum_apply₀ (f : ι → Measure α) {s : Set α} (hs : NullMeasurableSet s (sum f)) :
     sum f s = ∑' i, f i s := by
   apply le_antisymm ?_ (le_sum_apply _ _)
-  rcases hs.exists_measurable_subset_ae_eq  with ⟨t, ts, t_meas, ht⟩
+  rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, t_meas, ht⟩
   calc
   sum f s = sum f t := measure_congr ht.symm
   _ = ∑' i, f i t := sum_apply _ t_meas

Mathlib/MeasureTheory/Measure/Regular.lean

@@ -455,7 +455,7 @@ lemma of_restrict {μ : Measure α} {s : ℕ → Set α}
     (h : ∀ n, InnerRegularWRT (μ.restrict (s n)) p MeasurableSet)
     (hs : univ ⊆ ⋃ n, s n) (hmono : Monotone s) : InnerRegularWRT μ p MeasurableSet := by
   intro F hF r hr
-  have hBU : ⋃ n, F ∩ s n = F := by  rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
+  have hBU : ⋃ n, F ∩ s n = F := by rw [← inter_iUnion, univ_subset_iff.mp hs, inter_univ]
   have : μ F = ⨆ n, μ (F ∩ s n) := by
     rw [← measure_iUnion_eq_iSup, hBU]
     exact Monotone.directed_le fun m n h ↦ inter_subset_inter_right _ (hmono h)

Mathlib/NumberTheory/FLT/Three.lean

@@ -116,7 +116,7 @@ private lemma fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 {a b c : 
 
 open Finset Int in
 /--
-  To prove Fermat's Last Theorem for `n = 3`, it is enough to show that that for all `a`, `b`, `c`
+  To prove Fermat's Last Theorem for `n = 3`, it is enough to show that for all `a`, `b`, `c`
   in `ℤ` such that `c ≠ 0`, `¬ 3 ∣ a`, `¬ 3 ∣ b`, `a` and `b` are coprime and `3 ∣ c`, we have
   `a ^ 3 + b ^ 3 ≠ c ^ 3`.
 -/

Mathlib/NumberTheory/LSeries/RiemannZeta.lean

@@ -202,7 +202,7 @@ theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) :
 lemma riemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1) := by
   exact hurwitzZetaEven_residue_one 0
 
-/- naming scheme was changed from from `riemannCompletedZeta` to `completedRiemannZeta`; add
+/- naming scheme was changed from `riemannCompletedZeta` to `completedRiemannZeta`; add
 aliases for the old names -/
 section aliases
 

Mathlib/NumberTheory/NumberField/House.lean

@@ -149,7 +149,7 @@ private theorem asiegel_ne_0 : asiegel K a ≠ 0 := by
 
 variable {p q : ℕ} (h0p : 0 < p) (hpq : p < q) (x : β × (K →+* ℂ) → ℤ) (hxl : x ≠ 0)
 
-/-- `ξ` is the the product of `x (l, r)` and the `r`-th basis element of the newBasis of `K`. -/
+/-- `ξ` is the product of `x (l, r)` and the `r`-th basis element of the newBasis of `K`. -/
 private def ξ : β → 𝓞 K := fun l => ∑ r : K →+* ℂ, x (l, r) * (newBasis K r)
 
 include hxl in

Mathlib/Order/CompleteLattice.lean

@@ -1025,7 +1025,7 @@ lemma le_biSup {ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s)
 
 begin
   apply @le_antisymm,
-  safe, pose h := f a ⊓ g a, begin [smt] ematch, ematch  end
+  safe, pose h := f a ⊓ g a, begin [smt] ematch, ematch end
 end
 -/
 theorem iSup_sup [Nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a := by

Mathlib/Probability/Kernel/Basic.lean

@@ -223,7 +223,7 @@ lemma IsFiniteKernel.integrable (μ : Measure α) [IsFiniteMeasure μ]
     (κ : Kernel α β) [IsFiniteKernel κ] {s : Set β} (hs : MeasurableSet s) :
     Integrable (fun x => (κ x s).toReal) μ := by
   refine Integrable.mono' (integrable_const (IsFiniteKernel.bound κ).toReal)
-    ((κ.measurable_coe  hs).ennreal_toReal.aestronglyMeasurable)
+    ((κ.measurable_coe hs).ennreal_toReal.aestronglyMeasurable)
     (ae_of_all μ fun x => ?_)
   rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg,
     ENNReal.toReal_le_toReal (measure_ne_top _ _) (IsFiniteKernel.bound_ne_top _)]

Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

@@ -12,7 +12,7 @@ import Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
 
 Let `κ : Kernel α (β × ℝ)` and `ν : Kernel α β` be two finite kernels.
 A function `f : α × β → StieltjesFunction` is called a conditional kernel CDF of `κ` with respect
-to `ν` if it is measurable, tends to to 0 at -∞ and to 1 at +∞ for all `p : α × β`,
+to `ν` if it is measurable, tends to 0 at -∞ and to 1 at +∞ for all `p : α × β`,
 `fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and `x : ℝ` and for all measurable
 sets `s : Set β`, `∫ b in s, f (a, b) x ∂(ν a) = (κ a (s ×ˢ Iic x)).toReal`.
 
@@ -24,7 +24,7 @@ denoted by `hf.toKernel f` such that `κ = ν ⊗ₖ hf.toKernel f`.
 Let `κ : Kernel α (β × ℝ)` and `ν : Kernel α β`.
 
 * `ProbabilityTheory.IsCondKernelCDF`: a function `f : α × β → StieltjesFunction` is called
-  a conditional kernel CDF of `κ` with respect to `ν` if it is measurable, tends to to 0 at -∞ and
+  a conditional kernel CDF of `κ` with respect to `ν` if it is measurable, tends to 0 at -∞ and
   to 1 at +∞ for all `p : α × β`, if `fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and
   `x : ℝ` and for all measurable sets `s : Set β`,
   `∫ b in s, f (a, b) x ∂(ν a) = (κ a (s ×ˢ Iic x)).toReal`.
@@ -420,7 +420,7 @@ section IsCondKernelCDF
 variable {f : α × β → StieltjesFunction}
 
 /-- A function `f : α × β → StieltjesFunction` is called a conditional kernel CDF of `κ` with
-respect to `ν` if it is measurable, tends to to 0 at -∞ and to 1 at +∞ for all `p : α × β`,
+respect to `ν` if it is measurable, tends to 0 at -∞ and to 1 at +∞ for all `p : α × β`,
 `fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and `x : ℝ` and for all
 measurable sets `s : Set β`, `∫ b in s, f (a, b) x ∂(ν a) = (κ a (s ×ˢ Iic x)).toReal`. -/
 structure IsCondKernelCDF (f : α × β → StieltjesFunction) (κ : Kernel α (β × ℝ)) (ν : Kernel α β) :

Mathlib/Probability/Kernel/Disintegration/Integral.lean

@@ -187,7 +187,7 @@ lemma setLIntegral_condKernel (hf : Measurable f) {s : Set β}
     ∫⁻ b in s, ∫⁻ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst
       = ∫⁻ x in s ×ˢ t, f x ∂ρ := by
   conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-  rw [setLIntegral_compProd  hf hs ht]
+  rw [setLIntegral_compProd hf hs ht]
 
 @[deprecated (since := "2024-06-29")]
 alias set_lintegral_condKernel := setLIntegral_condKernel

Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

@@ -39,7 +39,7 @@ The file also contains an identification between the definitions in
 1-coboundaries (i.e. `B¹(G, A) := Im(d⁰: A → Fun(G, A))`).
 * `groupCohomology.H2 A`: 2-cocycles (i.e. `Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)`) modulo
 2-coboundaries (i.e. `B²(G, A) := Im(d¹: Fun(G, A) → Fun(G², A))`).
-* `groupCohomology.H1LequivOfIsTrivial`: the isomorphism `H¹(G, A) ≃ Hom(G, A)` when  the
+* `groupCohomology.H1LequivOfIsTrivial`: the isomorphism `H¹(G, A) ≃ Hom(G, A)` when the
 representation on `A` is trivial.
 * `groupCohomology.isoHn` for `n = 0, 1, 2`: an isomorphism
 `groupCohomology A n ≅ groupCohomology.Hn A`.

Mathlib/RingTheory/Polynomial/Hermite/Basic.lean

@@ -116,7 +116,7 @@ theorem hermite_monic (n : ℕ) : (hermite n).Monic :=
   leadingCoeff_hermite n
 
 theorem coeff_hermite_of_odd_add {n k : ℕ} (hnk : Odd (n + k)) : coeff (hermite n) k = 0 := by
-  induction n  generalizing k with
+  induction n generalizing k with
   | zero =>
     rw [zero_add k] at hnk
     exact coeff_hermite_of_lt hnk.pos