doc: demote repeated H1 headers (leanprover-community#36833)

Having more than one H1 header per file confuses search engines and thus makes documentation more difficult to find. Hence, we make sure that lean files only have a single H1 header in them.

In the case of `Mathlib/Tactic/Common.lean`, we achieve this by adding a new module header.

Author: harahu

Archive/Imo/Imo2002Q3.lean

@@ -12,7 +12,7 @@ import Mathlib.RingTheory.Polynomial.Content
 Find all pairs of positive integers $m,n ≥ 3$ for which there exist infinitely many
 positive integers $a$ such that $(a^m+a-1) / (a^n+a^2-1)$ is itself an integer.
 
-# Solution
+## Solution
 
 It suffices to find $(m,n)$ pairs for which $a^n+a^2-1 ∣ a^m+a-1$, where both sides are viewed as
 polynomials in $a$. This automatically gives $n ≤ m$, so we have

Archive/Imo/Imo2010Q5.lean

@@ -25,7 +25,7 @@ Determine if there exists a finite sequence of operations of the allowed types,
 that the five boxes $B_1, B_2, B_3, B_4, B_5$ become empty, while box $B_6$ contains exactly
 $2010^{2010^{2010}}$ coins.
 
-# Solution
+## Solution
 
 We follow the solution from https://web.evanchen.cc/exams/IMO-2010-notes.pdf.
 

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

@@ -439,7 +439,7 @@ lemma localFrame_coeff_eq_coeff (hxe : x ∈ e.baseSet) {i : ι} :
 
 end Bundle.Trivialization
 
-/-! # Determining smoothness of a section via its local frame coefficients
+/-! ### Determining smoothness of a section via its local frame coefficients
 We show that for finite rank bundles over a complete field, a section is smooth iff its coefficients
 in a local frame induced by a local trivialisation are. In many contexts, this statement holds for
 *any* local frame (e.g., for all real bundles which admit a continuous bundle metric, as is

Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean

@@ -15,7 +15,7 @@ import Mathlib.Probability.Distributions.Gaussian.Fernique
 
 In this file we prove basic properties of Gaussian random variables.
 
-# Implementation note
+## Implementation note
 
 Many lemmas are duplicated with an expanded form of some function. For instance there is
 `HasGaussianLaw.add` and `HasGaussianLaw.fun_add`. The reason is that if someone wants for instance

Mathlib/RingTheory/LocalProperties/Injective.lean

@@ -15,7 +15,7 @@ public import Mathlib.RingTheory.LocalProperties.Exactness
 
 # Being injective is a local property
 
-# Main Results
+## Main Results
 
 * `Module.injective_of_isLocalizedModule` : For module `M` over Noetherian ring `R`,
   being injective is preserved under localization.

Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean

@@ -16,7 +16,7 @@ public import Mathlib.RingTheory.LocalProperties.Projective
 
 In this file, we proved that projective dimension equal to supremum over localizations
 
-# Main definition and results
+## Main definition and results
 
 -/
 

Mathlib/RingTheory/QuasiFinite/Weakly.lean

@@ -20,7 +20,7 @@ equivalent to `Algebra.QuasiFiniteAt` under all relevant scenarios.
 This class should only be used in stating (and proving) Zariski's main theorem and should not be
 used elsewhere, and all public API shall have a `Algebra.QuasiFiniteAt` version.
 
-# Implementation details
+## Implementation details
 
 The definition of `Algebra.QuasiFiniteAt R q` as is says that the whole `S_q` is quasi-finite,
 which requires not only `q` to be quasi-finite, but also all primes below it (i.e. all generic

Mathlib/Tactic/Common.lean

@@ -123,6 +123,8 @@ public import Mathlib.Util.TransImports
 public import Mathlib.Util.WhatsNew
 
 /-!
+# Common tactics, linters, and utilities
+
 This file imports all tactics which do not have significant theory imports,
 and hence can be imported very low in the theory import hierarchy,
 thereby making tactics widely available without needing specific imports.
@@ -137,7 +139,7 @@ import hierarchy.
 public meta section
 
 /-!
-# Register tactics with `hint`. Tactics with larger priority run first.
+### Register tactics with `hint`. Tactics with larger priority run first.
 -/
 
 section Hint
@@ -157,7 +159,7 @@ register_hint 200 fun_prop
 end Hint
 
 /-!
-# Register tactics with `try?`. Tactics with larger priority run first.
+### Register tactics with `try?`. Tactics with larger priority run first.
 -/
 
 section Try

Mathlib/Tactic/Linter/EmptyLine.lean

@@ -26,7 +26,7 @@ def Substring.Raw.getRange : Substring.Raw → Syntax.Range
 
 namespace Syntax
 /-!
-# `Syntax` filters
+### `Syntax` filters
 -/
 
 /--