no goals
R : Type u_2
M : Type u_1
N : Type ?u.761155
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset M
x : M
hx : x ∈ span R ↑s
⊢ x ∈ span R (_root_.id '' ↑s)
rwa [Set.image_id]