∀ {G : Type u_1} {H : Type u_2} [inst : AddZeroClass G] [inst_1 : AddZeroClass H],
  Function.RightInverse
    (fun f =>
      { toFun := ⇑(AddMonoidHom.toMultiplicative.symm f.toMonoidHom),
        invFun := ⇑(AddMonoidHom.toMultiplicative.symm f.symm.toMonoidHom), left_inv := ⋯, right_inv := ⋯,
        map_add' := ⋯ })
    fun f =>
    { toFun := ⇑(AddMonoidHom.toMultiplicative f.toAddMonoidHom),
      invFun := ⇑(AddMonoidHom.toMultiplicative f.symm.toAddMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }