fin_cases leaves (fun i => i) ⟨0, _⟩ atoms that break linear_combination

After fin_cases i on i : Fin n, hypotheses mention P ((fun i => i) ⟨0, ⋯⟩) or P ⟨0, ⋯⟩ instead of P 0. linear_combination (norm := module) (and ring) treat these as atoms different from P 0, so a correct combination fails with a baffling scalar goal like μ 0 + μ 1 + μ 2 + μ 3 = 0. simp only [Fin.isValue] at h did not fix it for me. Robust fix: avoid fin_cases in the algebraic step; do it generically with weights containing if k = i then c else 0 and Finset.sum_ite_eq', Finset.sum_sub_distrib, Finset.sum_smul, then use fin_cases only in the final linarith step on scalar equations.