See PR #659, in Algebra.Hom.Group, around theorem MonoidHom.coe_coe. If the quickfix
attribute [to_additive AddMonoidHomClass.toZeroHomClass] MonoidHomClass.toOneHomClass
is removed, the to_additive tactic seems to be looking for AddMonoidHomClass.toOneHomClass, when it should look for AddMonoidHomClass.toZeroHomClass. It has no trouble translating OneHomClass to ZeroHomClass, but has trouble with toOneHomClass.