no goals
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
N : Submodule R M
hs : FG N
t : Set M
ht : Set.Finite t ∧ span R t = N
⊢ span R (↑f '' t) = Submodule.map f N
rw [span_image, ht.2]