feat(Tactic/Linter/Header): make header linter work downstream

[kim-em]

This PR makes linter.style.header usable in projects downstream of Mathlib. Previously isInMathlib hardcoded a lookup of Mathlib.lean, so the linter silently exited early in (e.g.) CSLib even when enabled via linter.mathlibStandardSet.

The fix uses the root of the current mainModule to find the aggregator file, so Cslib.Foo.Bar now checks Cslib.lean, matching the standard Lean convention that a library named Foo has its root file at Foo.lean. The "skip the aggregator itself" check is generalised from mainModule == \MathlibtomainModule == mainModule.getRoot`.

Reported by Chris Henson on Zulip; cc @chenson2018 @grunweg.

🤖 Prepared with Claude Code

[github-actions]

PR summary c1e30e172c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ isInLibraryRoot
- isInMathlib

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[chenson2018]

This looks good to me at first glance. Once the cache is ready I'll try it out with CSLib as additional confirmation.

Edit: This appears to be working as expected.

[chenson2018]

It looks the build now fails on a header lint in Archive, so it seems like this is working as intended!

[grunweg]

I don't find the wording "Defensive: " clear at all... let me double-check the comment being outdated: #38405

[grunweg]

Check successful: how rephrasing the comment as follows?

Suggested change

	-- Defensive: skip linting the library root file itself. In practice the
	-- `inLibraryRoot?` check above already covers this (a well-formed `<root>.lean`
	-- does not import itself), but a root module could appear in `headerTestFiles`.
	-- Skip linting the library root file itself.
	-- In practice, the `inLibraryRoot?` check above already covers this (a well-formed `<root>.lean`
	-- does not import itself), but a root module could appear in `headerTestFiles`.

[grunweg]

LGTM, with the one comment rephrased and the build failure fixed (i.e., that archive file getting a valid copyright header). Thanks for doing this!
bors d+

[mathlib-bors]

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.