no goals
R : Type u_2
R₂ : Type ?u.64934
K : Type ?u.64937
M : Type u_1
M₂ : Type ?u.64943
V : Type ?u.64946
S : Type ?u.64949
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 s : Set M
⊢ span R s = ⨆ (x : M) (_ : x ∈ s), span R {x}
simp only [← span_iUnion, Set.biUnion_of_singleton s]