∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : AddZeroClass H]
  (f : Multiplicative G ≃* Multiplicative H) (a : H),
  (AddEquiv.toMultiplicative.symm f).symm a = (AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom) a