no goals
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.269908
M₆ : Type ?u.269911
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p q : Submodule R M
x : M
⊢ x ∈ p ⊔ q ↔ x ∈ range (coprod (Submodule.subtype p) (Submodule.subtype q))
simp [Submodule.mem_sup, SetLike.exists]