[Merged by Bors] - doc: add newlines to clarify paragraph breaks

Mathlib/CategoryTheory/Filtered/Basic.lean

@@ -32,6 +32,7 @@ easier to describe than general colimits (and more often preserved by functors).
 
 In this file we show that any functor from a finite category to a filtered category admits a cocone:
 * `cocone_nonempty [FinCategory J] [IsFiltered C] (F : J ⥤ C) : Nonempty (Cocone F)`
+
 More generally,
 for any finite collection of objects and morphisms between them in a filtered category
 (even if not closed under composition) there exists some object `Z` receiving maps from all of them,

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -16,6 +16,7 @@ A lax monoidal functor `F` between monoidal categories `C` and `D`
 is a functor between the underlying categories equipped with morphisms
 * `ε : 𝟙_ D ⟶ F.obj (𝟙_ C)` (called the unit morphism)
 * `μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y)` (called the tensorator, or strength).
+
 satisfying various axioms. This is implemented as a typeclass `F.LaxMonoidal`.
 
 Similarly, we define the typeclass `F.OplaxMonoidal`. For these oplax monoidal functors,

Mathlib/CategoryTheory/Monoidal/Limits/Basic.lean

@@ -15,6 +15,7 @@ When `C` is a monoidal category, the limit functor `lim : (J ⥤ C) ⥤ C` is la
 i.e. there are morphisms
 * `(𝟙_ C) → limit (𝟙_ (J ⥤ C))`
 * `limit F ⊗ limit G ⟶ limit (F ⊗ G)`
+
 satisfying the laws of a lax monoidal functor.
 
 ## TODO

Mathlib/CategoryTheory/NatIso.lean

@@ -14,6 +14,7 @@ For the most part, natural isomorphisms are just another sort of isomorphism.
 
 We provide some special support for extracting components:
 * if `α : F ≅ G`, then `α.app X : F.obj X ≅ G.obj X`,
+
 and building natural isomorphisms from components:
 * ```
   NatIso.ofComponents

Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

@@ -130,6 +130,7 @@ protected theorem mdifferentiableAt (hn : n ≠ 0) {x : M} (hx : x ∈ Φ.source
 such as
 * further continuity and differentiability lemmas
 * refl and trans instances; lemmas between them.
+
 As this declaration is meant for internal use only, we keep it simple. -/
 end PartialDiffeomorph
 end PartialDiffeomorph

Mathlib/Lean/Meta/RefinedDiscrTree/Lookup.lean

@@ -206,12 +206,15 @@ The reason is that types are usually implicit arguments. For example
     This gets extra points for matching `1`
   - `Nat.succ.inj (n m : ℕ) (h : n.succ = m.succ) : n = m`.
     This gets extra points for matching `ℕ`
+
   Clearly, `rfl` is better.
+
 - If we rewrite `|(0 : ℝ)|`, we could find
   - `abs_zero : |(0 : α)| = 0`
     This gets extra points for matching `0`
   - `Real.norm_eq_abs : ∀ (r : ℝ), ‖r‖ = |r|`
     This gets extra points for matching `ℝ`
+
   Clearly, `abs_zero` is better
 
 In both examples, matching the type (`ℕ` or `ℝ`) was not very important for how good

Mathlib/Tactic/ComputeDegree.lean

@@ -19,6 +19,7 @@ Using `compute_degree` when the goal is of one of the seven forms
 *  `natDegree f = d`,
 *  `degree f = d`,
 *  `coeff f d = r`, if `d` is the degree of `f`,
+
 tries to solve the goal.
 It may leave side-goals, in case it is not entirely successful.
 
@@ -53,6 +54,7 @@ Assume that `f : R[X]` is a polynomial with coefficients in a semiring `R` and
 If the goal has the form `natDegree f < d`, then we convert it to two separate goals:
 * `natDegree f ≤ ?_`, on which we apply the following steps;
 * `?_ < d`;
+
 where `?_` is a metavariable that `compute_degree` computes in its process.
 We proceed similarly for `degree f < d`.
 

Mathlib/Tactic/MinImports.lean

@@ -194,6 +194,7 @@ declaration names that are implied by
 * the attributes of `cmd` (if there are any),
 * the identifiers contained in `cmd`,
 * if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`.
+
 The argument `id` is expected to be an identifier.
 It is used either for the internally generated name of a "nameless" `instance` or when parsing
 an identifier representing the name of a declaration.
@@ -217,6 +218,7 @@ module names that are implied by
 * the attributes of `cmd` (if there are any),
 * the identifiers contained in `cmd`,
 * if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`.
+
 The argument `id` is expected to be an identifier.
 It is used either for the internally generated name of a "nameless" `instance` or when parsing
 an identifier representing the name of a declaration.

Mathlib/Tactic/MoveAdd.lean

@@ -379,6 +379,7 @@ def reorderAndSimp (mv : MVarId) (instr : List (Expr × Bool)) :
 * an array of `Expr × Bool × Syntax`, as in the output of `parseArrows`,
 * the `Name` `op` of a binary operation,
 * an `Expr`ession `tgt`.
+
 It unifies each `Expr`ession appearing as a first factor of the array with the atoms
 for the operation `op` in the expression `tgt`, returning
 * the lists of pairs of a matched subexpression with the corresponding `Bool`ean;