chore(Topology): 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 b9d8d954f7

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.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.