chore(CategoryTheory): fix indentation in markdown lists (leanprover-community#35460)

harahu · harahu · commit 965b9674bee1 · 2026-02-21T19:35:38.000Z
Make sure to also indent subsequent lines of an item: this is required by the markdown specification (though not doc-gen), it expresses intent more clearly, and makes it easier to catch accidental misindentations.
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
@@ -29,8 +29,8 @@ basic facts about them.
 
 - The implication from `AB5` to `AB4` is established in `AB4.ofAB5`.
 - That `HasExactColimitsOfShape J C` is invariant under equivalences in both parameters is shown
-in `HasExactColimitsOfShape.of_domain_equivalence` and
-`HasExactColimitsOfShape.of_codomain_equivalence`.
+  in `HasExactColimitsOfShape.of_domain_equivalence` and
+  `HasExactColimitsOfShape.of_codomain_equivalence`.
 
 ## Remarks
 
diff --git a/Mathlib/CategoryTheory/Abelian/Projective/Ext.lean b/Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
@@ -21,10 +21,10 @@ of the complex `R.complex` and to make computations in the `Ext`-group.
 
 ## TODO
 * Functoriality in `X`: this would involve a morphism `X ⟶ X'`, projective
-resolutions `R` and `R'` of `X` and `X'`, a lift of `X ⟶ X'` as a morphism
-of cochain complexes `R.complex ⟶ R'.complex`; in this context,
-we should be able to compute the precomposition of an element
-`R.extMk f m hm hf : Ext X' Y n` by `X ⟶ X'`.
+  resolutions `R` and `R'` of `X` and `X'`, a lift of `X ⟶ X'` as a morphism
+  of cochain complexes `R.complex ⟶ R'.complex`; in this context,
+  we should be able to compute the precomposition of an element
+  `R.extMk f m hm hf : Ext X' Y n` by `X ⟶ X'`.
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/Cat/ObjectProperty.lean b/Mathlib/CategoryTheory/Bicategory/Functor/Cat/ObjectProperty.lean
@@ -18,10 +18,10 @@ to define a sub-pseudofunctor `P.fullsubcategory : Pseudofunctor B Cat`.
 
 ## TODO (@joelriou)
 * Given a Grothendieck topology `J` on a category `C`, define
-a type class `Pseudofunctor.ObjectProperty.IsLocal P J` extending
-`IsClosedUnderMapObj` saying that if an object locally satisfies
-the property, then it satisfies the property. Assuming this, show that
-`P.fullsubcategory` is a stack if the original pseudofunctor was.
+  a type class `Pseudofunctor.ObjectProperty.IsLocal P J` extending
+  `IsClosedUnderMapObj` saying that if an object locally satisfies
+  the property, then it satisfies the property. Assuming this, show that
+  `P.fullsubcategory` is a stack if the original pseudofunctor was.
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean b/Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean
@@ -27,10 +27,10 @@ unitary).
 
 ## TODOs
 * Define lax-composable (resp. pseudo-composable) arrows as strictly unitary
-lax (resp. pseudo-) functors out of `LocallyDiscrete Fin n`.
+  lax (resp. pseudo-) functors out of `LocallyDiscrete Fin n`.
 * Define identity-component oplax natural transformations ("icons") between
-strictly unitary pseudofunctors and construct a bicategory structure on
-bicategories, strictly unitary pseudofunctors and icons.
+  strictly unitary pseudofunctors and construct a bicategory structure on
+  bicategories, strictly unitary pseudofunctors and icons.
 * Construct the Duskin nerve of a bicategory using lax-composable arrows
 * Construct the 2-nerve of a bicategory using pseudo-composable arrows
 
diff --git a/Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean b/Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean
@@ -18,6 +18,7 @@ lax functors):
 * lax natural transformations;
 * oplax natural transformations;
 * strong natural transformations.
+
 These differ in the direction (and invertibility) of the 2-morphisms involved in the naturality
 condition.
 
