∀ {a b c : CategoryTheory.LocallyDiscrete CommRingCat} (x : a ⟶ b) (x_1 : b ⟶ c),
  CommRingCat.moduleCatExtendScalarsPseudofunctor.mapComp x x_1 =
    CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom x.as) (CommRingCat.Hom.hom x_1.as))