∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (a : α →* Multiplicative β)
  (a_1 : Additive α), (MonoidHom.toAdditiveLeft a) a_1 = Multiplicative.toAdd (a (Additive.toMul a_1))