-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem span_image_eq_map_linearCombination (s : Set α) :
    span R (v '' s) = Submodule.map (linearCombination R v) (supported R R s)

Proof state:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : x ∈ v '' s
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
rw [Set.mem_image] at hx

Result:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Proof state:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩

Result:
no goals

Proof state:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ ∀ (a : α), a ∈ s ∧ v a = x → x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
intro i hi

Result:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
⊢ z c • v c ∈ span R (v '' s)

Tactic:
haveI := Classical.decPred fun x => x ∈ s

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x => x ∈ s
⊢ z c • v c ∈ span R (v '' s)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
⊢ ∀ (i : α), z i • v i ∈ span R (v '' s)

Tactic:
intro c

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
⊢ z c • v c ∈ span R (v '' s)

Proof state:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ z ∈ comap (linearCombination R v) (span R (v '' s))

Tactic:
rw [mem_comap, linearCombination_apply]

Result:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ (z.sum fun i a => a • v i) ∈ span R (v '' s)

Proof state:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ (z.sum fun i a => a • v i) ∈ span R (v '' s)

Tactic:
refine sum_mem ?_

Result:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ ∀ c ∈ z.support, (fun i a => a • v i) c (z c) ∈ span R (v '' s)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ (linearCombination R v) (single i 1) = x

Tactic:
simp [hi.2]

Result:
no goals

Proof state:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), z i • v i ∈ span R (v '' s)
⊢ ∀ c ∈ z.support, (fun i a => a • v i) c (z c) ∈ span R (v '' s)

Tactic:
simp [this]

Result:
no goals

Proof state:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)

Tactic:
refine map_le_iff_le_comap.2 fun z hz => ?_

Result:
case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
⊢ z ∈ comap (linearCombination R v) (span R (v '' s))

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x => x ∈ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
by_cases h : c ∈ s

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x => x ∈ s
h : c ∈ s
⊢ z c • v c ∈ span R (v '' s)

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x => x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)

Proof state:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ v '' s ⊆ ↑(map (linearCombination R v) (supported R R s))

Tactic:
intro x hx

Result:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : x ∈ v '' s
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ span R (v '' s) = map (linearCombination R v) (supported R R s)

Tactic:
apply span_eq_of_le

Result:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ v '' s ⊆ ↑(map (linearCombination R v) (supported R R s))

case h₂
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)

Proof state:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
apply Exists.elim hx

Result:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ ∀ (a : α), a ∈ s ∧ v a = x → x ∈ ↑(map (linearCombination R v) (supported R R s))

Proof state:
case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x => x ∈ s
h : c ∉ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
simp [(Finsupp.mem_supported' R _).1 hz _ h]

Result:
no goals

Proof state:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x => x ∈ s
h : c ∈ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))

Result:
no goals