mathlib3

ccefda07 - perf(representation_theory/basic): speed up `representation.lin_hom` by a factor of 20 (#13739)

perf(representation_theory/basic): speed up `representation.lin_hom` by a factor of 20 (#13739) `ext` was over-expanding, and the `simp`s were not all squeezed. This is causing timeouts in other PRs.