α : Type u_1
M : Type u_2
N : Type ?u.390066
P : Type ?u.390069
R : Type u_3
S : Type ?u.390075
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.390167
M' : Type ?u.390170
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
⊢ x ∈ map (Finsupp.total α M R v) (supported R R s) ↔ ∃ l, l ∈ supported R R s ∧ ↑(Finsupp.total α M R v) l = x
α : Type u_1
M : Type u_2
N : Type ?u.390066
P : Type ?u.390069
R : Type u_3
S : Type ?u.390075
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.390167
M' : Type ?u.390170
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
⊢ x ∈ span R (v '' s) ↔ ∃ l, l ∈ supported R R s ∧ ↑(Finsupp.total α M R v) l = x
rw [span_image_eq_map_total]
no goals
α : Type u_1
M : Type u_2
N : Type ?u.390066
P : Type ?u.390069
R : Type u_3
S : Type ?u.390075
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.390167
M' : Type ?u.390170
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
⊢ x ∈ map (Finsupp.total α M R v) (supported R R s) ↔ ∃ l, l ∈ supported R R s ∧ ↑(Finsupp.total α M R v) l = x
simp