to_additive and multiple parents

Stream: mathlib4

[Scott Morrison]

In Algebra/Group/Defs.lean and Algebra/Group/Basic.lean we have a few instances of the following problem:

[Scott Morrison]

/-- An `add_monoid` is an `add_semigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
  nsmul : ℕ → M → M := nsmulRec
  nsmul_zero' : ∀ x, nsmul 0 x = 0 := by intros; rfl
  nsmul_succ' : ∀ (n : ℕ) (x), nsmul n.succ x = x + nsmul n x := by intros; rfl

/-- A `monoid` is a `semigroup` with an element `1` such that `1 * a = a * 1 = a`. -/
@[to_additive AddMonoid]
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
  npow : ℕ → M → M := npowRec
  npow_zero' : ∀ x, npow 0 x = 1 := by intros; rfl
  npow_succ' : ∀ (n : ℕ) (x), npow n.succ x = x * npow n x := by intros; rfl

-- FIXME to_additive didn't notice the second parent
attribute [to_additive AddMonoid.toAddZeroClass] Monoid.toMulOneClass

[Scott Morrison]

Perhaps this is another thing @Floris van Doorn could look at? Otherwise I'll create an issue and try to look at it later. :-)