no goals
R : Type u_3
M : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : n → M
i : n
⊢ (Finset.sum Finset.univ fun x => (if i = x then 1 else 0) • b x) = b i
simp only [ite_smul, zero_smul, one_smul, Finset.sum_ite_eq, Finset.mem_univ, ite_true]