R : Type u_2
M : Type u_1
N : Type ?u.764012
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : M
s : Set M
⊢ m ∈ span R (_root_.id '' s) ↔ ∃ c, ↑c.support ⊆ s ∧ (Finsupp.sum c fun mi r => r • mi) = m
R : Type u_2
M : Type u_1
N : Type ?u.764012
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (Finsupp.sum c fun mi r => r • mi) = m
conv_lhs => rw [← Set.image_id s]
no goals
R : Type u_2
M : Type u_1
N : Type ?u.764012
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : M
s : Set M
⊢ m ∈ span R (_root_.id '' s) ↔ ∃ c, ↑c.support ⊆ s ∧ (Finsupp.sum c fun mi r => r • mi) = m
exact Finsupp.mem_span_image_iff_total R (v := _root_.id (α := M))