failing `simps`

Stream: mathlib4

[Moritz Firsching]

While porting CategoryTheory.Groupoid.VertexGroup, I came across this error for the [simps] before vertexGroup:

Failed to find constructor nvMonoid in structure Div.

What is going on here?

see mathlib4#2609

[Floris van Doorn]

Fixed in !4#2883. This PR also implements the feature that if you use @[simps] on algebraic classes like Group, it will generate the right simp-lemmas (using */1 instead of Mul.mul/One.one).