feat(1000): fill in more entries (#20470)

---
<!-- The text above the `---` will become the commit message when your
PR is merged. Please leave a blank newline before the `---`, otherwise
GitHub will format the text above it as a title.

For details on the "pull request lifecycle" in mathlib, please see:
https://leanprover-community.github.io/contribute/index.html

In particular, note that most reviewers will only notice your PR
if it passes the continuous integration checks.
Please ask for help on https://leanprover.zulipchat.com if needed.

To indicate co-authors, include lines at the bottom of the commit
message
(that is, before the `---`) using the following format:

Co-authored-by: Author Name <[email protected]>

If you are moving or deleting declarations, please include these lines
at the bottom of the commit message
(that is, before the `---`) using the following format:

Moves:
- Vector.* -> List.Vector.*
- ...

Deletions:
- Nat.bit1_add_bit1
- ...

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]

-->

[![Open in
Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

---------

Co-authored-by: Rémy Degenne <[email protected]>

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -63,10 +63,10 @@ local notation "absR" => abs
 -- FIXME this monolithic proof causes a deterministic timeout with `-T50000`
 -- It should be broken in a sequence of more manageable pieces,
 -- perhaps with individual statements for the three steps below.
-/-- Existence of minimizers
+/-- **Existence of minimizers**, aka the **Hilbert projection theorem**.
+
 Let `u` be a point in a real inner product space, and let `K` be a nonempty complete convex subset.
-Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`.
- -/
+Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`. -/
 theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h₁ : IsComplete K)
     (h₂ : Convex ℝ K) : ∀ u : F, ∃ v ∈ K, ‖u - v‖ = ⨅ w : K, ‖u - w‖ := fun u => by
   let δ := ⨅ w : K, ‖u - w‖

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -211,7 +211,7 @@ end LYM
 
 /-- **Sperner's theorem**. The size of an antichain in `Finset α` is bounded by the size of the
 maximal layer in `Finset α`. This precisely means that `Finset α` is a Sperner order. -/
-theorem IsAntichain.sperner [Fintype α] {𝒜 : Finset (Finset α)}
+theorem _root_.IsAntichain.sperner [Fintype α] {𝒜 : Finset (Finset α)}
     (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
     #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2) := by
   classical

Mathlib/MeasureTheory/Covering/Besicovitch.lean

@@ -791,14 +791,17 @@ theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measur
     rw [← Nat.succ_eq_add_one, u_succ]
     exact (hF (u n) (Pu n)).1
 
-/-- The measurable Besicovitch covering theorem. Assume that, for any `x` in a set `s`,
-one is given a set of admissible closed balls centered at `x`, with arbitrarily small radii.
-Then there exists a disjoint covering of almost all `s` by admissible closed balls centered at some
-points of `s`.
-This version requires that the underlying measure is sigma-finite, and that the space has the
+/-- The measurable **Besicovitch covering theorem**.
+
+Assume that, for any `x` in a set `s`, one is given a set of admissible closed balls centered at
+`x`, with arbitrarily small radii. Then there exists a disjoint covering of almost all `s` by
+admissible closed balls centered at some points of `s`.
+
+This version requires the underlying measure to be sigma-finite, and the space to have the
 Besicovitch covering property (which is satisfied for instance by normed real vector spaces).
 It expresses the conclusion in a slightly awkward form (with a subset of `α × ℝ`) coming from the
 proof technique.
+
 For a version giving the conclusion in a nicer form, see `exists_disjoint_closedBall_covering_ae`.
 -/
 theorem exists_disjoint_closedBall_covering_ae_aux (μ : Measure α) [SFinite μ] (f : α → Set ℝ)
@@ -813,12 +816,14 @@ theorem exists_disjoint_closedBall_covering_ae_aux (μ : Measure α) [SFinite μ
     ⟨t, t_count, ts, tr, tν, tdisj⟩
   exact ⟨t, t_count, ts, tr, hμν tν, tdisj⟩
 
-/-- The measurable Besicovitch covering theorem. Assume that, for any `x` in a set `s`,
-one is given a set of admissible closed balls centered at `x`, with arbitrarily small radii.
-Then there exists a disjoint covering of almost all `s` by admissible closed balls centered at some
-points of `s`. We can even require that the radius at `x` is bounded by a given function `R x`.
-(Take `R = 1` if you don't need this additional feature).
-This version requires that the underlying measure is sigma-finite, and that the space has the
+/-- The measurable **Besicovitch covering theorem**.
+
+Assume that, for any `x` in a set `s`, one is given a set of admissible closed balls centered at
+`x`, with arbitrarily small radii. Then there exists a disjoint covering of almost all `s` by
+admissible closed balls centered at some points of `s`. We can even require that the radius at `x`
+is bounded by a given function `R x`. (Take `R = 1` if you don't need this additional feature).
+
+This version requires the underlying measure to be sigma-finite, and the space to have the
 Besicovitch covering property (which is satisfied for instance by normed real vector spaces).
 -/
 theorem exists_disjoint_closedBall_covering_ae (μ : Measure α) [SFinite μ] (f : α → Set ℝ)

Mathlib/MeasureTheory/Covering/Vitali.lean

@@ -198,12 +198,14 @@ theorem exists_disjoint_subfamily_covering_enlargement_closedBall
 alias exists_disjoint_subfamily_covering_enlargment_closedBall :=
   exists_disjoint_subfamily_covering_enlargement_closedBall
 
-/-- The measurable Vitali covering theorem. Assume one is given a family `t` of closed sets with
-nonempty interior, such that each `a ∈ t` is included in a ball `B (x, r)` and covers a definite
-proportion of the ball `B (x, 3 r)` for a given measure `μ` (think of the situation where `μ` is
-a doubling measure and `t` is a family of balls). Consider a (possibly non-measurable) set `s`
-at which the family is fine, i.e., every point of `s` belongs to arbitrarily small elements of `t`.
-Then one can extract from `t` a disjoint subfamily that covers almost all `s`.
+/-- The measurable **Vitali covering theorem**.
+
+Assume one is given a family `t` of closed sets with nonempty interior, such that each `a ∈ t` is
+included in a ball `B (x, r)` and covers a definite proportion of the ball `B (x, 3 r)` for a given
+measure `μ` (think of the situation where `μ` is a doubling measure and `t` is a family of balls).
+Consider a (possibly non-measurable) set `s` at which the family is fine, i.e., every point of `s`
+belongs to arbitrarily small elements of `t`. Then one can extract from `t` a disjoint subfamily
+that covers almost all `s`.
 
 For more flexibility, we give a statement with a parameterized family of sets.
 -/