Commit 2023-08-07 13:57 1accbf5b

chore: lower instance priority of CancelMonoid.toMonoid etc (#6145) This PR lowers the instance priority of inheritance going to cancellative structures, specifically those matching the regular expression (Add)?(Left|Right)?Cancel(Comm)?(Monoid|Semigroup)(WithZero)?. Most of these cancellative structures either derive from group structures or from (integral) domain structures (including fields). Thus we should be going through the group and semiring hierarchy before going through the cancellative hierarchy. In particular, IsDomain is a mixin depending on Semiring so trying to synthesize an IsDomain instance to satisfy Monoid before even trying Semiring makes no sense. We came across this issue when adding an extra way to find an IsDomain instance, because this slows down the failing cancellative search path enough to cause timeouts. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20is.20.60simpNF.60.20complaining.20here.3F