chore: avoid superfluous use of push_neg with contrapose, by_contra o…

[grunweg]

…r by_cases

Found by the linter in #37907.

---

[grunweg]

!bench

[leanprover-radar]

Benchmark results for f7917f4 against 24bf43f are in. There are no significant changes. @grunweg

• ✅ build//instructions: -5.9G (-0.00%)

No significant changes detected.

[github-actions]

PR summary 00dbc4ec64

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

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

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.

You can run this locally as

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

[JovanGerb]

Great! That's a non-trivial amount of tactics cleaned up :). I guess most of these removals are made possible by #31510. I wonder if a similar change should be made to by_cases, namely that if the hypothesis is already a negation, it doesn't make a double negation.

[wwylele]

I see myself got listed in suggested reviewers, likely because I put code with a lot of contrapose! without thinking. If the new guideline is to only use it when needed, then this looks good!

[JovanGerb]

maintainer merge

[JovanGerb]

Oh, it seems there is a merge conflict. Does the merge conflict label not work anymore?

[github-actions]

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

[grunweg]

Indeed - merged master.
CC @bryangingechen in case there's something to investigate about the merge conflict workflow. Maybe it just got stuck in the crossfire of github issues these days.