diff --git a/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean b/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean
index b524ea708540c1..cee897a3533003 100644
--- a/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean
+++ b/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean
@@ -23,14 +23,14 @@ terms of a quantity that is a root of a particular cubic equation.
 ## Main statements
 
 - `cubic_eq_zero_iff`: gives the roots of the cubic equation
-where the discriminant `p = 3 * a * c - b^2` is nonzero.
+  where the discriminant `p = 3 * a * c - b^2` is nonzero.
 - `cubic_eq_zero_iff_of_p_eq_zero`: gives the roots of the cubic equation
-where the discriminant equals zero.
+  where the discriminant equals zero.
 - `quartic_eq_zero_iff`: gives the roots of the quartic equation
-where the quantity `b^3 - 4 * a * b * c + 8 * a^2 * d` is nonzero, in terms of a root `u`
-to a cubic resolvent.
+  where the quantity `b^3 - 4 * a * b * c + 8 * a^2 * d` is nonzero, in terms of a root `u`
+  to a cubic resolvent.
 - `quartic_eq_zero_iff_of_q_eq_zero`: gives the roots of the quartic equation
-where the quantity `b^3 - 4 * a * b * c + 8 * a^2 * d` equals zero.
+  where the quantity `b^3 - 4 * a * b * c + 8 * a^2 * d` equals zero.
 
 ## Proof outline
 
