no goals
R : Type u_2
S : Type ?u.179265
M : Type u_1
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 : Submodule R M
hpq : Disjoint p q
a : { x // x ∈ p }
ha : ↑a ∈ q
⊢ a = 0
exact_mod_cast disjoint_def.mp hpq a (coe_mem a) ha