[Merged by Bors] - chore: review of automation in category theory

[semorrison]

Clean up of automation in the category theory library. Leaving out unnecessary proof steps, or fields done by aesop_cat, and making more use of available autoparameters.

---

[jcommelin]

This currently doesn't build. Once it builds, I would be interested in running a benchmark to see how much of a difference this use of automation makes. (Hopefully very little!)

[semorrison]

!bench

[semorrison]

!bench

[leanprover-bot]

Here are the benchmark results for commit ae8d859.
There were significant changes against commit 28f3fa3:

  Benchmark                                                     Metric         Change
  ===================================================================================
- build                                                         aesop            6.3%
- ~Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup   instructions     8.8%
- ~Mathlib.Algebra.Homology.Opposite                            instructions     6.9%
- ~Mathlib.CategoryTheory.Adjunction.Limits                     instructions    17.4%
- ~Mathlib.CategoryTheory.Adjunction.Opposites                  instructions     7.2%
- ~Mathlib.CategoryTheory.Bicategory.End                        instructions    32.0%
- ~Mathlib.CategoryTheory.Category.Bipointed                    instructions     9.3%
- ~Mathlib.CategoryTheory.Category.Pairwise                     instructions    42.6%
- ~Mathlib.CategoryTheory.Category.TwoP                         instructions     6.7%
- ~Mathlib.CategoryTheory.Endofunctor.Algebra                   instructions    43.2%
- ~Mathlib.CategoryTheory.FinCategory                           instructions    12.1%
- ~Mathlib.CategoryTheory.Functor.Hom                           instructions    16.6%
- ~Mathlib.CategoryTheory.IsConnected                           instructions    12.8%
- ~Mathlib.CategoryTheory.Limits.Cones                          instructions     6.0%
- ~Mathlib.CategoryTheory.Limits.HasLimits                      instructions    10.5%
- ~Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer          instructions     9.2%
- ~Mathlib.CategoryTheory.Monad.Algebra                         instructions     6.2%
- ~Mathlib.CategoryTheory.Monoidal.FunctorCategory              instructions    31.6%
- ~Mathlib.CategoryTheory.Over                                  instructions    21.8%
- ~Mathlib.CategoryTheory.PEmpty                                instructions    17.5%
- ~Mathlib.CategoryTheory.PUnit                                 instructions     9.3%
- ~Mathlib.CategoryTheory.Sites.Plus                            instructions     7.5%
- ~Mathlib.CategoryTheory.Sites.Pushforward                     instructions    16.7%
- ~Mathlib.CategoryTheory.Sites.Sheaf                           instructions    12.3%
+ ~Mathlib.CategoryTheory.Subterminal                           instructions   -16.4%
- ~Mathlib.CategoryTheory.Triangulated.Triangulated             instructions    14.5%
- ~Mathlib.Order.Category.DistLatCat                            instructions    15.6%
- ~Mathlib.Order.Category.FinPartOrd                            instructions    12.9%
- ~Mathlib.Order.Category.LatCat                                instructions    11.1%
- ~Mathlib.Order.Category.LinOrdCat                             instructions    15.1%
- ~Mathlib.Order.Category.NonemptyFinLinOrdCat                  instructions     7.2%
- ~Mathlib.Order.Category.PartOrdCat                            instructions    14.1%
- ~Mathlib.Order.Category.PreordCat                             instructions    13.7%
- ~Mathlib.Topology.Sheaves.LocalPredicate                      instructions     9.6%

[leanprover-bot]

Here are the benchmark results for commit d743f11.
The entire run failed.
Found no runs to compare against.

[semorrison]

bench suggests an increase of 0.75% in wall-clock.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed:

• Build

[jcommelin]

bors d+

[bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style