@@ -46,7 +47,7 @@ We also provide API for going between lax transformations and strong transformat
 
 ## References
 * [Niles Johnson, Donald Yau, *2-Dimensional Categories*](https://arxiv.org/abs/2002.06055),
-section 4.2.
+  section 4.2.
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Conj.lean b/Mathlib/CategoryTheory/Conj.lean
@@ -17,10 +17,10 @@ An isomorphism `α : X ≅ Y` defines
   `CategoryTheory.Iso.conj : End X ≃* End Y` by `α.conj f = α.inv ≫ f ≫ α.hom`;
 - a group isomorphism `CategoryTheory.Iso.conjAut : Aut X ≃* Aut Y` by
   `α.conjAut f = α.symm ≪≫ f ≪≫ α`
-using
-`CategoryTheory.Iso.homCongr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)`
-and `CategoryTheory.Iso.isoCongr : (f : X₁ ≅ X₂) → (g : Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂)`
-which are defined in  `CategoryTheory.HomCongr`.
+  using
+  `CategoryTheory.Iso.homCongr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁)`
+  and `CategoryTheory.Iso.isoCongr : (f : X₁ ≅ X₂) → (g : Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂)`
+  which are defined in  `CategoryTheory.HomCongr`.
 -/
 
 @[expose] public section
diff --git a/Mathlib/CategoryTheory/Distributive/Monoidal.lean b/Mathlib/CategoryTheory/Distributive/Monoidal.lean
@@ -40,7 +40,7 @@ A distributive monoidal category is a monoidal category that is both left and ri
   in the functor categories is computed pointwise.
 
 - We show that any preadditive monoidal category with coproducts is distributive. This includes the
-examples of abelian groups, R-modules, and vector bundles.
+  examples of abelian groups, R-modules, and vector bundles.
 
 ## TODO
 
diff --git a/Mathlib/CategoryTheory/FiberedCategory/Fibered.lean b/Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
@@ -16,11 +16,11 @@ This file defines what it means for a functor `p : 𝒳 ⥤ 𝒮` to be (pre)fib
 ## Main definitions
 
 - `IsPreFibered p` expresses `𝒳` is fibered over `𝒮` via a functor `p : 𝒳 ⥤ 𝒮`, as in SGA VI.6.1.
-This means that any morphism in the base `𝒮` can be lifted to a Cartesian morphism in `𝒳`.
+  This means that any morphism in the base `𝒮` can be lifted to a Cartesian morphism in `𝒳`.
 
 - `IsFibered p` expresses `𝒳` is fibered over `𝒮` via a functor `p : 𝒳 ⥤ 𝒮`, as in SGA VI.6.1.
-This means that it is prefibered, and that the composition of any two Cartesian morphisms is
-Cartesian.
+  This means that it is prefibered, and that the composition of any two Cartesian morphisms is
+  Cartesian.
 
 In the literature one often sees the notion of a fibered category defined as the existence of
 strongly Cartesian morphisms lying over any given morphism in the base. This is equivalent to the
diff --git a/Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean b/Mathlib/CategoryTheory/Functor/Derived/Adjunction.lean
@@ -27,7 +27,7 @@ that `F' ⋙ G'` is the right derived functor of `F ⋙ L₁ ⋙ G'`).
 ## References
 
 * [Georges Maltsiniotis, *Le théorème de Quillen, d'adjonction des
-foncteurs dérivés, revisité*][Maltsiniotis2007]
+  foncteurs dérivés, revisité*][Maltsiniotis2007]
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean b/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@@ -27,8 +27,8 @@ along the localization functor `L`.
 ## TODO
 
 - refactor `Functor.rightDerived` (and `Functor.leftDerived`) when the necessary
-material enters mathlib: derived categories, injective/projective derivability
-structures, existence of derived functors from derivability structures.
+  material enters mathlib: derived categories, injective/projective derivability
+  structures, existence of derived functors from derivability structures.
 
 ## References
 
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean b/Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean
@@ -23,7 +23,7 @@ corresponding property `isDenseAt F` of objects of `D`.
 
 * formalize dense subcategories
 * show the presheaves of types are canonical colimits relatively
-to the Yoneda embedding
+  to the Yoneda embedding
 
 ## References
 * https://ncatlab.org/nlab/show/dense+functor
