no goals
R : Type u_3
R₂ : Type ?u.65876
K : Type ?u.65879
M : Type u_2
M₂ : Type ?u.65885
V : Type ?u.65888
S : Type ?u.65891
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
ι : Type u_1
v : ι → M
⊢ span R (range v) = ⨆ (i : ι), span R {v i}
rw [span_eq_iSup_of_singleton_spans, iSup_range]