grunweg

I just reviewed the script (and some CI bits) in #11874. Summarising what I said there: looks very good, I only have minor comments.

Thanks for the quick response! I'll trust Mario and Kim on `getLeanLibs`, so this PR looks good to go, from my side. maintainer merge

I've proposed moving the common code into `Mathlib/Utils` in #13339.

@Komyyy Coming here for PR triage: thanks for your PR. It currently has a merge conflict, which means it won't show up in the review queue (and is less likely...

I presume this is looking for review? Let me label it accordingly - if my guess was wrong, feel free to update that status. With my reviewer's hat on, I...

It seems this PR is awaiting action by the PR author: let me label it accordingly. Looking at the PR description, it seems to me this PR is doing several...

Coming here for triaging old PRs: is this one still relevant? The relevant Lean PR looks like it has been stale for more than ten months. @JovanGerb Can you clarify...

Can you update the PR description, please (since you removed one of the lemmas from this PR)? Thanks!

> > Also: should the linter move to `Mathlib/Tactic/Linter`? (Did the [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2FTactic.2F*) come to a conclusion?) > > That discussion did not come to a conclusion... Given that some...

I just realised: this linter already exists in `batteries`; it is the `docBlameThm` linter, defined [here](https://github.com/leanprover-community/batteries/blob/c0efc1fd2a0bec51bd55c5b17348af13d7419239/Batteries/Tactic/Lint/Misc.lean#L88) in batteries. (That linter is not autofixable by itself, so I see no pain...