∀ {R : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (e : M ≃ N) (r : R)
  (m : M), (AddMonoidAlgebra.mapDomainAddEquiv R e) (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single (e m) r