Eq sum eval T

lemma eq_sum_evalT {n : ℕ} {c : Fin (n + 1) → C} (t : Tensor S c) :    t = ∑ i, permT id (IsReindexing.append_succ_last c) (prodT (evalT (Fin.last n) i t)      (basis ![c (Fin.last n)] (ComponentIdx.single.symm i)))   := by  induction' t using Tensor.induction_on_basis with b a t h t1 t2 h1 h2  · conv_rhs => enter [2, i]; rw [evalT_basis]    generalize_proofs h1 h2 h3    rw [Finset.sum_eq_single (b (Fin.last n))]    · simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ↓reduceIte]      rw [prodT_basis, basis_apply, permT_pure]      congr      funext i      simp only [Pure.basisVector, Pure.permP_basisVector]      congr      refine Fin.addCases (fun j => ?_) (fun j => ?_) i      · simp only [id_eq, ComponentIdx.prod_symm_castAdd, Function.comp_apply]        erw [basisIdxCongr_apply_apply]        exact ComponentIdx.congr_right b _ _ (by rw [Fin.succAbove_last]; rfl)      · simp only [id_eq, ComponentIdx.prod_symm_natAdd, ComponentIdx.single_symm_apply,          basisIdxCongr_apply_apply]        erw [basisIdxCongr_apply_apply]        exact ComponentIdx.congr_right _ _ _ (by fin_cases j; rfl)    · intro j h1 h1      rw [if_neg (by grind)]      simp    · simp  · simp  · conv_lhs => rw [h]    simp [Finset.smul_sum]  · simp [Finset.sum_add_distrib]    grind