ι : Type u_3
ι' : Type ?u.464742
R : Type u_1
R₂ : Type ?u.464748
K : Type ?u.464751
M : Type u_2
M' : Type ?u.464757
M'' : Type ?u.464760
V : Type u
V' : Type ?u.464765
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
P : Submodule R M
b : Basis ι R { x // x ∈ P }
x : M
⊢ x ∈ LinearMap.range (Finsupp.total ι M R (↑(Submodule.subtype P) ∘ ↑b)) ↔
    ∃ c, x = Finsupp.sum c fun i x => x • ↑(↑b i)
ι : Type u_3
ι' : Type ?u.464742
R : Type u_1
R₂ : Type ?u.464748
K : Type ?u.464751
M : Type u_2
M' : Type ?u.464757
M'' : Type ?u.464760
V : Type u
V' : Type ?u.464765
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
P : Submodule R M
b : Basis ι R { x // x ∈ P }
x : M
⊢ x ∈ P ↔ ∃ c, x = Finsupp.sum c fun i x => x • ↑(↑b i)
conv_lhs =>
  rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
      ← Finsupp.range_total]
no goals
ι : Type u_3
ι' : Type ?u.464742
R : Type u_1
R₂ : Type ?u.464748
K : Type ?u.464751
M : Type u_2
M' : Type ?u.464757
M'' : Type ?u.464760
V : Type u
V' : Type ?u.464765
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
P : Submodule R M
b : Basis ι R { x // x ∈ P }
x : M
⊢ x ∈ LinearMap.range (Finsupp.total ι M R (↑(Submodule.subtype P) ∘ ↑b)) ↔
    ∃ c, x = Finsupp.sum c fun i x => x • ↑(↑b i)
simp [@eq_comm _ x, Function.comp, Finsupp.total_apply]