∀ {R : Type u_1} [inst : CommRing R] (X : CategoryTheory.Mon (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp
      (ModuleCat.MonModuleEquivalenceAlgebra.functor.map
        ((CategoryTheory.NatIso.ofComponents
                (fun A =>
                  { hom := { hom := ModuleCat.ofHom { toFun := id, map_add' := ⋯, map_smul' := ⋯ }, isMonHom_hom := ⋯ },
                    inv := { hom := ModuleCat.ofHom { toFun := id, map_add' := ⋯, map_smul' := ⋯ }, isMonHom_hom := ⋯ },
                    hom_inv_id := ⋯, inv_hom_id := ⋯ })
                ⋯).hom.app
          X))
      ((CategoryTheory.NatIso.ofComponents
              (fun A =>
                {
                  hom :=
                    AlgCat.ofHom
                      { toFun := id, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ },
                  inv :=
                    AlgCat.ofHom
                      { toFun := id, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ })
              ⋯).hom.app
        (ModuleCat.MonModuleEquivalenceAlgebra.functor.obj X)) =
    CategoryTheory.CategoryStruct.id (ModuleCat.MonModuleEquivalenceAlgebra.functor.obj X)