Refactoring algebraic properties of bundled maps

Stream: mathlib4

[Moritz Doll]

In #33477 I started a refactor of introducing type-classes for FunLike and algebraic operations that capture properties like (f + g) x = f x + g x. Reasons for having this are twofold: (a) there are a couple of lemmas that are duplicated with various types of functions, but that are only using equalities as above, most importantly Finset.prod_apply, which states that (∏ i ∈ s, f i) x = ∏ i ∈ s, f i x. (b) when defining function spaces, there is a lot of boilerplate in defining the add_apply lemmas (you want them to be simp) and also to obtain various instances like AddCommGroup (which follows trivially from the corresponding properties on the codomain).
In #33477, specifically Mathlib.Analysis.Distribution.SchwartzSpace I have an example of how much boilerplate we could get rid of and how defining function spaces gets simplified.
The problem however is obviously performance, because this will stress the typeclass inference system more.
The benchmark for just changing AddHom and AddMonoidHom, (and SchwartzMap, but that one does not really contribute) is
instructions: +3.0T (+1.6%), wall-clock: +30s (+2.3%).
Refactoring something like LinearMap and ContinuousLinearMap will be somewhat annoying I assume and also negatively impact the performance, so I would like to know whether this refactor is appreciated and how much performance we are willing to sacrifice.

Earlier discussions are at (I started a new topic, because my old one was a Is there code for X):
https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60FunLike.60.20with.20additional.20algebraic.20structure/with/566022971
and https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/AddMonoidHomClass.20confusion/with/502885117

[Moritz Doll]

:ping_pong: for feedback on this potential refactor. I would like to have an opinion of someone more familiar with type classes/inference system to judge whether this is worth doing.
It is a lot of work refactoring all bundled FunLike types, so I don't want to put in serious efforts for nothing.