no goals
R : Type u_2
M : Type u_3
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis n R M
i : n
⊢ ↑(LinearEquiv.symm (equivFun b)) (↑(stdBasis R (fun x => R) i) 1) = ↑b i
simp