no goals
R : Type u_1
S : Type ?u.37276
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
⊢ p ≠ ⊥ ↔ ∃ x, x ∈ p ∧ x ≠ 0
simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]