case h
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ x ∈ LinearMap.range (Finsupp.total α M R v) ↔ x ∈ span R (Set.range v)
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
⊢ LinearMap.range (Finsupp.total α M R v) = span R (Set.range v)
ext x
case h.mp
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ x ∈ LinearMap.range (Finsupp.total α M R v) → x ∈ span R (Set.range v)

case h.mpr
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ x ∈ span R (Set.range v) → x ∈ LinearMap.range (Finsupp.total α M R v)
case h
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ x ∈ LinearMap.range (Finsupp.total α M R v) ↔ x ∈ span R (Set.range v)
constructor
case h.mp
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
hx : x ∈ LinearMap.range (Finsupp.total α M R v)
⊢ x ∈ span R (Set.range v)
case h.mp
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ x ∈ LinearMap.range (Finsupp.total α M R v) → x ∈ span R (Set.range v)
intro hx
case h.mp
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
hx : ∃ y, ↑(Finsupp.total α M R v) y = x
⊢ x ∈ span R (Set.range v)
case h.mp
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
hx : x ∈ LinearMap.range (Finsupp.total α M R v)
⊢ x ∈ span R (Set.range v)
rw [LinearMap.mem_range] at hx
case h.mp.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
l : α →₀ R
hl : ↑(Finsupp.total α M R v) l = x
⊢ x ∈ span R (Set.range v)
case h.mp
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
hx : ∃ y, ↑(Finsupp.total α M R v) y = x
⊢ x ∈ span R (Set.range v)
rcases hx with ⟨l, hl⟩
case h.mp.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
l : α →₀ R
hl : ↑(Finsupp.total α M R v) l = x
⊢ ↑(Finsupp.total α M R v) l ∈ span R (Set.range v)
case h.mp.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
l : α →₀ R
hl : ↑(Finsupp.total α M R v) l = x
⊢ x ∈ span R (Set.range v)
rw [← hl]
case h.mp.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
l : α →₀ R
hl : ↑(Finsupp.total α M R v) l = x
⊢ (sum l fun i a => a • v i) ∈ span R (Set.range v)
case h.mp.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
l : α →₀ R
hl : ↑(Finsupp.total α M R v) l = x
⊢ ↑(Finsupp.total α M R v) l ∈ span R (Set.range v)
rw [Finsupp.total_apply]
no goals
case h.mp.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
l : α →₀ R
hl : ↑(Finsupp.total α M R v) l = x
⊢ (sum l fun i a => a • v i) ∈ span R (Set.range v)
exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))
case h.mpr.a
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ Set.range v ⊆ ↑(LinearMap.range (Finsupp.total α M R v))
case h.mpr
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ x ∈ span R (Set.range v) → x ∈ LinearMap.range (Finsupp.total α M R v)
apply span_le.2
case h.mpr.a
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
hx : x ∈ Set.range v
⊢ x ∈ ↑(LinearMap.range (Finsupp.total α M R v))
case h.mpr.a
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x : M
⊢ Set.range v ⊆ ↑(LinearMap.range (Finsupp.total α M R v))
intro x hx
case h.mpr.a.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
i : α
hi : v i = x
⊢ x ∈ ↑(LinearMap.range (Finsupp.total α M R v))
case h.mpr.a
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
hx : x ∈ Set.range v
⊢ x ∈ ↑(LinearMap.range (Finsupp.total α M R v))
rcases hx with ⟨i, hi⟩
case h.mpr.a.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
i : α
hi : v i = x
⊢ ∃ y, ↑(Finsupp.total α M R v) y = x
case h.mpr.a.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
i : α
hi : v i = x
⊢ x ∈ ↑(LinearMap.range (Finsupp.total α M R v))
rw [SetLike.mem_coe, LinearMap.mem_range]
case h.mpr.a.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
i : α
hi : v i = x
⊢ ↑(Finsupp.total α M R v) (single i 1) = x
case h.mpr.a.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
i : α
hi : v i = x
⊢ ∃ y, ↑(Finsupp.total α M R v) y = x
use Finsupp.single i 1
no goals
case h.mpr.a.intro
α : Type u_3
M : Type u_1
N : Type ?u.330103
P : Type ?u.330106
R : Type u_2
S : Type ?u.330112
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.330204
M' : Type ?u.330207
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
x✝ x : M
i : α
hi : v i = x
⊢ ↑(Finsupp.total α M R v) (single i 1) = x
simp [hi]