[Merged by Bors] - chore: replace aesop with simp where possible

[kim-em]

I'm investigating how aesop is being used (and making comparisons with the in development grind tactic), but finding many uses of aesop can in fact just be replaced by simp.

Hopefully using the simpler tool is both faster, and more readable. We'll see.

[github-actions]

PR summary fc678697dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance {X Y : Action V G} : Zero (X ⟶ Y) := ⟨0, by simp⟩
- instance {X Y : Action V G} : Zero (X ⟶ Y) := ⟨0, by aesop_cat⟩
-+-+ homMk'_mk_id

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

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

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 18fe524.
The entire run failed.
Found no significant differences.

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit fc67869.
There were significant changes against commit b43248b:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ ~Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax   instructions   -23.8%
+ ~Mathlib.CategoryTheory.Triangulated.Functor                 instructions    -3.5%

[kbuzzard]

Nice!

bors merge

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style