diff --git a/Mathlib/CategoryTheory/Grothendieck.lean b/Mathlib/CategoryTheory/Grothendieck.lean
@@ -34,10 +34,10 @@ where morphisms consist again of `β : b ⟶ b'` and `φ : f ⟶ (G.map (op β))
 
 - `Grothendieck F` is the Grothendieck construction.
 - Elements of `Grothendieck F` whose base is `c : C` can be transported along `f : c ⟶ d` using
-`transport`.
+  `transport`.
 - A natural transformation `α : F ⟶ G` induces `map α : Grothendieck F ⥤ Grothendieck G`.
 - The Grothendieck construction and `map` together form a functor (`functor`) from the functor
-category `E ⥤ Cat` to the over category `Over E`.
+  category `E ⥤ Cat` to the over category `Over E`.
 - A functor `G : D ⥤ C` induces `pre F G : Grothendieck (G ⋙ F) ⥤ Grothendieck F`.
 
 ## References
diff --git a/Mathlib/CategoryTheory/GuitartExact/Basic.lean b/Mathlib/CategoryTheory/GuitartExact/Basic.lean
@@ -38,8 +38,8 @@ derived functors.
 ## TODO
 
 * Define the notion of derivability structure from
-[the paper by Kahn and Maltsiniotis][KahnMaltsiniotis2008] using Guitart exact squares
-and construct (pointwise) derived functors using this notion
+  [the paper by Kahn and Maltsiniotis][KahnMaltsiniotis2008] using Guitart exact squares
+  and construct (pointwise) derived functors using this notion
 
 ## References
 * https://ncatlab.org/nlab/show/exact+square
diff --git a/Mathlib/CategoryTheory/HomCongr.lean b/Mathlib/CategoryTheory/HomCongr.lean
@@ -20,7 +20,7 @@ As corollaries, an isomorphism `α : X ≅ Y` defines
   `CategoryTheory.Iso.conj : End X ≃* End Y` by `α.conj f = α.inv ≫ f ≫ α.hom`;
 - a group isomorphism `CategoryTheory.Iso.conjAut : Aut X ≃* Aut Y` by
   `α.conjAut f = α.symm ≪≫ f ≪≫ α`
-which can be found in  `CategoryTheory.Conj`.
+  which can be found in  `CategoryTheory.Conj`.
 -/
 
 @[expose] public section
diff --git a/Mathlib/CategoryTheory/Idempotents/Basic.lean b/Mathlib/CategoryTheory/Idempotents/Basic.lean
@@ -17,15 +17,15 @@ preadditive categories).
 ## Main definitions
 
 - `IsIdempotentComplete C` expresses that `C` is idempotent complete, i.e.
-all idempotents in `C` split. Other characterisations of idempotent completeness are given
-by `isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent` and
-`isIdempotentComplete_iff_idempotents_have_kernels`.
+  all idempotents in `C` split. Other characterisations of idempotent completeness are given
+  by `isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent` and
+  `isIdempotentComplete_iff_idempotents_have_kernels`.
 - `isIdempotentComplete_of_abelian` expresses that abelian categories are
-idempotent complete.
+  idempotent complete.
 - `isIdempotentComplete_iff_ofEquivalence` expresses that if two categories `C` and `D`
-are equivalent, then `C` is idempotent complete iff `D` is.
+  are equivalent, then `C` is idempotent complete iff `D` is.
 - `isIdempotentComplete_iff_opposite` expresses that `Cᵒᵖ` is idempotent complete
-iff `C` is.
+  iff `C` is.
 
 ## References
 * [Stacks: Karoubian categories] https://stacks.math.columbia.edu/tag/09SF
diff --git a/Mathlib/CategoryTheory/Idempotents/Karoubi.lean b/Mathlib/CategoryTheory/Idempotents/Karoubi.lean
@@ -17,9 +17,9 @@ In this file, we define the Karoubi envelope `Karoubi C` of a category `C`.
 ## Main constructions and definitions
 
 - `Karoubi C` is the Karoubi envelope of a category `C`: it is an idempotent
-complete category. It is also preadditive when `C` is preadditive.
+  complete category. It is also preadditive when `C` is preadditive.
 - `toKaroubi C : C ⥤ Karoubi C` is a fully faithful functor, which is an equivalence
-(`toKaroubiIsEquivalence`) when `C` is idempotent complete.
+  (`toKaroubiIsEquivalence`) when `C` is idempotent complete.
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean
@@ -19,10 +19,10 @@ is a colimit of representables. This result is also known as the density theorem
 the co-Yoneda lemma and the Ninja Yoneda lemma. Three formulations are given:
 * `colimitOfRepresentable` uses the category of elements of a functor to types;
 * `isColimitTautologicalCocone` uses the category of costructured arrows
-for `yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁`;
+  for `yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁`;
 * `isColimitTautologicalCocone'` uses the category of costructured arrows
