Sorry, I am not yet convinced these classes are worth having. Can you remind me:

1. What instances you want to have that involve these new typeclasses.

2. What lemmas you expect these classes to generalise.

1. There are the instances in this PR, for ENNReal, WithTop α, WithBot α, PUnit, EReal, PartENat, Measure and Filter. Additionally, every canonically ordered monoid is a NoBotSum, as is PNat, but I'm not sure if that's useful. (I now see I missed Interval in this PR I'll add it soon).
2. There are add_top/top_add/add_bot/bot_add, which currently exist for LinearOrderedAddCommMonoidWithTop, WithTop, PartENat, Measure, WithBot, Filter, Interval, EReal. There are add_eq_top/add_eq_bot, which exist for WithTop, PartENat, ENNReal, WithBot, Filter, EReal (and could exist for LinearOrderedAddCommMonoidWithTop but is missing), as well as add_eq_zero_iff for canonical monoids (although that should probably remain separate). Additionally, I think it might generalize Filter.bot_sub with EReal.bot_sub and Filter.sub_bot with Interval.sub_bot, although I'm not quite sure about that.

1. So no instance is parametric? no instance depends on the new typeclasses? (as in take in one of the new typeclasses as an argument, rather than as an output)
2. Why can't we just add the missing lemmas for the specific types? Is it that you are trying to avoid a name clash?

It's really important that we can justify every typeclass we add to mathlib because, once a typeclass exists, people feel encouraged to generalise lemmas to it even when it is not mathematically useful to do so, and this makes those typeclasses look crucial when they are not, and also hard to remove.

I worry that the typeclasses in the present PR generalise few lemmas (< 10) from few types (< 10) which are very different mathematically very different (in particular are not thought to be different incarnations of the same algebraic structure, the way eg ℤ and ℝ are rings), meaning that those typeclasses have no backing on paper. Further, the list of generalised lemmas seems very sparse among the lemmas about top in the API of the respective types, meaning that people will find themselves using top lemmas specific to their types, except sometimes where the lemma they want just happens to be generalisable to one of your new typeclasses. This is cognitive overload.

1. There are a bunch of potential instances for the order dual (NoTopSum <-> NoBotSum, IsTopAbsorbing <-> IsBotAbsorbing), and for a bunch of type synonyms, but that's all I can think of.
2. I think wanting to avoid a name clash is one of the main reasons for this, yes.

Additionally, looking at MulZeroClass and NoZeroDivisors many of the multiplicative lemmas for them have additive equivalences here, which I think is also part of my reason for this, although probably many of them aren't useful.
Not direct equivalence:

• MulZeroClass.negZeroClass is equivalent to stating that in a IsTopAbsorbing SubtractionMonoid we have -⊤= ⊤ (and the same for bottom).
• WithZero.mulZeroClass, WithBot.instMulZeroClass, WithTop.instMulZeroClass, WithBot.instNoZeroDivisors, WithTop.instNoZeroDivisors: these are mostly the contents of this PR, except for WithZero preserving IsTopAbsorbing/IsBotAbsorbing/NoTopSum/NoBotSum

Directly equivalent:

• mul_eq_zero_of_left, mul_eq_zero_of_right
• eq_zero_of_mul_self_eq_zero
• mul_self_eq_zero, mul_self_ne_zero
• zero_eq_mul_self, zero_ne_mul_self
• mul_eq_zero_comm, mul_ne_zero_comm
• mul_eq_zero, mul_ne_zero, mul_ne_zero_iff
• mul_zero_eq_const, zero_mul_eq_const
• eq_zero_of_ne_zero_of_mul_left_eq_zero, eq_zero_of_ne_zero_of_mul_right_eq_zero
• left_ne_zero_of_mul, right_ne_zero_of_mul
• mul_eq_zero_of_ne_zero_imp_eq_zero
• ne_zero_and_ne_zero_of_mul
• ite_zero_mul, mul_ite_zero
• ite_zero_mul_ite_zero
• SemiconjBy.zero_left, SemiconjBy.zero_right
• Commute.zero_left, Commute.zero_right
• instMulZeroClassLex
• instMulZeroClassOrderDual
• IsLeftRegular.subsingleton, IsRegular.subsingleton, IsRightRegular.subsingleton
• isLeftRegular_zero_iff_subsingleton, isRegular_iff_subsingleton, isRightRegular_zero_iff_subsingleton
• more regular stuff
• Pi.mulZeroClass
• pow_eq_zero, pow_ne_zero
• sq_eq_zero_iff
• pow_eq_zero_iff, pow_ne_zero_iff, pow_eq_zero_iff'
• List.prod_eq_zero_iff, List.prod_ne_zero
• Multiset.prod_eq_zero_iff, Multiset.prod_ne_zero
• Finsupp.prod_ne_zero_iff, Finsupp.prod_eq_zero_iff
• isSquare_zero

Another instance of this I just noticed is that Multisets are a NoBotSum

Another instance of this I just noticed is that Multisets are a NoBotSum

That's already covered by the fact that they are a canonically ordered monoid

Do you still need this PR now that your SubtractionMonoid instance is merged?

I don't need it, but I still think it's good