simp [LinearMap.stdBasis_apply]
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : Field R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
x : α → R
⊢ ∑ i : α, y (update 0 i 1) * x i = (∑ x : α, y ((Pi.basisFun R α) x) • (Pi.basisFun R α).coord x) x
no goals