Commit 2024-10-10 12:21 9d0db8d6

chore(Category/Ring): turn CommRingCat and CommSemiRingCat into abbrevs (#17612) This builds on #11595 by also turning the commutative categories into abbreviations. Note that we keep some instances that the analogous changes in #11595 deleted: these turn out to not be strictly necessary, but prevent a few timeouts. This change paves the way for #17583 changing unification hints for bundled categories. Previously, we would use a unification hint to turn (forget CommRingCat).obj X into (X : Type*), after #17583 it would apply to (forget (Bundled CommRing)).obj X instead. That might assign some metavariables, leading to cases where the type of an object became Bundled CommRing instead of the expected CommRingCat. Unification hints are not very tweakable, so we can't really avoid this. So as a bit of a workaround, we can instead make the two reducibly defeq. I expect no real performance hit, since we are replacing the discrimination tree key CommRingCat with Bundled CommRing, where both are not further (semi)reducibly reducible.