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.
See PR #659, in
Algebra.Hom.Group, around theoremMonoidHom.coe_coe. If the quickfixis removed, the
to_additivetactic seems to be looking forAddMonoidHomClass.toOneHomClass, when it should look forAddMonoidHomClass.toZeroHomClass. It has no trouble translatingOneHomClasstoZeroHomClass, but has trouble withtoOneHomClass.