WIP: tinker with Function.Surjective.module

[kbuzzard]

---

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8b03d56.
There were significant changes against commit 03720bd:

  Benchmark                                     Metric         Change
  ===================================================================
- ~Mathlib.Algebra.Category.ModuleCat.Abelian   instructions     5.8%
- ~Mathlib.Algebra.Category.ModuleCat.Limits    instructions    15.7%

[kbuzzard]

I wonder why this change has such a detrimental effect on those files? Note to self -- chase this up. Note to anyone else reading: I remove a "with" and then in contrast to the usual behaviour (either nothing, or a bunch of files go quicker), here a bunch of files go slower.

[kbuzzard]

Mathlib.Algebra.Category.ModuleCat.Limits is 250 lines and compiles on my machine in 8 seconds, so a 15.7% increase is not the end of the world :-) Around half the time is spent on one declaration, directLimitsIsColimit. On master according to count_heartbeats this takes 140000-150000 heartbeats, and according to the profiler it takes about 5 seconds on my machine. Piping the trace output of the declaration to a file gives a 40952-line file.

With the change in this PR, the declaration now takes about 6 seconds, it goes up to 188426 heartbeats and the trace is now 49911 lines, an increase of 25%.

[kbuzzard]

master now has the change that this PR makes because it was also (essentially) made in #6241 . Note that that PR was also benchmarked and similar slowdowns were observed in the same two files.