∀ {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_2}
  {N : Type u_1} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M] [inst_6 : Module S M]
  [IsScalarTower R S M] [inst_8 : Module R N] [inst_9 : Module S N] [IsScalarTower R S N],
  Function.Surjective ⇑(algebraMap R S) →
    ∀ (f : M ≃ₗ[R] N) (r : S) (x : M), (↑f).toFun (r • x) = (RingHom.id S) r • (↑f).toFun x