mathlib

42c42370 - chore(mv_polynomial/equiv): speed up elaboration by adjusting priorities (#7840)

chore(mv_polynomial/equiv): speed up elaboration by adjusting priorities (#7840) `option_equiv_left` timed out several times in bors, since the introduction of non-unital rings. We fix this by adjusting the priority to make sure that the problematic instance is found right away. Also speed up circumcenter file (which also just timed out in bors) by squeezing simps.