chore(Combinatorics): avoid lazy continuation lines (leanprover-community#37165)

We separate free-standing text that currently is mistakenly attached to the last item of lists.

In `Mathlib/Combinatorics/SimpleGraph/Walks/Counting.lean`, we also indent some continuation lines that seem intentional. We do this in order to resolve any ambiguity regarding intended meaning.

Author: harahu

Mathlib/Combinatorics/Configuration.lean

@@ -28,6 +28,7 @@ This file introduces abstract configurations of points and lines, and proves som
 * `Configuration.HasPoints.card_le`: `HasPoints` implies `|L| ≤ |P|`.
 * `Configuration.HasLines.hasPoints`: `HasLines` and `|P| = |L|` implies `HasPoints`.
 * `Configuration.HasPoints.hasLines`: `HasPoints` and `|P| = |L|` implies `HasLines`.
+
 Together, these four statements say that any two of the following properties imply the third:
 (a) `HasLines`, (b) `HasPoints`, (c) `|P| = |L|`.
 
@@ -64,6 +65,7 @@ instance : Membership (Dual L) (Dual P) :=
   2) there does not exist a point that is on all of the lines,
   3) there is at most one line through any two points,
   4) any two lines have at most one intersection point.
+
   Conditions 3 and 4 are equivalent. -/
 class Nondegenerate : Prop where
   exists_point : ∀ l : L, ∃ p, p ∉ l

Mathlib/Combinatorics/HalesJewett.lean

@@ -263,6 +263,7 @@ instance {α ι κ : Type*} [Nonempty ι] [Inhabited κ] :
 - each line is only one color except possibly at its endpoint
 - the lines all have the same endpoint
 - the colors of the lines are distinct.
+
 Used in the proof `exists_mono_in_high_dimension`. -/
 structure ColorFocused {α ι κ : Type*} (C : (ι → Option α) → κ) where
   /-- The underlying multiset of almost monochromatic lines of a color-focused collection. -/

Mathlib/Combinatorics/SimpleGraph/Walks/Counting.lean

@@ -12,10 +12,10 @@ public import Mathlib.Combinatorics.SimpleGraph.Paths
 
 ## Main definitions
 - `walkLengthTwoEquivCommonNeighbors`: bijective correspondence between walks of length two
-from `u` to `v` and common neighbours of `u` and `v`. Note that `u` and `v` may be the same.
+  from `u` to `v` and common neighbours of `u` and `v`. Note that `u` and `v` may be the same.
 - `finsetWalkLength`: the `Finset` of length-`n` walks from `u` to `v`.
-This is used to give `{p : G.walk u v | p.length = n}` a `Fintype` instance, and it
-can also be useful as a recursive description of this set when `V` is finite.
+  This is used to give `{p : G.walk u v | p.length = n}` a `Fintype` instance, and it
+  can also be useful as a recursive description of this set when `V` is finite.
 
 TODO: should this be extended further?
 -/