[Merged by Bors] - feat(Tactic/Linter/UnusedTactic): also lint inside conv =>

[JovanGerb]

This PR extends the unused tactic linter to also lint inside conv =>/conv_lhs =>/slice_lhs i j =>. It is sometimes neccessary to use the skip conv mode tactic to skip goals you don't want to conv into, so I added the conv mode skip to the list of exception tactics.

I also added a test, and did some general cleanup:

• The warning message of the linter is improved.
• The hard-coded exception that #show_kind had, is replaced with just adding it to the list of exceptions.

After this, the unused tactic linter will (almost entirely) subsume the unreachable tactic linter. So, we will be able to turn it off, which will gain us quite a bit of performance.

---

[github-actions]

PR summary fdd74a788a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit fdd74a7).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit fdd74a788a
Reference commit 8cbb95e6e0

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).

[grunweg]

Thanks for doing this. This seems reasonable - I just have three minor comments.

[grunweg]

Thanks for doing this! I'd like another pair of eyes in the changes to Fubini.lean; the linter changes LGTM.
maintainer merge?

[grunweg]

Oh, and can you update the PR description to mention the wording tweaks also?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[JovanGerb]

This can also be written as slice_lhs 1 3 => skip. I'm not sure which is preferred.

[adomani]

Thanks!

A very minor omission is a test for the guardHyp/guardTarget behaviour.

bors d+

[mathlib-bors]

✌️ JovanGerb can now approve this pull request until 2026-08-21 07:25 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[JovanGerb]

The test file is very small - most things aren't tested. Should I add tests for all the exceptions?

[adomani]

Not all necessarily, but it seems like the guards are excepted via a slightly different route than, say, skip in conv mode, so one unlinted guard is probably enough.

Thanks!

[JovanGerb]

It looks like the guards are excepted via a different mechanism than the skip, but it is secretly the same mechanism. I will make another PR cleaning this up, and that PR will also remove the UnusedTacticExtension file, since it is not needed to have this separate file.

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Test and lint
• ci (staging) / Lint style