diff --git a/Counterexamples/NowhereDifferentiable.lean b/Counterexamples/NowhereDifferentiable.lean
index 3fb26d476ce42b..2497df7520bf8f 100644
--- a/Counterexamples/NowhereDifferentiable.lean
+++ b/Counterexamples/NowhereDifferentiable.lean
@@ -24,7 +24,7 @@ which is the original bound given by Karl Weierstrass. There is a better bound $
 ## References
 
 * [Weierstrass, Karl, *Über continuirliche Functionen eines reellen Arguments, die für keinen Werth
-des letzeren einen bestimmten Differentialquotienten besitzen*][weierstrass1895]
+  des letzeren einen bestimmten Differentialquotienten besitzen*][weierstrass1895]
 * [G. H. Hardy, *Weierstrass's Non-Differentiable Function*][hardyweierstrass]
 
 -/
@@ -77,8 +77,8 @@ theorem uniformContinuous_weierstrass {a : ℝ} (ha : a ∈ Set.Ioo 0 1) (b : 
 To show that Weierstrass function $f(x)$ is not differentiable at any $x$, we choose a sequence
 $\{x_m\}$ such that, as $m\to\infty$
  - $\{x_m\}$ converges to $x$
- - The slope $(f(x_m) - f(x)) / (x_m - x)$ grows unbounded
-which means the derivative $f'(x)$ cannot exist.
+ - The slope $(f(x_m) - f(x)) / (x_m - x)$ grows unbounded,
+   which means the derivative $f'(x)$ cannot exist.
 -/
 
 /-- The approximating sequence `seq` is defined as $x_m = \lfloor b^m x + 3/2 \rfloor / b^m$ -/
diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean
index 86999d1284ddc4..8681f5c59bf922 100644
--- a/Mathlib/Combinatorics/HalesJewett.lean
+++ b/Mathlib/Combinatorics/HalesJewett.lean
@@ -51,10 +51,10 @@ allows us to work directly with `α`, `Option α`, `(ι → α) → κ`, and `ι
 ## TODO
 
 - Prove a finitary version of Van der Waerden's theorem (either by compactness or by modifying the
-current proof).
+  current proof).
 
 - One could reformulate the proof of Hales-Jewett to give explicit upper bounds on the number of
-coordinates needed.
+  coordinates needed.
 
 ## Tags
 
diff --git a/Mathlib/Combinatorics/Quiver/Arborescence.lean b/Mathlib/Combinatorics/Quiver/Arborescence.lean
index 38eee9d31ef5dd..fdc13f4cd2c6f6 100644
--- a/Mathlib/Combinatorics/Quiver/Arborescence.lean
+++ b/Mathlib/Combinatorics/Quiver/Arborescence.lean
@@ -20,12 +20,12 @@ that for every `b : V` there is a unique path from `root` to `b`.
 - `Quiver.Arborescence V`: a typeclass asserting that `V` is an arborescence
 - `arborescenceMk`: a convenient way of proving that a quiver is an arborescence
 - `RootedConnected r`: a typeclass asserting that there is at least one path from `r` to `b` for
-every `b`.
+  every `b`.
 - `geodesicSubtree r`: given `[RootedConnected r]`, this is a subquiver of `V` which contains
-just enough edges to include a shortest path from `r` to `b` for every `b`.
+  just enough edges to include a shortest path from `r` to `b` for every `b`.
 - `geodesicArborescence : Arborescence (geodesicSubtree r)`: an instance saying that the geodesic
-subtree is an arborescence. This proves the directed analogue of 'every connected graph has a
-spanning tree'. This proof avoids the use of Zorn's lemma.
+  subtree is an arborescence. This proves the directed analogue of 'every connected graph has a
+  spanning tree'. This proof avoids the use of Zorn's lemma.
 -/
 
 @[expose] public section
diff --git a/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean b/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
index d8e203b752144a..a8b3c60b207bbb 100644
--- a/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
+++ b/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
@@ -20,7 +20,7 @@ We define:
 * `Quiver.IsStronglyConnected V`: every pair of vertices is connected by a (possibly empty) path.
 * `Quiver.IsSStronglyConnected V`: every pair of vertices is connected by a path of positive length.
 * `Quiver.StronglyConnectedComponent V`: the quotient by the equivalence relation “paths in both
-directions”.
+  directions”.
 
 These concepts relate strong and weak connectivity and let us reason about strongly connected
 components in directed graphs.
diff --git a/Mathlib/GroupTheory/GroupAction/Iwasawa.lean b/Mathlib/GroupTheory/GroupAction/Iwasawa.lean
index cf7c00bdad58cf..b0ef5b661a56d0 100644
--- a/Mathlib/GroupTheory/GroupAction/Iwasawa.lean
+++ b/Mathlib/GroupTheory/GroupAction/Iwasawa.lean
@@ -11,9 +11,9 @@ public import Mathlib.GroupTheory.Subgroup.Simple
 
 /-! # Iwasawa criterion for simplicity
 
-- `IwasawaStructure` : the structure underlying the Iwasawa criterion
-For a group `G`, this consists of an action of `G` on a type `α` and,
-for every `a : α`, of a subgroup `T a`, such that the following properties hold:
+- `IwasawaStructure` : the structure underlying the Iwasawa criterion.
+  For a group `G`, this consists of an action of `G` on a type `α` and,
+  for every `a : α`, of a subgroup `T a`, such that the following properties hold:
   - for all `a`, `T a` is commutative
   - for all `g : G` and `a : α`, `T (g • a) = MulAut.conj g • T a`
   - the subgroups `T a` generate `G`
@@ -22,12 +22,12 @@ We then prove two versions of the Iwasawa criterion when
 there is an Iwasawa structure.
 
 - `IwasawaStructure.commutator_le` asserts that if the action of `G` on `α`
-is quasiprimitive, then every normal subgroup that acts nontrivially
-contains `commutator G`
+  is quasiprimitive, then every normal subgroup that acts nontrivially
+  contains `commutator G`.
 
-- `IwasawaStructure.isSimpleGroup` : the Iwasawa criterion for simplicity
-If the action of `G` on `α` is quasiprimitive and faithful,
-and `G` is nontrivial and perfect, then `G` is simple.
+- `IwasawaStructure.isSimpleGroup` : the Iwasawa criterion for simplicity.
+  If the action of `G` on `α` is quasiprimitive and faithful,
+  and `G` is nontrivial and perfect, then `G` is simple.
 
 ## TODO
 
diff --git a/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean b/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
index ec5774b3342c83..2875e6627f672f 100644
--- a/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
+++ b/Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
@@ -13,9 +13,9 @@ public import Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
 Let `G` be a group acting on a type `α`.
 
 * `MulAction.IsMultiplyPreprimitive` :
-The action is said to be `n`-primitive if, for every subset `s :
-Set α` with `n` elements, the actions f `stabilizer G s` on the
-complement of `s` is primitive.
+  The action is said to be `n`-primitive if, for every subset `s :
+  Set α` with `n` elements, the actions f `stabilizer G s` on the
+  complement of `s` is primitive.
 
 * `MulAction.is_zero_preprimitive` : any action is 0-primitive
 
@@ -30,9 +30,9 @@ complement of `s` is primitive.
   ofFixingSubgroup.isMultiplyPreprimitive
 
 * `MulAction.ofFixingSubgroup.isMultiplyPreprimitive`:
-If an action is `s.ncard + m`-primitive, then
-the action of `FixingSubgroup G s` on the complement of `s`
-is `m`-primitive.
+  If an action is `s.ncard + m`-primitive, then
+  the action of `FixingSubgroup G s` on the complement of `s`
+  is `m`-primitive.
 
 -/
 
diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
index ae7e6af13cd367..e8ac492a9c042d 100644
--- a/Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
+++ b/Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
@@ -17,51 +17,51 @@ public import Mathlib.Tactic.Group
 
 Given a `MulAction` of `G` on `α` and `s : Set α`,
 
-* `SubMulAction.ofFixingSubgroup` is the action
+- `SubMulAction.ofFixingSubgroup` is the action
   of `FixingSubgroup G s` on the complement `sᶜ` of `s`.
 
 - We define equivariant maps that relate various of these `SubMulAction`s
-and permit to manipulate them in a relatively smooth way:
+  and permit to manipulate them in a relatively smooth way:
 
   * `SubMulAction.ofFixingSubgroup_equivariantMap`:
-  the identity map from `sᶜ` to `α`, as an equivariant map
-  relative to the injection of `FixingSubgroup G s` into `G`.
+    the identity map from `sᶜ` to `α`, as an equivariant map
+    relative to the injection of `FixingSubgroup G s` into `G`.
 
-  * `SubMulAction.fixingSubgroupInsertEquiv M a s` : the
-  multiplicative equivalence between `fixingSubgroup M (insert a s)`
-  and `fixingSubgroup (stabilizer M a) s`
+  * `SubMulAction.fixingSubgroupInsertEquiv M a s`: the
+    multiplicative equivalence between `fixingSubgroup M (insert a s)`
+    and `fixingSubgroup (stabilizer M a) s`
 
-  * `SubMulAction.ofFixingSubgroup_insert_map` : the equivariant
-  map between `SubMulAction.ofFixingSubgroup M (Set.insert a s)`
-  and `SubMulAction.ofFixingSubgroup (MulAction.stabilizer M a) s`.
+  * `SubMulAction.ofFixingSubgroup_insert_map`: the equivariant
+    map between `SubMulAction.ofFixingSubgroup M (Set.insert a s)`
+    and `SubMulAction.ofFixingSubgroup (MulAction.stabilizer M a) s`.
 
   * `SubMulAction.fixingSubgroupEquivFixingSubgroup`:
-  the multiplicative equivalence between `SubMulAction.ofFixingSubgroup M s`
-  and `SubMulAction.ofFixingSubgroup M t` induced by `g : M`
-  such that `g • t = s`.
+    the multiplicative equivalence between `SubMulAction.ofFixingSubgroup M s`
+    and `SubMulAction.ofFixingSubgroup M t` induced by `g : M`
+    such that `g • t = s`.
 
   * `SubMulAction.conjMap_ofFixingSubgroup`:
-  the equivariant map between `SubMulAction.ofFixingSubgroup M t`
-  and `SubMulAction.ofFixingSubgroup M s`
-  induced by `g : M` such that `g • t = s`.
+    the equivariant map between `SubMulAction.ofFixingSubgroup M t`
+    and `SubMulAction.ofFixingSubgroup M s`
+    induced by `g : M` such that `g • t = s`.
 
   * `SubMulAction.ofFixingSubgroup_of_inclusion`:
-  the identity from `SubMulAction.ofFixingSubgroup M s`
-  to `SubMulAction.ofFixingSubgroup M t`, when `t ⊆ s`,
-  as an equivariant map.
+    the identity from `SubMulAction.ofFixingSubgroup M s`
+    to `SubMulAction.ofFixingSubgroup M t`, when `t ⊆ s`,
+    as an equivariant map.
 
   * `SubMulAction.ofFixingSubgroup_of_singleton`:
-  the identity map from `SubMulAction.ofStabilizer M a`
-  to `SubMulAction.ofFixingSubgroup M {a}`.
+    the identity map from `SubMulAction.ofStabilizer M a`
+    to `SubMulAction.ofFixingSubgroup M {a}`.
 
   * `SubMulAction.ofFixingSubgroup_of_eq`:
-  the identity from `SubMulAction.ofFixingSubgroup M s`
-  to `SubMulAction.ofFixingSubgroup M t`, when `s = t`,
-  as an equivariant map.
+    the identity from `SubMulAction.ofFixingSubgroup M s`
+    to `SubMulAction.ofFixingSubgroup M t`, when `s = t`,
+    as an equivariant map.
 
   * `SubMulAction.ofFixingSubgroup.append`: appends
-  an enumeration of `ofFixingSubgroup M s` at the end
-  of an enumeration of `s`, as an equivariant map.
+    an enumeration of `ofFixingSubgroup M s` at the end
+    of an enumeration of `s`, as an equivariant map.
 
 -/
 
diff --git a/Mathlib/GroupTheory/PushoutI.lean b/Mathlib/GroupTheory/PushoutI.lean
index 84e5d03e441026..11f64625da9763 100644
--- a/Mathlib/GroupTheory/PushoutI.lean
+++ b/Mathlib/GroupTheory/PushoutI.lean
@@ -26,10 +26,10 @@ in the diagram are injective).
 
 - `Monoid.PushoutI.NormalWord`: a normal form for words in the pushout
 - `Monoid.PushoutI.of_injective`: if all the maps in the diagram are injective in a pushout of
-groups then so is `of`
+  groups then so is `of`
 - `Monoid.PushoutI.Reduced.eq_empty_of_mem_range`: For any word `w` in the coproduct,
-if `w` is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then
-`w` itself is not in the image of the base monoid.
+  if `w` is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then
+  `w` itself is not in the image of the base monoid.
 
 ## References
 
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean b/Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
index 0fdcee0c22b67b..e673fec5c210a9 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
@@ -28,7 +28,7 @@ of the simplex.
 * `centroid` is the centroid of a simplex, defined via `Finset.univ.centroid` on its vertices.
 
 * `faceOppositeCentroid` is the centroid of the facet obtained by removing one vertex from the
-simplex.
+  simplex.
 
 * `median` is the line connecting a vertex to the corresponding faceOppositeCentroid.
 
diff --git a/Mathlib/LinearAlgebra/Dual/BaseChange.lean b/Mathlib/LinearAlgebra/Dual/BaseChange.lean
index 2e337a03fa2aed..5ef30558e89e42 100644
--- a/Mathlib/LinearAlgebra/Dual/BaseChange.lean
+++ b/Mathlib/LinearAlgebra/Dual/BaseChange.lean
@@ -17,10 +17,10 @@ public import Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
 If `f : Module.Dual R V` and `Algebra R A`, then
 
 * `Module.Dual.baseChange A f` is the element
-of `Module.Dual A (A ⊗[R] V)` deduced by base change.
+  of `Module.Dual A (A ⊗[R] V)` deduced by base change.
 
 * `Module.Dual.baseChangeHom` is the `R`-linear map
-given by `Module.Dual.baseChange`.
+  given by `Module.Dual.baseChange`.
 
 * `IsBaseChange.dual` : for finite free modules, taking dual commutes with base change.
 
diff --git a/Mathlib/LinearAlgebra/Finsupp/Pi.lean b/Mathlib/LinearAlgebra/Finsupp/Pi.lean
index 224d8fae177bd4..01eaaa07fe3363 100644
--- a/Mathlib/LinearAlgebra/Finsupp/Pi.lean
+++ b/Mathlib/LinearAlgebra/Finsupp/Pi.lean
@@ -14,9 +14,9 @@ public import Mathlib.Algebra.Order.Group.Nat
 
 * `Finsupp.linearEquivFunOnFinite`: `α →₀ β` and `a → β` are equivalent if `α` is finite
 * `FunOnFinite.map`: the map `(X → M) → (Y → M)` induced by a map `f : X ⟶ Y` when
-`X` and `Y` are finite.
+  `X` and `Y` are finite.
 * `FunOnFinite.linearMmap`: the linear map `(X → M) →ₗ[R] (Y → M)` induced
-by a map `f : X ⟶ Y` when `X` and `Y` are finite.
+  by a map `f : X ⟶ Y` when `X` and `Y` are finite.
 
 ## Tags
 
diff --git a/Mathlib/LinearAlgebra/Transvection.lean b/Mathlib/LinearAlgebra/Transvection.lean
index 954ac74803add6..2a79c7b5ae2bab 100644
--- a/Mathlib/LinearAlgebra/Transvection.lean
+++ b/Mathlib/LinearAlgebra/Transvection.lean
@@ -26,7 +26,7 @@ public import Mathlib.LinearAlgebra.Dual.BaseChange
 * `LinearMap.transvections R V`: the set of transvections.
 
 * `LinearEquiv.dilatransvections R V`: the set of linear equivalences
-whose associated linear map is of the form `LinearMap.transvection f v`.
+  whose associated linear map is of the form `LinearMap.transvection f v`.
 
 * `LinearEquiv.transvection.det` shows that it has determinant `1`.
 
diff --git a/Mathlib/RepresentationTheory/FinGroupCharZero.lean b/Mathlib/RepresentationTheory/FinGroupCharZero.lean
index 7c25181515167b..f63a4db79e728c 100644
--- a/Mathlib/RepresentationTheory/FinGroupCharZero.lean
+++ b/Mathlib/RepresentationTheory/FinGroupCharZero.lean
@@ -24,9 +24,9 @@ then every object of `Rep k G` (resp. `FDRep k G`) is injective and projective.
 We also give two simpleness criteria for an object `V` of `FDRep k G`, when `k` is
 an algebraically closed field in which the order of `G` is invertible:
 * `FDRep.simple_iff_end_is_rank_one`: `V` is simple if and only `V ⟶ V` is a `k`-vector
-space of dimension `1`.
+  space of dimension `1`.
 * `FDRep.simple_iff_char_is_norm_one`: when `k` is characteristic zero, `V` is simple
-if and only if `∑ g : G, V.character g * V.character g⁻¹ = Fintype.card G`.
+  if and only if `∑ g : G, V.character g * V.character g⁻¹ = Fintype.card G`.
 
 -/