finite_dimensional performance issues

Stream: general

[Wrenna Robson]

When I use the finite_dimensional definitions and lemmas in mathlib, even just in statements, they seem to work very slowly. Specifically I'm asserting things like finite_dimensional (degree_lt F t). It's honestly annoying enough that I think I'm going to have to find another way around it... anyone know what the cause might be?

[Scott Morrison]

Could you post a #mwe for people to have a look at?