no goals
R : Type u_1
R₂ : Type ?u.120610
K : Type ?u.120613
M : Type u_2
M₂ : Type ?u.120619
V : Type ?u.120622
S : Type ?u.120625
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s✝ t : Set M
s : Submodule R M
v₀ : M
⊢ s ≤ span R {v₀} ↔ ∀ (v : M), v ∈ s → ∃ r, r • v₀ = v
simp_rw [SetLike.le_def, mem_span_singleton]