chore(AlgebraicTopology): 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.

---

[github-actions]

PR summary 7cf290f932

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.

[joelriou]

While we believe that the linter verifyGrindOnly is useful at identifying bugs in the grind tactic, this PR (and #40022, #39769, #39808) only removes the symptoms rather than fixing the real issue which is a bug in the grind tactic in Lean core.

[grunweg]

It would be extremely valuable to have some of these as minimized bug reports to Lean core, so the underlying issue (perhaps a grind bug) can be fixed. We appreciate this is much more work than this PR --- but if you would like to help move this forward, that would be a very helpful next step. Probably Kim's lean-minimize tool can help here.

[chenson2018]

@joelriou @grunweg Thanks for the feedback. This makes sense, but still seems less than ideal in the short term from the Mathlib perspective. I opened a Zulip thread to discuss.