-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem mem_span_image_iff_exists_fun {s : Set α} :
    x ∈ span R (v '' s) ↔ ∃ t : Finset α, ↑t ⊆ s ∧ ∃ c : t → R, ∑ i, c i • v i = x

Proof state:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : { x // x ∈ t } → R
hx : ∑ i : { x // x ∈ t }, c i • v ↑i = x
⊢ ∑ i : { x // x ∈ t }, c i • v ↑i ∈ span R (v '' s)

Tactic:
exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
⊢ x ∈ span R (v '' s) ↔ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x

case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : { x // x ∈ t } → R
hx : ∑ i : { x // x ∈ t }, c i • v ↑i = x
⊢ x ∈ span R (v '' s)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝¹ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : { x // x ∈ t } → R
hx : ∑ i : { x // x ∈ t }, c i • v ↑i = x
a : { x // x ∈ t }
x✝ : a ∈ Finset.univ
⊢ v ↑a ∈ v '' s

Tactic:
aesop

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : { x // x ∈ t } → R
hx : ∑ i : { x // x ∈ t }, c i • v ↑i = x
⊢ x ∈ span R (v '' s)

Tactic:
rw [← hx]

Result:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : { x // x ∈ t } → R
hx : ∑ i : { x // x ∈ t }, c i • v ↑i = x
⊢ ∑ i : { x // x ∈ t }, c i • v ↑i ∈ span R (v '' s)

Proof state:
case refine_1.intro.intro
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x

Tactic:
refine ⟨l.support, hl, l ∘ (↑), ?_⟩

Result:
case refine_1.intro.intro
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∑ i : { x // x ∈ l.support }, (⇑l ∘ Subtype.val) i • v ↑i = x

Proof state:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x

Tactic:
obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h

Result:
case refine_1.intro.intro
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i : { x // x ∈ t }, c i • v ↑i = x

Proof state:
case refine_1.intro.intro
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∑ i : { x // x ∈ l.support }, (⇑l ∘ Subtype.val) i • v ↑i = x

Tactic:
rw [← hx]

Result:
case refine_1.intro.intro
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∑ i : { x // x ∈ l.support }, (⇑l ∘ Subtype.val) i • v ↑i = (Finsupp.linearCombination R v) l

Proof state:
case refine_1.intro.intro
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∑ i : { x // x ∈ l.support }, (⇑l ∘ Subtype.val) i • v ↑i = (Finsupp.linearCombination R v) l

Tactic:
exact l.support.sum_coe_sort fun a ↦ l a • v a

Result:
no goals