no goals
ι✝ : Type ?u.58229
ι' : Type ?u.58232
R : Type u_2
R₂ : Type ?u.58238
K : Type ?u.58241
M : Type u_3
M' : Type ?u.58247
M'' : Type ?u.58250
V : Type u
V' : Type ?u.58255
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
m : M
⊢ ↑b.repr m ∈ Finsupp.supported R R ↑(↑b.repr m).support ∧ ↑(Finsupp.total ι M R ↑b) (↑b.repr m) = m
simp [Finsupp.mem_supported_support]