case intro.intro
ι✝ : Type ?u.63088
ι' : Type ?u.63091
R : Type u_2
R₂ : Type ?u.63097
K : Type ?u.63100
M : Type u_3
M' : Type ?u.63106
M'' : Type ?u.63109
V : Type u
V' : Type ?u.63114
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b✝ b₁ : Basis ι✝ R M
i : ι✝
c : R
x : M
ι : Type u_1
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (↑b '' s)
l : ι →₀ R
hl : l ∈ Finsupp.supported R R s
hlm : ↑(Finsupp.total ι M R ↑b) l = m
⊢ ↑(↑b.repr m).support ⊆ s
ι✝ : Type ?u.63088
ι' : Type ?u.63091
R : Type u_2
R₂ : Type ?u.63097
K : Type ?u.63100
M : Type u_3
M' : Type ?u.63106
M'' : Type ?u.63109
V : Type u
V' : Type ?u.63114
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b✝ b₁ : Basis ι✝ R M
i : ι✝
c : R
x : M
ι : Type u_1
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (↑b '' s)
⊢ ↑(↑b.repr m).support ⊆ s
rcases(Finsupp.mem_span_image_iff_total _).1 hm with ⟨l, hl, hlm⟩
no goals
case intro.intro
ι✝ : Type ?u.63088
ι' : Type ?u.63091
R : Type u_2
R₂ : Type ?u.63097
K : Type ?u.63100
M : Type u_3
M' : Type ?u.63106
M'' : Type ?u.63109
V : Type u
V' : Type ?u.63114
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b✝ b₁ : Basis ι✝ R M
i : ι✝
c : R
x : M
ι : Type u_1
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (↑b '' s)
l : ι →₀ R
hl : l ∈ Finsupp.supported R R s
hlm : ↑(Finsupp.total ι M R ↑b) l = m
⊢ ↑(↑b.repr m).support ⊆ s
rwa [← hlm, repr_total, ← Finsupp.mem_supported R l]