simp only [Pi.basisFun_apply, LinearMap.coeFn_sum, Finset.sum_apply, LinearMap.smul_apply,
  Basis.coord_apply, Pi.basisFun_repr, smul_eq_mul]
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = (∑ x : η, w ((Pi.basisFun R η) x) • (Pi.basisFun R η).coord x) y
case h.e'_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
w : Module.Dual R (η → R)
h : ∀ w_1 ∈ U, w w_1 = 0
y : η → R
hy : y ∈ U
⊢ ∑ x : η, w (Pi.single x 1) * y x = ∑ x : η, w ((LinearMap.stdBasis R (fun x => R) x) 1) * y x