case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ v '' s ⊆ ↑(map (Finsupp.total α M R v) (supported R R s))

case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ map (Finsupp.total α M R v) (supported R R s) ≤ span R (v '' s)
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ span R (v '' s) = map (Finsupp.total α M R v) (supported R R s)
apply span_eq_of_le
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : x ∈ v '' s
⊢ x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ v '' s ⊆ ↑(map (Finsupp.total α M R v) (supported R R s))
intro x hx
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
⊢ x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : x ∈ v '' s
⊢ x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
rw [Set.mem_image] at hx
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
⊢ ∀ (a : α), a ∈ s ∧ v a = x → x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
⊢ x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
apply Exists.elim hx
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
⊢ ∀ (a : α), a ∈ s ∧ v a = x → x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
intro i hi
no goals
case h₁
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ x ∈ ↑(map (Finsupp.total α M R v) (supported R R s))
exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩
no goals
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
x : M
hx : ∃ x_1, x_1 ∈ s ∧ v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ ↑(Finsupp.total α M R v) (single i 1) = x
simp [hi.2]
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
⊢ z ∈ comap (Finsupp.total α M R v) (span R (v '' s))
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
⊢ map (Finsupp.total α M R v) (supported R R s) ≤ span R (v '' s)
refine' map_le_iff_le_comap.2 fun z hz => _
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), ↑z i • v i ∈ span R (v '' s)
⊢ (sum z fun i a => a • v i) ∈ span R (v '' s)
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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 (Finsupp.total α M R v) (span R (v '' s))
rw [mem_comap, total_apply]
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), ↑z i • v i ∈ span R (v '' s)
⊢ ∀ (c : α), c ∈ z.support → (fun i a => a • v i) c (↑z c) ∈ span R (v '' s)
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), ↑z i • v i ∈ span R (v '' s)
⊢ (sum z fun i a => a • v i) ∈ span R (v '' s)
refine' sum_mem _
no goals
case h₂
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
this : ∀ (i : α), ↑z i • v i ∈ span R (v '' s)
⊢ ∀ (c : α), c ∈ z.support → (fun i a => a • v i) c (↑z c) ∈ span R (v '' s)
simp [this]
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
⊢ ↑z c • v c ∈ span R (v '' s)
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
⊢ ∀ (i : α), ↑z i • v i ∈ span R (v '' s)
intro c
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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)
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
⊢ ↑z c • v c ∈ span R (v '' s)
haveI := Classical.decPred fun x => x ∈ s
case pos
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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)
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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)
by_cases h : c ∈ s
no goals
case pos
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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)
exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
no goals
case neg
α : Type u_1
M : Type u_2
N : Type ?u.379165
P : Type ?u.379168
R : Type u_3
S : Type ?u.379174
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.379266
M' : Type ?u.379269
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → 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)
simp [(Finsupp.mem_supported' R _).1 hz _ h]