R : Type u_2
M : Type u_1
N : Type ?u.755002
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
w : Set M
x : { x // x ∈ span R w }
⊢ ↑(Finsupp.total (↑w) M R Subtype.val) (Exists.choose (_ : ∃ l, ↑(Finsupp.total (↑w) M R Subtype.val) l = ↑x)) = ↑x
R : Type u_2
M : Type u_1
N : Type ?u.755002
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
w : Set M
x : { x // x ∈ span R w }
⊢ ↑(Finsupp.total (↑w) M R Subtype.val) (repr R w x) = ↑x
rw [Span.repr_def]
no goals
R : Type u_2
M : Type u_1
N : Type ?u.755002
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
w : Set M
x : { x // x ∈ span R w }
⊢ ↑(Finsupp.total (↑w) M R Subtype.val) (Exists.choose (_ : ∃ l, ↑(Finsupp.total (↑w) M R Subtype.val) l = ↑x)) = ↑x
exact ((Finsupp.mem_span_iff_total _ _ _).mp x.2).choose_spec