∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst_1 : MulOneClass β],
  Function.RightInverse
    (fun f => { toFun := fun a => Additive.ofMul (f (Multiplicative.ofAdd a)), map_zero' := ⋯, map_add' := ⋯ }) fun f =>
    { toFun := fun a => Additive.toMul (f (Multiplicative.toAdd a)), map_one' := ⋯, map_mul' := ⋯ }