doc(Archive): ensure only a single H1 header per file (#31384)

This PR ensures we only have a single H1 header per lean file in the Archive subdirectory. We do this for the following reasons:

- Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting webpage actually is.
- The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3.

Author: harahu

Archive/Imo/Imo1975Q1.lean

@@ -15,7 +15,7 @@ Let `x₁, x₂, ... , xₙ` and `y₁, y₂, ... , yₙ` be two sequences of re
 `x₁ ≥ x₂ ≥ ... ≥ xₙ` and `y₁ ≥ y₂ ≥ ... ≥ yₙ`. Prove that if `z₁, z₂, ... , zₙ` is any permutation
 of `y₁, y₂, ... , yₙ`, then `∑ (xᵢ - yᵢ)^2 ≤ ∑ (xᵢ - zᵢ)^2`
 
-# Solution
+## Solution
 
 Firstly, we expand the squares within both sums and distribute into separate finite sums. Then,
 noting that `∑ yᵢ ^ 2 = ∑ zᵢ ^ 2`, it remains to prove that `∑ xᵢ * zᵢ ≤ ∑ xᵢ * yᵢ`, which is true

Archive/Imo/Imo1985Q2.lean

@@ -20,7 +20,7 @@ so that:
 
 Prove that all numbers in $N$ must receive the same color.
 
-# Solution
+## Solution
 
 Let $a \sim b$ denote that $a$ and $b$ have the same color.
 Because $j$ is coprime to $n$, every number in $N$ is of the form $kj\bmod n$ for a unique

Archive/Imo/Imo1994Q1.lean

@@ -18,7 +18,7 @@ such that for any two indices `i` and `j` with `1 ≤ i ≤ j ≤ m` and `aᵢ +
 there exists an index `k` such that `aᵢ + aⱼ = aₖ`.
 Show that `(a₁+a₂+...+aₘ)/m ≥ (n+1)/2`
 
-# Sketch of solution
+## Sketch of solution
 
 We can order the numbers so that `a₁ ≤ a₂ ≤ ... ≤ aₘ`.
 The key idea is to pair the numbers in the sum and show that `aᵢ + aₘ₊₁₋ᵢ ≥ n+1`.

Archive/Imo/Imo1997Q3.lean

@@ -18,7 +18,7 @@ $|x_1 + x_2 + \cdots + x_n| = 1$ and $|x_i| ≤ \frac{n+1}2$ for $i = 1, 2, \dot
 Show that there exists a permutation $y_1, y_2, \dots, y_n$ of $x_1, x_2, \dots, x_n$ such that
 $|y_1 + 2y_2 + \cdots + ny_n| ≤ \frac{n+1}2$.
 
-# Solution
+## Solution
 
 For a permutation $π$ let $S(π) = \sum_{i=1}^n i x_{π(i)}$. We wish to show that there exists $π$
 with $|S(π)| ≤ \frac{n+1}2$.

Archive/Imo/Imo2001Q3.lean

@@ -20,7 +20,7 @@ both the girl and the boy.
 
 Show that there is a problem that was solved by at least three girls and at least three boys.
 
-# Solution
+## Solution
 
 Note that not all of the problems a girl $g$ solves can be "hard" for boys, in the sense that
 at most two boys solved it. If that was true, by condition 1 at most $6 × 2 = 12$ boys solved

Archive/Imo/Imo2001Q4.lean

@@ -15,7 +15,7 @@ $a = (a_1, a_2, \dots, a_n)$ of $\{1, 2, \dots, n\}$, define $S(a) = \sum_{i=1}^
 Prove that there exist two permutations $a ≠ b$ of $\{1, 2, \dots, n\}$ such that
 $n!$ is a divisor of $S(a) - S(b)$.
 
-# Solution
+## Solution
 
 Suppose for contradiction that all the $S(a)$ have distinct residues modulo $n!$, then
 $$\sum_{i=0}^{n!-1} i ≡ \sum_a S(a) = \sum_i c_i \sum_a a_i = (n-1)! \frac{n(n+1)}2 \sum_i c_i$$

Archive/Imo/Imo2001Q5.lean

@@ -11,7 +11,7 @@ import Mathlib.Geometry.Euclidean.Triangle
 Let `ABC` be a triangle. Let `AP` bisect `∠BAC` and let `BQ` bisect `∠ABC`, with `P` on `BC` and
 `Q` on `AC`. If `AB + BP = AQ + QB` and `∠BAC = 60°`, what are the angles of the triangle?
 
-# Solution
+## Solution
 
 We follow the solution from https://web.evanchen.cc/exams/IMO-2001-notes.pdf.
 

Archive/Imo/Imo2005Q3.lean

@@ -14,7 +14,7 @@ import Mathlib.Tactic.Ring
 Let `x`, `y` and `z` be positive real numbers such that `xyz ≥ 1`. Prove that:
 `(x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0`
 
-# Solution
+## Solution
 The solution by Iurie Boreico from Moldova is presented, which won a special prize during the exam.
 The key insight is that `(x^5-x^2)/(x^5+y^2+z^2) ≥ (x^2-y*z)/(x^2+y^2+z^2)`, which is proven by
 factoring `(x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2))` into a non-negative expression

Archive/Imo/Imo2008Q2.lean

@@ -21,7 +21,7 @@ for all real numbers `x`,`y`, `z`, each different from 1, and satisfying `xyz =
 (b) Prove that equality holds above for infinitely many triples of rational numbers `x`, `y`, `z`,
 each different from 1, and satisfying `xyz = 1`.
 
-# Solution
+## Solution
 (a) Since `xyz = 1`, we can apply the substitution `x = a/b`, `y = b/c`, `z = c/a`.
 Then we define `m = c-b`, `n = b-a` and rewrite the inequality as `LHS - 1 ≥ 0`
 using `c`, `m` and `n`. We factor `LHS - 1` as a square, which finishes the proof.

Archive/Imo/Imo2008Q3.lean

@@ -15,7 +15,7 @@ import Mathlib.Tactic.LinearCombination
 Prove that there exist infinitely many positive integers `n` such that `n^2 + 1` has a prime
 divisor which is greater than `2n + √(2n)`.
 
-# Solution
+## Solution
 We first prove the following lemma: for every prime `p > 20`, satisfying `p ≡ 1 [MOD 4]`,
 there exists `n ∈ ℕ` such that `p ∣ n^2 + 1` and `p > 2n + √(2n)`. Then the statement of the
 problem follows from the fact that there exist infinitely many primes `p ≡ 1 [MOD 4]`.