-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
`m` can be written as a finite `R`-linear combination of elements of `s`.
The implementation uses a sum indexed by `Fin n` for some `n`. -/
lemma mem_span_set' {m : M} {s : Set M} :
    m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → s),
      ∑ i, f i • (g i : M) = m

Proof state:
case refine_2.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → ↑s
⊢ ∑ i : Fin n, f i • ↑(g i) ∈ span R s

Tactic:
exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))

Result:
no goals

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
h : m ∈ span R s
⊢ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m

Tactic:
rcases mem_span_set.1 h with ⟨c, cs, rfl⟩

Result:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
⊢ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = c.sum fun mi r => r • mi

Proof state:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
A : { x // x ∈ c.support } ≃ Fin c.support.card
⊢ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = c.sum fun mi r => r • mi

Tactic:
refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩

Result:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
A : { x // x ∈ c.support } ≃ Fin c.support.card
⊢ ∑ i : Fin c.support.card, (fun i => c ↑(A.symm i)) i • ↑((fun i => ⟨↑(A.symm i), ⋯⟩) i) = c.sum fun mi r => r • mi

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
h : m ∈ span R s
⊢ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m

case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ (∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m) → m ∈ span R s

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ (∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m) → m ∈ span R s

Tactic:
rintro ⟨n, f, g, rfl⟩

Result:
case refine_2.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → ↑s
⊢ ∑ i : Fin n, f i • ↑(g i) ∈ span R s

Proof state:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
A : { x // x ∈ c.support } ≃ Fin c.support.card
⊢ ∑ i : Fin c.support.card, (fun i => c ↑(A.symm i)) i • ↑((fun i => ⟨↑(A.symm i), ⋯⟩) i) =
    ∑ i : { x // x ∈ c.support }, c ↑i • ↑i

Tactic:
exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)

Result:
no goals

Proof state:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
⊢ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = c.sum fun mi r => r • mi

Tactic:
have A : c.support ≃ Fin c.support.card := Finset.equivFin _

Result:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
A : { x // x ∈ c.support } ≃ Fin c.support.card
⊢ ∃ n f g, ∑ i : Fin n, f i • ↑(g i) = c.sum fun mi r => r • mi

Proof state:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
A : { x // x ∈ c.support } ≃ Fin c.support.card
⊢ ∑ i : Fin c.support.card, (fun i => c ↑(A.symm i)) i • ↑((fun i => ⟨↑(A.symm i), ⋯⟩) i) = c.sum fun mi r => r • mi

Tactic:
rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]

Result:
case refine_1.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
c : M →₀ R
cs : ↑c.support ⊆ s
h : (c.sum fun mi r => r • mi) ∈ span R s
A : { x // x ∈ c.support } ≃ Fin c.support.card
⊢ ∑ i : Fin c.support.card, (fun i => c ↑(A.symm i)) i • ↑((fun i => ⟨↑(A.symm i), ⋯⟩) i) =
    ∑ i : { x // x ∈ c.support }, c ↑i • ↑i