mathlib3

0dfac6eb - chore(*): speed up slow proofs (#7253)

chore(*): speed up slow proofs (#7253) Proofs that are too slow for the forthcoming `gsmul` refactor. I learnt that `by convert ...` is extremely useful even to close a goal, when elaboration using the expected type is a bad idea.