-for `uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁`, when the presheaf has values
-in `Type (max w v₁)`;
+  for `uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁`, when the presheaf has values
+  in `Type (max w v₁)`;
 
 In this file, we also study the left Kan extensions of functors `A : C ⥤ ℰ`
 along the Yoneda embedding `uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂`
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equifibered.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equifibered.lean
@@ -14,13 +14,13 @@ public import Mathlib.CategoryTheory.MorphismProperty.Composition
 
 ## Main definition
 - `CategoryTheory.NatTrans.Equifibered`:
-A natural transformation `α : F ⟶ G` is equifibered if every commutative square of the following
-form is a pullback.
-```
-F(X) → F(Y)
- ↓      ↓
-G(X) → G(Y)
-```
+  A natural transformation `α : F ⟶ G` is equifibered if every commutative square of the following
+  form is a pullback.
+  ```
+  F(X) → F(Y)
+   ↓      ↓
+  G(X) → G(Y)
+  ```
 - `CategoryTheory.NatTrans.Coequifibered`: The dual notion.
 
 -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Kernels.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Kernels.lean
@@ -21,9 +21,9 @@ l|      |r
     b
 ```
 * If this is a pullback square, then the induced map `kernel t ⟶ kernel b`
-is an isomorphism.
+  is an isomorphism.
 * If this is a pushout square, then the induced map `cokernel t ⟶ cokernel b`
-is an isomorphism.
+  is an isomorphism.
 
 (Similar results for the (co)kernels of the vertical maps can be obtained
 by applying these results to the flipped square.)
diff --git a/Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean b/Mathlib/CategoryTheory/LocallyCartesianClosed/ChosenPullbacksAlong.lean
@@ -24,7 +24,7 @@ public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
 - We prove that `ChosenPullbacksAlong` has good closure properties: isos have chosen pullbacks,
   and composition of morphisms with chosen pullbacks have chosen pullbacks.
 
--  We prove that chosen pullbacks yields usual pullbacks: `ChosenPullbacksAlong.isPullback`
+- We prove that chosen pullbacks yield usual pullbacks: `ChosenPullbacksAlong.isPullback`
   proves that for morphisms `f` and `g` with the same codomain, the object
   `ChosenPullbacksAlong.pullbackObj f g` together with morphisms
   `ChosenPullbacksAlong.fst f g` and `ChosenPullbacksAlong.snd f g` form a pullback square
diff --git a/Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean b/Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean
@@ -19,11 +19,11 @@ where the tensor product of `F` and `G` is the functor `x ↦ F.obj x ⊗ G.obj
 
 ## TODOs
 - Given a `LawfulDayConvolutionMonoidalCategoryStruct C V D`, show that
-ι induces a monoidal functor `D ⥤ (C ⊛⥤ V)`.
+  ι induces a monoidal functor `D ⥤ (C ⊛⥤ V)`.
 - Specialize to the case `V := Type _`, and prove a universal property stating
