Slow proofs in group_cohomology_resolution

Stream: maths

[Amelia Livingston]

There are some one line proofs here in a file of mine that take about a minute to compile. Could anyone help me understand why this is? Fwiw I refactored these maps to use more category theory and general building blocks and the code is way faster. But again, I don't know why :) many thanks for any help.

[Junyan Xu]

For the first one: by apply to_tensor_aux_single f m is super fast, haha
The original to_tensor_aux_single _ _ takes 41.2s, and by apply to_tensor_aux_single (without specifying f and m) takes 22.9s for me.
For the second: by apply of_tensor_aux_single g m x
I've observed the magic of by apply before but don't really understand it. Lean spends too much time on unification without it, apparently.

[Amelia Livingston]

Thank you so much!

[Eric Wieser]

Does (foo : _) work in the same places that by apply foo does?

[Amelia Livingston]

It compiles, but still takes about 40s for the first lemma to compile and 26s for the second

[Junyan Xu]

On my machine:
to_tensor_aux_single _ _ 23.9s (not sure why I got 41.2s last time)
to_tensor_aux_single f m 23.5s
id $ to_tensor_aux_single f m 23.6s
by apply to_tensor_aux_single 22.9s
(to_tensor_aux_single f m : _) 12.2s
id to_tensor_aux_single f m 10s
(id to_tensor_aux_single f m : _) ~70ms
by apply to_tensor_aux_single f m ~70ms
(id (to_tensor_aux_single f m) : _) ~70ms

Note to_tensor and of_tensor are still slow and I've not found a good way to speed them up.