diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
index 85df8e6a1e1f3c..62d845f049e668 100644
--- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
+++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
@@ -26,6 +26,7 @@ This file is about Bochner integrals. See the file `AEEqOfLIntegral` for Lebesgu
 All results listed below apply to two functions `f, g`, together with two main hypotheses,
 * `f` and `g` are integrable on all measurable sets with finite measure,
 * for all measurable sets `s` with finite measure, `∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ`.
+
 The conclusion is then `f =ᵐ[μ] g`. The main lemmas are:
 * `ae_eq_of_forall_setIntegral_eq_of_sigmaFinite`: case of a sigma-finite measure.
 * `AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq`: for functions which are
diff --git a/Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean b/Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean
index de6afdc2f24e9a..df91f7a9ea0f7e 100644
--- a/Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean
+++ b/Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean
@@ -33,9 +33,10 @@ We use the filter version to prove that absolutely continuous functions are clos
 * scalar multiplication - `AbsolutelyContinuousOnInterval.const_smul`,
   `AbsolutelyContinuousOnInterval.const_mul`;
 * multiplication - `AbsolutelyContinuousOnInterval.smul`,
-`AbsolutelyContinuousOnInterval.mul`;
+  `AbsolutelyContinuousOnInterval.mul`;
+
 and that absolutely continuous implies uniformly continuous in
-`AbsolutelyContinuousOnInterval.uniformContinuousOn`
+`AbsolutelyContinuousOnInterval.uniformContinuousOn`.
 
 We use the `ε`-`δ` definition to prove that
 * Lipschitz continuous functions are absolutely continuous -
@@ -68,11 +69,11 @@ namespace AbsolutelyContinuousOnInterval
 function that maps the finite sequence of the intervals to the total length of the intervals.
 Details:
 1. Technically the filter is on `ℕ × (ℕ → X × X)`. A finite sequence `uIoc (a i) (b i)`, `i < n`
-is represented by any `E : ℕ × (ℕ → X × X)` which satisfies `E.1 = n` and `E.2 i = (a i, b i)` for
-`i < n`. Its total length is `∑ i ∈ Finset.range n, dist (a i) (b i)`.
+   is represented by any `E : ℕ × (ℕ → X × X)` which satisfies `E.1 = n` and `E.2 i = (a i, b i)`
+   for `i < n`. Its total length is `∑ i ∈ Finset.range n, dist (a i) (b i)`.
 2. For a sequence `G : ℕ → ℕ × (ℕ → X × X)`, convergence of `G` along `totalLengthFilter` means that
-the total length of `G j`, i.e., `∑ i ∈ Finset.range (G j).1, dist ((G j).2 i).1 ((G j).2 i).2)`,
-tends to `0` as `j` tends to infinity.
+   the total length of `G j`, i.e., `∑ i ∈ Finset.range (G j).1, dist ((G j).2 i).1 ((G j).2 i).2)`,
+   tends to `0` as `j` tends to infinity.
 -/
 def totalLengthFilter : Filter (ℕ × (ℕ → X × X)) := Filter.comap
   (fun E ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) (𝓝 0)
diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
index 587ad1e81dc387..871ab43d9d9789 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
@@ -105,19 +105,19 @@ functions :
    like `L1.integral_coe_eq_integral`.
 
 4. Since simple functions are dense in `L¹`,
-```
-univ = closure {s simple}
-     = closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
-     ⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
-     = {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself
-```
-Use `isClosed_property` or `DenseRange.induction_on` for this argument.
+   ```
+   univ = closure {s simple}
+        = closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
+        ⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
+        = {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself
+   ```
+   Use `isClosed_property` or `DenseRange.induction_on` for this argument.
 
 ## Notation
 
 * `α →ₛ E` : simple functions (defined in `Mathlib/MeasureTheory/Function/SimpleFunc.lean`)
 * `α →₁[μ] E` : functions in L1 space, i.e., equivalence classes of integrable functions (defined in
-                `Mathlib/MeasureTheory/Function/LpSpace/Basic.lean`)
+  `Mathlib/MeasureTheory/Function/LpSpace/Basic.lean`)
 * `∫ a, f a ∂μ` : integral of `f` with respect to a measure `μ`
 * `∫ a, f a` : integral of `f` with respect to `volume`, the default measure on the ambient type
 
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index a7948537dbdf45..f0b3ef7ba952d4 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -42,9 +42,11 @@ Linearity:
 - `setToFun_smul_left : setToFun μ (fun s ↦ c • (T s)) (hT.smul c) f = c • setToFun μ T hT f`
 - `setToFun_zero : setToFun μ T hT (0 : α → E) = 0`
 - `setToFun_neg : setToFun μ T hT (-f) = - setToFun μ T hT f`
+
 If `f` and `g` are integrable:
 - `setToFun_add : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g`
 - `setToFun_sub : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g`
+
 If `T` satisfies `∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x`:
 - `setToFun_smul : setToFun μ T hT (c • f) = c • setToFun μ T hT f`
 
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
index 4f6ca7ef7bec40..5f51b4dc260a5b 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
@@ -295,6 +295,7 @@ section ae
 predicate holds for almost every `x : β` and
 - `∅ : Set α`
 - a family of sets generating the σ-algebra of `α`
+
 Moreover, if for almost every `x : β`, the predicate is closed under complements and countable
 disjoint unions, then the predicate holds for almost every `x : β` and all measurable sets of `α`.
 
diff --git a/Mathlib/MeasureTheory/Measure/WithDensity.lean b/Mathlib/MeasureTheory/Measure/WithDensity.lean
index 20256c531e1588..06c802a4635846 100644
--- a/Mathlib/MeasureTheory/Measure/WithDensity.lean
+++ b/Mathlib/MeasureTheory/Measure/WithDensity.lean
@@ -67,6 +67,7 @@ to `+∞` on nonempty sets. Let `s = {x₀}` and `f` the indicator of `sᶜ`. Th
 * `μ.withDensity f s = +∞`. Indeed, this is the infimum of `μ.withDensity f t` over measurable sets
   `t` containing `s`. As `s` is not measurable, such a set `t` contains a point `x ≠ x₀`. Then
   `μ.withDensity f t ≥ μ.withDensity f {x} = ∫⁻ a in {x}, f a ∂μ = μ {x} = +∞`.
+
 One checks that `μ.withDensity f = μ`, while `μ.restrict s` gives zero mass to sets not
 containing `x₀`, and infinite mass to those that contain it. -/