case refine'_1
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
⊢ (fun i => single i 1) '' s ⊆ ↑(supported R R s)

case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i => single i 1) '' s)
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
⊢ supported R R s = span R ((fun i => single i 1) '' s)
refine' (span_eq_of_le _ _ (SetLike.le_def.2 fun l hl => _)).symm
case refine'_1.intro.intro
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
w✝ : α
hp : w✝ ∈ s
⊢ (fun i => single i 1) w✝ ∈ ↑(supported R R s)
case refine'_1
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
⊢ (fun i => single i 1) '' s ⊆ ↑(supported R R s)
rintro _ ⟨_, hp, rfl⟩
no goals
case refine'_1.intro.intro
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
w✝ : α
hp : w✝ ∈ s
⊢ (fun i => single i 1) w✝ ∈ ↑(supported R R s)
exact single_mem_supported R 1 hp
case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ sum l single ∈ span R ((fun i => single i 1) '' s)
case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i => single i 1) '' s)
rw [← l.sum_single]
case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
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)
case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ sum l single ∈ span R ((fun i => single i 1) '' s)
refine' sum_mem fun i il => _
case h.e'_4
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
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
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
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)
case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
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)
convert smul_mem (M := α →₀ R) (x := single i 1) (span R ((fun i => single i 1) '' s)) (l i) ?_
no goals
case h.e'_4
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (↑l i) = ↑l i • single i 1
simp [span]
case refine'_2.a
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i 1 ∈ (fun i => single i 1) '' s
case refine'_2
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
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)
apply subset_span
no goals
case refine'_2.a
α : Type u_1
M : Type ?u.63004
N : Type ?u.63007
P : Type ?u.63010
R : Type u_2
S : Type ?u.63016
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
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i 1 ∈ (fun i => single i 1) '' s
apply Set.mem_image_of_mem _ (hl il)