no goals
R : Type u
M : Type v
F : Type ?u.155008
G : Type ?u.155011
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I J : Ideal R
N P : Submodule R M
S : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
ι : Type u_1
s : Set ι
f : ι → M
x : M
⊢ x ∈ I • span R (f '' s) ↔ ∃ a x_1, (Finsupp.sum a fun i c => c • f ↑i) = x
rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range]