-that for every monoidal category `W` with suitable colimits,
-colimit-preserving monoidal functors `(Cᵒᵖ ⊛⥤ Type u) ⥤ W` are equivalent to
-monoidal functors `C ⥤ W`. Show that the Yoneda embedding is monoidal.
+  that for every monoidal category `W` with suitable colimits,
+  colimit-preserving monoidal functors `(Cᵒᵖ ⊛⥤ Type u) ⥤ W` are equivalent to
+  monoidal functors `C ⥤ W`. Show that the Yoneda embedding is monoidal.
 -/
 
 @[expose] public section
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Representable.lean b/Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@@ -55,7 +55,7 @@ Given `hf : relativelyRepresentable f`, with `f : X ⟶ Y` and `g : F.obj a ⟶
   pullback of `f` and `g`.
 * `hf.snd g` is the morphism `hf.pullback g ⟶ F.obj a`
 * `hf.fst g` is the morphism `F.obj (hf.pullback g) ⟶ X`
-*  If `F` is full, and `f` is of type `F.obj c ⟶ G`, we also have `hf.fst' g : hf.pullback g ⟶ X`
+* If `F` is full, and `f` is of type `F.obj c ⟶ G`, we also have `hf.fst' g : hf.pullback g ⟶ X`
   which is the preimage under `F` of `hf.fst g`.
 * `hom_ext`, `hom_ext'`, `lift`, `lift'` are variants of the universal property of
   `F.obj (hf.pullback g)`, where as much as possible has been formulated internally to `C`.
diff --git a/Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean b/Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean
@@ -37,12 +37,12 @@ to `limitsOfShape` in the opposite category `Cᵒᵖ` and vice versa.
 ## TODO
 
 * refactor `ObjectProperty.ind` by saying that it is the supremum
-of `P.colimitsOfShape J` for a filtered category `J`
-(generalize also to `κ`-filtered categories?)
+  of `P.colimitsOfShape J` for a filtered category `J`
+  (generalize also to `κ`-filtered categories?)
 * formalize the closure of `P` under finite colimits (which require
-iterating over `ℕ`), and more generally the closure under colimits
-indexed by a category whose type of arrows has a cardinality
-that is bounded by a certain regular cardinal (@joelriou)
+  iterating over `ℕ`), and more generally the closure under colimits
+  indexed by a category whose type of arrows has a cardinality
+  that is bounded by a certain regular cardinal (@joelriou)
 
 -/
 
diff --git a/Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean b/Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean
@@ -33,9 +33,9 @@ By requiring `P.limitsOfShape J ≤ P`, we introduce a typeclass
 ## TODO
 
 * formalize the closure of `P` under finite limits (which require
-iterating over `ℕ`), and more generally the closure under limits
-indexed by a category whose type of arrows has a cardinality
-that is bounded by a certain regular cardinal (@joelriou)
+  iterating over `ℕ`), and more generally the closure under limits
+  indexed by a category whose type of arrows has a cardinality
+  that is bounded by a certain regular cardinal (@joelriou)
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean b/Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean
@@ -22,13 +22,13 @@ is an isomorphism iff `Z` belongs to `W.isLocal` (see the lemma `isIso_toSucc_if
 The morphism `toSucc W Z : Z ⟶ succ W Z` is defined as a composition
 of two morphisms that are roughly described as follows:
 * `toStep W Z : Z ⟶ step W Z`: for any morphism `f : X ⟶ Y` satisfying `W`
-and any morphism `X ⟶ Z`, we "attach" a morphism `Y ⟶ step W Z` (using
-coproducts and a pushout in essentially the same way as it is done in
-the file `Mathlib/CategoryTheory/SmallObject/Construction.lean` for the small object
-argument);
+  and any morphism `X ⟶ Z`, we "attach" a morphism `Y ⟶ step W Z` (using
+  coproducts and a pushout in essentially the same way as it is done in
+  the file `Mathlib/CategoryTheory/SmallObject/Construction.lean` for the small object
+  argument);
 * `fromStep W Z : step W Z ⟶ succ W Z`: this morphism coequalizes all pairs
-of morphisms `g₁ g₂ : Y ⟶ step W Z` such that there is a `f : X ⟶ Y`
-satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.
+  of morphisms `g₁ g₂ : Y ⟶ step W Z` such that there is a `f : X ⟶ Y`
+  satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.
 
 The morphism `toSucc W Z : Z ⟶ succ W Z` is a variant of the (wrong) definition
 p. 32 in the book by Adámek and Rosický. In this book, a slightly different object
@@ -48,9 +48,9 @@ of morphisms in a locally `κ`-presentable category `C` (with `κ : Cardinal.{w}
 a regular cardinal) such that the domains and codomains of the morphisms
 satisfying `W` are `κ`-presentable:
 * `MorphismProperty.isRightAdjoint_ι_isLocal`: existence of the left adjoint
