∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β],
  Function.RightInverse
    (fun f =>
      let __src := AddEquiv.mulOp.symm f.toAddEquiv;
      let __src_1 := MulEquiv.op.symm f.toMulEquiv;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
    fun f =>
    let __src := AddEquiv.mulOp f.toAddEquiv;
    let __src_1 := MulEquiv.op f.toMulEquiv;
    { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }