∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] {f g : R →+* S} (e : f = g) (M : ModuleCat S) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.restrictScalarsCongr e).inv.app M)) x = x