no goals
R : Type u_1
R₂ : Type ?u.205557
K : Type ?u.205560
M : Type u_2
M₂ : Type ?u.205566
V : Type ?u.205569
S : Type ?u.205572
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
p : Submodule R M
x : { x // x ∈ p }
⊢ map (Submodule.subtype p) (span R {x}) = span R {↑x}
simp [← span_image]