no goals
R : Type u_1
S : Type ?u.170489
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 p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ∧ x ∈ p' → x ∈ {0}) ↔ ∀ (x : M), x ∈ p → x ∈ p' → x = 0
simp