∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (p : Submodule R M) [Algebra.IsEpi R A] [Module.Flat R A], Function.Injective ⇑(Submodule.tensorToSpan A p)