∀ (R : Type u_1) {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (e : M ≃+ N),
  (AddMonoidAlgebra.mapDomainRingHom R ↑e.symm).comp (AddMonoidAlgebra.mapDomainRingHom R ↑e) =
    RingHom.id (AddMonoidAlgebra R M)