-of the inclusion `W.isLocal ⥤ C`;
+  of the inclusion `W.isLocal ⥤ C`;
 * `MorphismProperty.isLocallyPresentable_isLocal`: the full subcategory
-`W.isLocal` is locally presentable.
+  `W.isLocal` is locally presentable.
 
 This is essentially the implication (i) → (ii) in Theorem 1.39 (and the corollary 1.40)
 in the book by Adámek and Rosický (note that according to the
diff --git a/Mathlib/CategoryTheory/Shift/Adjunction.lean b/Mathlib/CategoryTheory/Shift/Adjunction.lean
@@ -34,11 +34,11 @@ the compatibility condition on `adj.unit` for a fixed `a` in `A` and for isomorp
 `e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`. We then prove that:
 - If `e₁` and `e₂` satisfy this condition, then `e₁` uniquely determines `e₂` and vice versa.
 - If `a = 0`, the isomorphisms `Functor.CommShift.isoZero F` and `Functor.CommShift.isoZero G`
-satisfy the condition.
+  satisfy the condition.
 - The condition is stable by addition on `A`, if we use `Functor.CommShift.isoAdd` to deduce
-commutation isomorphism for `a + b` from such isomorphism from `a` and `b`.
+  commutation isomorphism for `a + b` from such isomorphism from `a` and `b`.
 - Given commutation isomorphisms for `F`, our candidate commutation isomorphisms for `G`,
-constructed in `Adjunction.RightAdjointCommShift.iso`, satisfy the compatibility condition.
+  constructed in `Adjunction.RightAdjointCommShift.iso`, satisfy the compatibility condition.
 
 Once we have established all this, the compatibility of the commutation isomorphism for
 `F` expressed in `CommShift.zero` and `CommShift.add` immediately implies the similar
diff --git a/Mathlib/CategoryTheory/Shift/CommShiftTwo.lean b/Mathlib/CategoryTheory/Shift/CommShiftTwo.lean
@@ -26,9 +26,9 @@ a `TwistShiftData` structure (see the file `Mathlib.CategoryTheory.Shift.Twist`)
 
 ## TODO (@joelriou)
 * Show that `G : C₁ ⥤ C₂ ⥤ D` satisfies `Functor.CommShift₂Int` iff the uncurried
-functor `C₁ × C₂ ⥤ D` commutes with the shift by `ℤ × ℤ`, where `C₁ × C₂` is
-equipped with the obvious product shift, and `D` is equipped with
-the twisted shift.
+  functor `C₁ × C₂ ⥤ D` commutes with the shift by `ℤ × ℤ`, where `C₁ × C₂` is
+  equipped with the obvious product shift, and `D` is equipped with
+  the twisted shift.
 
 -/
 
diff --git a/Mathlib/CategoryTheory/Sites/CoverPreserving.lean b/Mathlib/CategoryTheory/Sites/CoverPreserving.lean
@@ -25,8 +25,8 @@ Then, a cover-preserving and compatible-preserving functor is continuous.
 ## Main results
 
 - `CategoryTheory.isContinuous_of_coverPreserving`: If `G : C ⥤ D` is
-cover-preserving and compatible-preserving, then `G` is a continuous functor,
-i.e. `G.op ⋙ -` as a functor `(Dᵒᵖ ⥤ A) ⥤ (Cᵒᵖ ⥤ A)` of presheaves maps sheaves to sheaves.
+  cover-preserving and compatible-preserving, then `G` is a continuous functor,
+  i.e. `G.op ⋙ -` as a functor `(Dᵒᵖ ⥤ A) ⥤ (Cᵒᵖ ⥤ A)` of presheaves maps sheaves to sheaves.
 
 ## References
 
diff --git a/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean b/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean
diff --git a/Mathlib/CategoryTheory/Sites/SheafHom.lean b/Mathlib/CategoryTheory/Sites/SheafHom.lean
diff --git a/Mathlib/CategoryTheory/Subobject/ArtinianObject.lean b/Mathlib/CategoryTheory/Subobject/ArtinianObject.lean
diff --git a/Mathlib/CategoryTheory/Triangulated/SpectralObject.lean b/Mathlib/CategoryTheory/Triangulated/SpectralObject.lean
