∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : AddMonoidAlgebra R N),
  AddMonoidAlgebra.comapDomain f hf x = AddMonoidAlgebra.ofCoeff (Finsupp.comapDomain f x.coeff ⋯)