∀ {R : Type u_1} {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (p : Submodule R M),
  Submodule.span S (Set.range ⇑(Submodule.inclusionSpan S p)) = ⊤