simp only [piEquiv, Basis.constr, Pi.basisFun_apply, LinearMap.stdBasis_apply,
  LinearEquiv.coe_symm_mk]
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ (piEquiv α R R).symm y i = y (Pi.single i 1)
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ y (update 0 i 1) = y (Pi.single i 1)