∀ {R : Type u} [inst : CommRing R] {x x_1 : CategoryTheory.Mon (ModuleCat R)} (f : x ⟶ x_1) (a : ↑x.X),
  (AlgCat.Hom.hom (ModuleCat.MonModuleEquivalenceAlgebra.functor.map f)) a =
    (CategoryTheory.ConcreteCategory.hom f.hom) a