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