no goals
ι : Type u_1
ι' : Type ?u.177420
R : Type u_2
R₂ : Type ?u.177426
K : Type ?u.177429
M : Type u_3
M' : Type ?u.177435
M'' : Type ?u.177438
V : Type u
V' : Type ?u.177443
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
b : Basis ι R M
i : ι
f : ι →₀ R
⊢ ↑(coord b i) (↑(LinearEquiv.symm b.repr) f) = ↑f i
simp only [repr_symm_apply, coord_apply, repr_total]