Commit 2024-06-10 06:00 59083072

perf(VectorBundle/FiberwiseLinear): speed up (#13454) #12061 regressed this file pretty badly; speed it up again by mostly reverting a change from that PR, and pushing it further: instead of applying mem_iUnion (which is slow), extract a more specialised statement mem_aux and use it. Before these changes, the profiler output on smoothFiberwiseLinear was

simp took 2.01s
tactic execution of Lean.Parser.Tactic.rintro took 103ms
simp took 905ms
simp took 507ms
simp took 1.26s
simp took 1.14s
elaboration took 645ms

after these changes, it is

simp took 534ms
simp took 183ms
simp took 127ms
simp took 421ms
simp took 365ms
elaboration took 350ms

Still not great at all, but deeper fixes require more time and expertise than I currently have.