no goals
R : Type u_1
S : Type u_3
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
⊢ restrictScalars S p = ⊤ ↔ p = ⊤
simp [SetLike.ext_iff]