α : Type u_1
M : Type u_2
N : Type ?u.439719
P : Type ?u.439722
R : Type u_3
S : Type ?u.439728
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.439820
M' : Type ?u.439823
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ span R (v '' s) ≤ map (Finsupp.total α M R v) (supported R R s)
α : Type u_1
M : Type u_2
N : Type ?u.439719
P : Type ?u.439722
R : Type u_3
S : Type ?u.439728
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.439820
M' : Type ?u.439823
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ LinearMap.range (Finsupp.totalOn α M R v s) = ⊤
rw [Finsupp.totalOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
  ←LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
  range_subtype]
no goals
α : Type u_1
M : Type u_2
N : Type ?u.439719
P : Type ?u.439722
R : Type u_3
S : Type ?u.439728
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.439820
M' : Type ?u.439823
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ span R (v '' s) ≤ map (Finsupp.total α M R v) (supported R R s)
exact (span_image_eq_map_total _ _).le