Theorem: Module.Dual.sum_update (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : 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 = y x
Tactic:
rw [← LinearMap.congr_fun ((Pi.basisFun R α).sum_dual_apply_smul_coord y) x]
State after:
α : 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

State before:
α : 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
Tactic:
simp [LinearMap.stdBasis_apply]
State after:
no goals