∀ (G : Type u_3) [inst : AddGroup G] (a : Multiplicative G ≃* Multiplicative G) (a_1 : G),
  (AddEquiv.symm ((MulAutMultiplicative G) a)) a_1 = Multiplicative.toAdd (a.symm (Multiplicative.ofAdd a_1))