-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem range_linearCombination : LinearMap.range (linearCombination R v) = span R (range v)

Proof state:
case h.mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ LinearMap.range (linearCombination R v) → x ∈ span R (Set.range v)

Tactic:
intro hx

Result:
case h.mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
hx : x ∈ LinearMap.range (linearCombination R v)
⊢ x ∈ span R (Set.range v)

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
x✝ x : M
i : α
hi : v i = x
⊢ (linearCombination R v) (single i 1) = x

Tactic:
simp [hi]

Result:
no goals

Proof state:
case h.mpr.a.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
i : α
hi : v i = x
⊢ x ∈ ↑(LinearMap.range (linearCombination R v))

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_range]

Result:
case h.mpr.a.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
i : α
hi : v i = x
⊢ ∃ y, (linearCombination R v) y = x

Proof state:
case h.mp.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (linearCombination R v) l ∈ span R (Set.range v)

Tactic:
rw [linearCombination_apply]

Result:
case h.mp.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (l.sum fun i a => a • v i) ∈ span R (Set.range v)

Proof state:
case h.mp.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (l.sum fun i a => a • v i) ∈ span R (Set.range v)

Tactic:
exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))

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
x : M
⊢ x ∈ LinearMap.range (linearCombination R v) ↔ x ∈ span R (Set.range v)

Tactic:
constructor

Result:
case h.mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ LinearMap.range (linearCombination R v) → x ∈ span R (Set.range v)

case h.mpr
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) → x ∈ LinearMap.range (linearCombination R v)

Proof state:
case h.mpr.a
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
hx : x ∈ Set.range v
⊢ x ∈ ↑(LinearMap.range (linearCombination R v))

Tactic:
rcases hx with ⟨i, hi⟩

Result:
case h.mpr.a.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
i : α
hi : v i = x
⊢ x ∈ ↑(LinearMap.range (linearCombination R v))

Proof state:
case h.mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
hx : ∃ y, (linearCombination R v) y = x
⊢ x ∈ span R (Set.range v)

Tactic:
rcases hx with ⟨l, hl⟩

Result:
case h.mp.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ x ∈ span R (Set.range v)

Proof state:
case h.mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
hx : x ∈ LinearMap.range (linearCombination R v)
⊢ x ∈ span R (Set.range v)

Tactic:
rw [LinearMap.mem_range] at hx

Result:
case h.mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
hx : ∃ y, (linearCombination R v) y = x
⊢ x ∈ span R (Set.range v)

Proof state:
case h.mpr
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) → x ∈ LinearMap.range (linearCombination R v)

Tactic:
apply span_le.2

Result:
case h.mpr.a
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ Set.range v ⊆ ↑(LinearMap.range (linearCombination R v))

Proof state:
case h.mpr.a.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
i : α
hi : v i = x
⊢ ∃ y, (linearCombination R v) y = x

Tactic:
use Finsupp.single i 1

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
x✝ x : M
i : α
hi : v i = x
⊢ (linearCombination R v) (single i 1) = x

Proof state:
case h.mp.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ x ∈ span R (Set.range v)

Tactic:
rw [← hl]

Result:
case h.mp.intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (linearCombination R v) l ∈ span R (Set.range v)

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
⊢ LinearMap.range (linearCombination R v) = span R (Set.range v)

Tactic:
ext x

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
x : M
⊢ x ∈ LinearMap.range (linearCombination R v) ↔ x ∈ span R (Set.range v)

Proof state:
case h.mpr.a
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ Set.range v ⊆ ↑(LinearMap.range (linearCombination R v))

Tactic:
intro x hx

Result:
case h.mpr.a
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
hx : x ∈ Set.range v
⊢ x ∈ ↑(LinearMap.range (linearCombination R v))