doc(Data): misc. improvements (#31431)

This PR fixes a batch of typos in the `Data` subdirectory. Found and fixed with help from Codex. As part of this work, we also demote some headers that shouldn't have been H1.

Author: harahu

Mathlib/Data/ENNReal/Real.lean

@@ -15,7 +15,7 @@ files.
 
 This file provides a `positivity` extension for `ENNReal.ofReal`.
 
-# Main theorems
+## Main statements
 
   - `trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal`: often used for `WithLp` and `lp`
   - `dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal`: often used for `WithLp` and `lp`

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -461,7 +461,7 @@ lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2
 
 
 /-!
-# Factorial via binary splitting.
+### Factorial via binary splitting.
 
 We prove this is equal to the standard factorial and mark it `@[csimp]`.
 

Mathlib/Data/Nat/Fib/Basic.lean

@@ -13,46 +13,38 @@ import Mathlib.Data.Nat.Choose.Basic
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 
 /-!
-# Fibonacci Numbers
+# Fibonacci numbers
 
-This file defines the fibonacci series, proves results about it and introduces
-methods to compute it quickly.
--/
-
-/-!
-# The Fibonacci Sequence
-
-## Summary
-
-Definition of the Fibonacci sequence `F₀ = 0, F₁ = 1, Fₙ₊₂ = Fₙ + Fₙ₊₁`.
+This file defines the Fibonacci sequence as `F₀ = 0, F₁ = 1, Fₙ₊₂ = Fₙ + Fₙ₊₁`. Furthermore, it
+proves results about the sequence and introduces methods to compute it quickly.
 
-## Main Definitions
+## Main definitions
 
 - `Nat.fib` returns the stream of Fibonacci numbers.
 
-## Main Statements
+## Main statements
 
-- `Nat.fib_add_two`: shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁.`.
+- `Nat.fib_add_two`: shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁`.
 - `Nat.fib_gcd`: `fib n` is a strong divisibility sequence.
 - `Nat.fib_succ_eq_sum_choose`: `fib` is given by the sum of `Nat.choose` along an antidiagonal.
 - `Nat.fib_succ_eq_succ_sum`: shows that `F₀ + F₁ + ⋯ + Fₙ = Fₙ₊₂ - 1`.
 - `Nat.fib_two_mul` and `Nat.fib_two_mul_add_one` are the basis for an efficient algorithm to
   compute `fib` (see `Nat.fastFib`).
 
-## Implementation Notes
+## Implementation notes
 
 For efficiency purposes, the sequence is defined using `Stream.iterate`.
 
 ## Tags
 
-fib, fibonacci
+Fibonacci numbers, Fibonacci sequence
 -/
 
 namespace Nat
 
 
 
-/-- Implementation of the fibonacci sequence satisfying
+/-- Implementation of the Fibonacci sequence satisfying
 `fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1)`.
 
 *Note:* We use a stream iterator for better performance when compared to the naive recursive
@@ -74,7 +66,7 @@ theorem fib_one : fib 1 = 1 :=
 theorem fib_two : fib 2 = 1 :=
   rfl
 
-/-- Shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁.` -/
+/-- Shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁`. -/
 theorem fib_add_two {n : ℕ} : fib (n + 2) = fib n + fib (n + 1) := by
   simp [fib, Function.iterate_succ_apply']