fix: explicitly enable header linter (#31849)

In files that don't import `Mathlib.Init` but do import `Mathlib.Tactic.Linter.Header`, the linter didn't fire currently: the option is only enabled when we define `linter.mathlibStandardSet`. So in the Mathlib lakefile (but not for downstream projects) we should enable the linter explicitly.

Not sure how we should test this, since it is a lakefile option.

Spotted during review of #31820.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Author: Vierkantor

lakefile.lean

@@ -27,6 +27,9 @@ require "leanprover-community" / "plausible" @ git "main"
 `lake build` uses them, as well as `Archive` and `Counterexamples`. -/
 abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.mathlibStandardSet, true⟩,
+  -- Explicitly enable the header linter, since the standard set is defined in `Mathlib.Init`
+  -- but we want to run this linter in files imported by `Mathlib.Init`.
+  ⟨`linter.style.header, true⟩,
   ⟨`linter.checkInitImports, true⟩,
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,