leanprover-community · grunweg · May 12, 2026
diff --git a/Mathlib/Algebra/Lie/OfAssociative.lean b/Mathlib/Algebra/Lie/OfAssociative.lean
@@ -71,9 +71,9 @@ bracket equal to its ring commutator.
 
 Note that this cannot be a global instance because it would create a diamond when `M = A`,
 specifically we can build two mathematically-different `bracket A A`s:
- 1. `@Ring.bracket A _` which says `⁅a, b⁆ = a * b - b * a`
- 2. `(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket` which says `⁅a, b⁆ = a • b`
-    (and thus `⁅a, b⁆ = a * b`)
+1. `@Ring.bracket A _` which says `⁅a, b⁆ = a * b - b * a`
+2. `(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket` which says `⁅a, b⁆ = a • b`
+  (and thus `⁅a, b⁆ = a * b`)
 
 See note [reducible non-instances] -/
 abbrev LieRingModule.ofAssociativeModule : LieRingModule A M where

diff --git a/Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean b/Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean
@@ -175,8 +175,8 @@ variable [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulS
   [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A]
 
 /-- If `e : G ≃* H` is a multiplicative equivalence between two monoids and
- ` ∀ (a : G) (x : A), a • x = (e a) • x`, then `SkewMonoidAlgebra.domCongr e` is an
-  algebra equivalence between their skew monoid algebras. -/
+` ∀ (a : G) (x : A), a • x = (e a) • x`, then `SkewMonoidAlgebra.domCongr e` is an
+algebra equivalence between their skew monoid algebras. -/
 def domCongrAlg {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = (e a) • x) :
     SkewMonoidAlgebra A G ≃ₐ[k] SkewMonoidAlgebra A H :=
   AlgEquiv.ofLinearEquiv

diff --git a/Mathlib/Analysis/Calculus/ParametricIntegral.lean b/Mathlib/Analysis/Calculus/ParametricIntegral.lean
@@ -233,8 +233,8 @@ theorem hasFDerivAt_integral_of_dominated_of_fderiv_le {F' : H → α → H →L
 open scoped Interval in
 /-- Differentiation under integral of `x ↦ ∫ x in a..b, F x a` at a given point `x₀`, assuming
 `F x₀` is integrable on `(a,b)`, `x ↦ F x a` is differentiable on a neighborhood of `x₀` for ae `a`
- with derivative norm uniformly bounded by an integrable function (the neighborhood is independent
- of `a`), and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
+with derivative norm uniformly bounded by an integrable function (the neighborhood is independent
+of `a`), and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
 theorem hasFDerivAt_integral_of_dominated_of_fderiv_le'' [NormedSpace ℝ H] {μ : Measure ℝ}
     {F : H → ℝ → E} {F' : H → ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (hs : s ∈ 𝓝 x₀)
     (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) <| μ.restrict (Ι a b))

diff --git a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
@@ -276,8 +276,8 @@ lemma isCardinalFiltered_iff_aux₂ {ι : Type w} {j : ι → J} {k : J}
 
 variable (J κ) in
 /-- A category is `κ`-filtered iff
-1) any family of objects of cardinality `< κ` admits a map towards a common object, and
-2) any family of morphisms `j ⟶ k` of cardinality `< κ` (between *fixed* objects
+1. any family of objects of cardinality `< κ` admits a map towards a common object, and
+2. any family of morphisms `j ⟶ k` of cardinality `< κ` (between *fixed* objects
    `j` and `k`) can be coequalized by a suitable morphism `k ⟶ l`.
 -/
 lemma isCardinalFiltered_iff :

diff --git a/Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean b/Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
@@ -241,7 +241,7 @@ noncomputable def D₂.multispanIndex : MultispanIndex (multispanShape W Z) C wh
 variable [HasMulticoequalizer (D₂.multispanIndex W Z)]
 
 /-- The object `succ W Z` is the multicoequalizer of all pairs of morphisms
- `g₁ g₂ : Y ⟶ step W Z` with a `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`. -/
+`g₁ g₂ : Y ⟶ step W Z` with a `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`. -/
 noncomputable abbrev succ := multicoequalizer (D₂.multispanIndex W Z)
 
 /-- The projection from `Z` to the multicoequalizer of all morphisms `g₁ g₂ : Y ⟶ step W Z` with

diff --git a/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean b/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
@@ -275,8 +275,8 @@ include hw hcf
 
 /--
 If `G` is `Kᵣ₊₂`-free and contains a `Wᵣ,ₖ` together with a vertex `x` adjacent to all of its common
- clique vertices then there exist (not necessarily distinct) vertices `a, b, c, d`, one from each of
- the four `r + 1`-cliques of `Wᵣ,ₖ`, none of which are adjacent to `x`.
+clique vertices then there exist (not necessarily distinct) vertices `a, b, c, d`, one from each of
+the four `r + 1`-cliques of `Wᵣ,ₖ`, none of which are adjacent to `x`.
 -/
 private lemma exist_not_adj_of_adj_inter (hW : ∀ ⦃y⦄, y ∈ s ∩ t → G.Adj x y) :
     ∃ a b c d, a ∈ insert w₁ s ∧ ¬ G.Adj x a ∧ b ∈ insert w₂ t ∧ ¬ G.Adj x b ∧ c ∈ insert v s ∧

diff --git a/Mathlib/Dynamics/BirkhoffSum/QuasiMeasurePreserving.lean b/Mathlib/Dynamics/BirkhoffSum/QuasiMeasurePreserving.lean
@@ -39,7 +39,7 @@ theorem birkhoffSum_ae_eq_of_ae_eq (hf : QuasiMeasurePreserving f μ μ) (hφ :
   exact (hf.iterate i).ae (hφ.mono (fun _ h _ => h))
 
 /-- If observables `φ` and `ψ` are `μ`-a.e. equal then the corresponding `birkhoffAverage` are
- `μ`-a.e. equal. -/
+`μ`-a.e. equal. -/
 theorem birkhoffAverage_ae_eq_of_ae_eq (R : Type*) [DivisionSemiring R] [Module R M]
     (hf : QuasiMeasurePreserving f μ μ) (hφ : φ =ᵐ[μ] ψ) n :
     birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n :=

diff --git a/Mathlib/Geometry/Euclidean/Simplex.lean b/Mathlib/Geometry/Euclidean/Simplex.lean
@@ -68,13 +68,13 @@ lemma Equilateral.acuteAngled {s : Simplex ℝ P n} (he : s.Equilateral) : s.Acu
   linarith [Real.pi_pos]
 
 /-- The distance from a vertex to the `centroid` equals `n` times the distance from the `centroid`
- to the corresponding `faceOppositeCentroid`. -/
+to the corresponding `faceOppositeCentroid`. -/
 theorem dist_point_centroid [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
     dist (s.points i) s.centroid = n * dist s.centroid (s.faceOppositeCentroid i) := by
   simp_rw [dist_eq_norm_vsub, s.point_vsub_centroid_eq_smul_vsub i, norm_smul, Real.norm_natCast]
 
 /-- The distance from a vertex to its `faceOppositeCentroid` equals `(n + 1)` times the distance
- from the `centroid` to that `faceOppositeCentroid`. -/
+from the `centroid` to that `faceOppositeCentroid`. -/
 theorem dist_point_faceOppositeCentroid [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
     dist (s.points i) (s.faceOppositeCentroid i) =
     (n + 1) * dist s.centroid (s.faceOppositeCentroid i) := by

diff --git a/Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean b/Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
@@ -72,7 +72,7 @@ theorem centroid_eq_affineCombination (s : Simplex k P n) :
     s.centroid = affineCombination k univ s.points (centroidWeights k univ) := by rfl
 
 /-- The centroid of a simplex does not lie in the affine span of any proper subset of its
- vertices. -/
+vertices. -/
 theorem centroid_notMem_affineSpan_of_ne_univ [CharZero k] (s : Simplex k P n)
     {t : Set (Fin (n + 1))} (ht : t ≠ Set.univ) :
     s.centroid ∉ affineSpan k (s.points '' t) := by
@@ -238,7 +238,7 @@ theorem faceOppositeCentroid_mem_affineSpan_face [CharZero k] (s : Simplex k P n
   centroid_mem_affineSpan (s.faceOpposite i)
 
 /-- The `faceOppositeCentroid` is the affine combination of the complement vertices with equal
- weights `1/n`. -/
+weights `1/n`. -/
 theorem faceOppositeCentroid_eq_affineCombination (s : Affine.Simplex k P n) (i : Fin (n + 1)) :
     s.faceOppositeCentroid i = ((affineCombination k {i}ᶜ s.points) fun _ ↦ (↑n)⁻¹) := by
   unfold faceOppositeCentroid
@@ -250,7 +250,7 @@ theorem faceOppositeCentroid_eq_affineCombination (s : Affine.Simplex k P n) (i
   rfl
 
 /-- The vector from a vertex to the corresponding `faceOppositeCentroid` equals the average of the
- displacements to the other vertices. -/
+displacements to the other vertices. -/
 theorem faceOppositeCentroid_vsub_point_eq_smul_sum_vsub [CharZero k] (s : Affine.Simplex k P n)
     (i : Fin (n + 1)) :
     s.faceOppositeCentroid i -ᵥ (s.points i) = (n : k)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) := by
@@ -318,7 +318,7 @@ theorem faceOppositeCentroid_vsub_faceOppositeCentroid [CharZero k] (s : Affine.
   rw [this, smul_smul, inv_eq_one_div, one_div_mul_cancel (NeZero.ne (n : k)), one_smul]
 
 /-- The vector from a vertex to its `faceOppositeCentroid` is `(n+1)` times the vector from the
- `centroid` to that `faceOppositeCentroid`. -/
+`centroid` to that `faceOppositeCentroid`. -/
 theorem faceOppositeCentroid_vsub_point_eq_smul_vsub [CharZero k] (s : Simplex k P n)
     (i : Fin (n + 1)) :
     s.faceOppositeCentroid i -ᵥ s.points i =
@@ -419,7 +419,7 @@ theorem faceOppositeCentroid_eq_smul_vsub_vadd_point [CharZero k] (s : Simplex k
 section median
 
 /-- The median of a simplex is the line through a vertex and its corresponding
- `faceOppositeCentroid`.
+`faceOppositeCentroid`.
 -/
 def median (s : Simplex k P n) (i : Fin (n + 1)) : AffineSubspace k P :=
   line[k, s.points i, s.faceOppositeCentroid i]

diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean b/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean
@@ -296,8 +296,8 @@ theorem TendstoInDistribution.prodMk_of_tendstoInMeasure_const
     simpa [tendstoInMeasure_iff_norm] using hY
 
 /-- **Slutsky's theorem** for a continuous function: if `X n` converges in distribution to `Z`,
- `Y n` converges in probability to a constant `c`, and `g` is a continuous function, then
- `g (X n, Y n)` converges in distribution to `g (Z, c)`. -/
+`Y n` converges in probability to a constant `c`, and `g` is a continuous function, then
+`g (X n, Y n)` converges in distribution to `g (Z, c)`. -/
 theorem TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const {E' F : Type*}
     {mE' : MeasurableSpace E'} [SeminormedAddCommGroup E'] [SecondCountableTopology E']
     [BorelSpace E']

diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean b/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
@@ -335,7 +335,7 @@ theorem TendstoInMeasure.exists_seq_tendsto_ae' {u : Filter ι} [NeBot u] [IsCou
   exact ⟨ms ∘ ns, hms1.comp hns1.tendsto_atTop, hns2⟩
 
 /-- `TendstoInMeasure` is equivalent to every subsequence having another subsequence
- which converges almost surely. -/
+which converges almost surely. -/
 theorem exists_seq_tendstoInMeasure_atTop_iff [IsFiniteMeasure μ]
     {f : ℕ → α → E} (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) {g : α → E} :
     TendstoInMeasure μ f atTop g ↔

diff --git a/Mathlib/MeasureTheory/Group/Action.lean b/Mathlib/MeasureTheory/Group/Action.lean
@@ -240,19 +240,20 @@ variable (G) {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : Measure
 variable [MeasurableConstSMul G α] in
 /-- Equivalent definitions of a measure invariant under a multiplicative action of a group.
 
-- 0: `SMulInvariantMeasure G α μ`;
+0. `SMulInvariantMeasure G α μ`;
 
-- 1: for every `c : G` and a measurable set `s`, the measure of the preimage of `s` under scalar
-     multiplication by `c` is equal to the measure of `s`;
+1. for every `c : G` and a measurable set `s`, the measure of the preimage of `s` under scalar
+  multiplication by `c` is equal to the measure of `s`;
 
-- 2: for every `c : G` and a measurable set `s`, the measure of the image `c • s` of `s` under
-     scalar multiplication by `c` is equal to the measure of `s`;
+2. for every `c : G` and a measurable set `s`, the measure of the image `c • s` of `s` under
+  scalar multiplication by `c` is equal to the measure of `s`;
 
-- 3, 4: properties 2, 3 for any set, including non-measurable ones;
+3. property 1 for any set, including non-measurable ones;
+4. property 2 for any set, including non-measurable ones;
 
-- 5: for any `c : G`, scalar multiplication by `c` maps `μ` to `μ`;
+5. for any `c : G`, scalar multiplication by `c` maps `μ` to `μ`;
 
-- 6: for any `c : G`, scalar multiplication by `c` is a measure-preserving map. -/
+6. for any `c : G`, scalar multiplication by `c` is a measure-preserving map. -/
 @[to_additive]
 theorem smulInvariantMeasure_tfae :
     List.TFAE

diff --git a/Mathlib/Probability/Kernel/Deterministic.lean b/Mathlib/Probability/Kernel/Deterministic.lean
@@ -122,7 +122,7 @@ theorem IsDeterministic.exists_eq_deterministic [StandardBorelSpace β] (κ : Ke
     exact hf a
 
 /-- The equation of a Positive Markov category: if the composition of two Markov kernels `η ∘ₖ κ` is
- deterministic, the distribution over both `η ∘ₖ κ` and `κ` can be obtained by computing `η ∘ₖ κ`
+deterministic, the distribution over both `η ∘ₖ κ` and `κ` can be obtained by computing `η ∘ₖ κ`
 and `κ` independently. -/
 lemma comp_parallelComp_comp_copy {γ : Type*} [MeasurableSpace γ] {κ : Kernel α β}
     {η : Kernel β γ} [IsMarkovKernel κ] [IsMarkovKernel η] [IsDeterministic (η ∘ₖ κ)] :

diff --git a/Mathlib/RepresentationTheory/Invariants.lean b/Mathlib/RepresentationTheory/Invariants.lean
@@ -106,7 +106,7 @@ variable {ρ σ} in
     simp [hf.isIntertwining]
 
 /-- The invariants of the representation `linHom ρ σ` correspond to intertwining maps
- from `ρ` to `σ`. -/
+from `ρ` to `σ`. -/
 def invariantsEquivIntertwiningMap : (linHom ρ σ).invariants ≃ₗ[k] IntertwiningMap ρ σ where
   toFun f := f.val.intertwiningMap_of_isIntertwiningMap ρ σ
     ((mem_linHom_invariants_iff_isIntertwining f.val).mp f.property).isIntertwining

diff --git a/Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean b/Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean
@@ -643,7 +643,7 @@ private theorem isSubDPIdeal_aux (hIJ : IsSubDPIdeal hI (J ⊓ I)) :
 set_option backward.privateInPublic true in
 set_option backward.privateInPublic.warn false in
 /-- When `I ⊓ J` is a sub-dp-ideal of `I`, this is the divided power structure on the ideal
- `I(A⧸J)` of the quotient. -/
+`I(A⧸J)` of the quotient. -/
 noncomputable def dividedPowers : DividedPowers (I.map (Ideal.Quotient.mk J)) :=
   DividedPowers.Quotient.OfSurjective.dividedPowers
     hI Ideal.Quotient.mk_surjective (refl _) (isSubDPIdeal_aux hI hIJ)

diff --git a/Mathlib/RingTheory/MvPowerSeries/Basic.lean b/Mathlib/RingTheory/MvPowerSeries/Basic.lean
@@ -564,8 +564,8 @@ section toSubring
 variable [Ring R] (p : MvPowerSeries σ R) (T : Subring R) (hp : ∀ n, p.coeff n ∈ T)
 
 /-- Given a multivariate formal power series `p` and a subring `T` that contains the
- coefficients of `p`, return the corresponding multivariate formal power series
- whose coefficients are in `T`. -/
+coefficients of `p`, return the corresponding multivariate formal power series
+whose coefficients are in `T`. -/
 def toSubring : MvPowerSeries σ T := fun n => ⟨p.coeff n, hp n⟩
 
 @[simp]

diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -504,8 +504,8 @@ section toSubring
 variable [Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ n, p.coeff n ∈ T)
 
 /-- Given a formal power series `p` and a subring `T` that contains the
- coefficients of `p`, return the corresponding formal power series
- whose coefficients are in `T`. -/
+coefficients of `p`, return the corresponding formal power series
+whose coefficients are in `T`. -/
 def toSubring : PowerSeries T := mk fun n => ⟨p.coeff n, hp n⟩
 
 @[simp]

diff --git a/Mathlib/Tactic/Algebra/Basic.lean b/Mathlib/Tactic/Algebra/Basic.lean
@@ -401,8 +401,8 @@ variable {u v : Lean.Level} {R : Q(Type u)} {A : Q(Type v)} {sR : Q(CommSemiring
   {sA : Q(CommSemiring $A)} (sAlg : Q(Algebra $R $A)) (a : Q($A)) (b : Q($A))
 
 /-- Infer from the expression what base ring the normalization should use.
- Finds all scalar rings in the expression and picks the 'larger' one in the sense that
- it is an algebra over the smaller rings. -/
+Finds all scalar rings in the expression and picks the 'larger' one in the sense that
+it is an algebra over the smaller rings. -/
 def inferBase (ca : Cache q($sA)) (e : Expr) : MetaM <| Σ u : Lean.Level, Q(Type u) := do
   let rings ← (← collectScalarRings e).mapM getLevelQ'
   let res ← match rings with

diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean
@@ -412,7 +412,7 @@ def splitApply (mvs static : List MVarId) : MetaM ((List MVarId) × (List MVarId
 
 /-- `miscomputedDegree? deg false_goals` takes as input
 *  an `Expr`ession `deg`, representing the degree of a polynomial
-   (i.e. an `Expr`ession of inferred type either `ℕ` or `WithBot ℕ`);
+  (i.e. an `Expr`ession of inferred type either `ℕ` or `WithBot ℕ`);
 *  a list of `MVarId`s `false_goals`.
 
 Although inconsequential for this function, the list of goals `false_goals` reduces to `False`

diff --git a/Mathlib/Tactic/FunProp/Core.lean b/Mathlib/Tactic/FunProp/Core.lean
@@ -367,7 +367,8 @@ For example
   - `funPropDecl` is `FunPropDecl` for `Continuous`
   - `e = q(Continuous fun x ↦ foo (bar x) y)`
   - `fData` contains info on `fun x ↦ foo (bar x) y`
-  This tries to prove `Continuous fun x ↦ foo (bar x) y` from `Continuous fun x ↦ foo (bar x)`
+
+This tries to prove `Continuous fun x ↦ foo (bar x) y` from `Continuous fun x ↦ foo (bar x)`
 -/
 def removeArgRule (funPropDecl : FunPropDecl) (e : Expr) (fData : FunctionData)
     (funProp : Expr → FunPropM (Option Result)) :

diff --git a/Mathlib/Topology/Covering/Basic.lean b/Mathlib/Topology/Covering/Basic.lean
@@ -430,9 +430,9 @@ open Function in
 `V` be an open subset of `X`. Suppose that there is a family `U` of disjoint subsets of `E`
 that covers `f⁻¹(V)` such that for every `i`,
 
- 1. `f` is injective on `Uᵢ`,
- 2. `V` is contained in the image `f(Uᵢ)`,
- 3. the open sets in `V` are determined by their preimages in `Uᵢ`.
+1. `f` is injective on `Uᵢ`,
+2. `V` is contained in the image `f(Uᵢ)`,
+3. the open sets in `V` are determined by their preimages in `Uᵢ`.
 
 Then `f` admits a `Bundle.Trivialization` over the base set `V`. -/
 @[simps source target baseSet] noncomputable def IsOpen.trivializationDiscrete [Nonempty (X → E)]

diff --git a/Mathlib/Topology/EMetricSpace/PairReduction.lean b/Mathlib/Topology/EMetricSpace/PairReduction.lean
@@ -119,7 +119,7 @@ lemma exists_radius_le (t : T) (V : Finset T) (ha : 1 < a) (c : ℝ≥0∞) :
     le_trans (mod_cast Finset.card_filter_le V _) (hr (max r 1) (le_max_left r 1)).le⟩
 
 /-- The log-size radius of `t` in `V` is the smallest natural number n greater than zero such that
- `|{x ∈ V | d(t, x) ≤ nc}| ≤ aⁿ`. -/
+`|{x ∈ V | d(t, x) ≤ nc}| ≤ aⁿ`. -/
 noncomputable
 def logSizeRadius (t : T) (V : Finset T) (a c : ℝ≥0∞) : ℕ :=
   if h : 1 < a then Nat.find (exists_radius_le t V h c) else 0