chore(Data): refactor proofs where grind? fails

[chenson2018]

These are sources of technical debt as now reported in the weekly linting report. The idea is that a successful grind proof can fail to report the theorems it used via grind?, which means that if these proofs break across toolchains that it becomes significantly harder to repair.

Most of these are fixed by squeezing the call to grind and unsetting linter.tacticAnalysis.verifyGrindOnly so they no longer appear in the weekly report. Unfortunately, this can't be on by default for performance reasons, but I highly encourage using this linter when adding any grind proofs.

---

[github-actions]

PR summary ff06817091

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

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

---

No changes to strong technical debt.

No changes to weak technical debt.

[Vierkantor]

@kim-em, I recall that this linter was intended to generate bug reports for the Lean developers, not for fixing in Mathlib. Is that still true or is grind? now stable?

[chenson2018]

Is that still true or is grind? now stable?

According to the latest weekly linting, there are 66 proofs in Mathlib that still have this problem. So the situation has improved (I recall it being about double this when I added it to weekly linting) but still exists.

I recall that this linter was intended to generate bug reports for the Lean developers, not for fixing in Mathlib.

This seems to be the position expressed by #40023 (comment). I understand the reasoning, but personally am not very satisfied with leaving these proofs in a state where they essentially need to be reproven by hand if there are any breaking changes in grind. This isn't a constant problem, but something I have experienced in practice.

I had opened this thread to discuss, but received no response.