∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N),
  (MonoidAlgebra.mapDomainRingEquiv R e).symm = MonoidAlgebra.mapDomainRingEquiv R e.symm