Eq sum eval T zero

lemma eq_sum_evalT_zero {n : ℕ} {c : Fin (n + 1) → C} (t : Tensor S c) :    t = ∑ i, permT _ (IsReindexing.append_of_first c)    (prodT (basis ![c 0] (ComponentIdx.single.symm i)) (evalT 0 i t))  := 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 0)]    · simp only [↓reduceIte]      rw [prodT_basis, basis_apply, permT_pure]      congr      funext i      simp only [Pure.basisVector, Pure.permP_basisVector]      congr      refine Fin.cases ?_ (fun j => ?_) i      · simp only [ComponentIdx.prod, Equiv.coe_fn_symm_mk, Fin.cast_zero, Fin.addCases,          ComponentIdx.single_symm_apply, basisIdxCongr_apply_apply]        exact ComponentIdx.congr_right b 0 0 rfl      · simp only [ComponentIdx.prod, Equiv.coe_fn_symm_mk, Fin.addCases]        rw [dif_neg (by simp)]        simp only [eqRec_eq_cast, basisIdxCongr, Equiv.cast_apply, cast_cast]        symm        rw [cast_eq_iff_heq]        congr 1    · 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