-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_eq_span_single (s : Set α) :
    supported R R s = span R ((fun i => single i 1) '' s)

Proof state:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l.sum single ∈ span R ((fun i => single i 1) '' s)

Tactic:
refine sum_mem fun i il => ?_

Result:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) ∈ span R ((fun i => single i 1) '' s)

Proof state:
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ supported R R s = span R ((fun i => single i 1) '' s)

Tactic:
refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm

Result:
case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ (fun i => single i 1) '' s ⊆ ↑(supported R R s)

case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i => single i 1) '' s)

Proof state:
case refine_2.a
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i 1 ∈ (fun i => single i 1) '' s

Tactic:
apply Set.mem_image_of_mem _ (hl il)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i => single i 1) '' s)

Tactic:
rw [← l.sum_single]

Result:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l.sum single ∈ span R ((fun i => single i 1) '' s)

Proof state:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) ∈ span R ((fun i => single i 1) '' s)

Tactic:
convert smul_mem (M := α →₀ R) (x := single i 1) (span R ((fun i => single i 1) '' s)) (l i) ?_

Result:
case h.e'_5
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) = l i • single i 1

case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i 1 ∈ span R ((fun i => single i 1) '' s)

Proof state:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i 1 ∈ span R ((fun i => single i 1) '' s)

Tactic:
apply subset_span

Result:
case refine_2.a
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i 1 ∈ (fun i => single i 1) '' s

Proof state:
case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ (fun i => single i 1) '' s ⊆ ↑(supported R R s)

Tactic:
rintro _ ⟨_, hp, rfl⟩

Result:
case refine_1.intro.intro
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
w✝ : α
hp : w✝ ∈ s
⊢ (fun i => single i 1) w✝ ∈ ↑(supported R R s)

Proof state:
case h.e'_5
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) = l i • single i 1

Tactic:
simp [span]

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
w✝ : α
hp : w✝ ∈ s
⊢ (fun i => single i 1) w✝ ∈ ↑(supported R R s)

Tactic:
exact single_mem_supported R 1 hp

Result:
no goals