Folding polynomial eq sum split Nth

@[simp low]lemma folding_polynomial_eq_sum_splitNth {𝔽 : Type} [Field 𝔽]  {f : Polynomial 𝔽} {n : ℕ}  [inst : NeZero n] :  FoldingPolynomial.foldingPolynomial (X ^ n) f =    ∑ i, C (splitNth f n i) * (X ^ i.val) := by  symm  apply FoldingPolynomial.folding_polynomial_is_unique'  · conv =>      rhs      rw [splitNth_def (f := f) (inst := inst)]    rw [      Polynomial.map_sum,      Polynomial.eval_finsetSum]    simp only [Polynomial.map_mul, map_C, coe_compRingHom, Polynomial.map_pow, map_X,    eval_mul, eval_C, eval_pow, eval_X]    simp only [comp]    conv =>      lhs      rhs      ext x      rw [mul_comm]      rfl  · simp only [Bivariate.degreeX, finsetSum_coeff, coeff_C_mul, coeff_X_pow, mul_ite, mul_one,    mul_zero, natDegree_pow, natDegree_X]    simp only [Finset.sup_le_iff, mem_support_iff, finsetSum_coeff, coeff_C_mul, coeff_X_pow,    mul_ite, mul_one, mul_zero, ne_eq]    intro b hb    apply natDegree_sum_le_of_forall_le    rintro ⟨i, hi⟩ _    by_cases heq: b = i    · simp only [heq, ↓reduceIte]      exact splitNth_degree_le    · simp [heq]  · simp only [Bivariate.natDegreeY, natDegree_pow, natDegree_X, mul_one]    apply Nat.lt_of_le_pred (by {      apply Nat.zero_lt_of_ne_zero      aesop    })    apply Polynomial.natDegree_sum_le_of_forall_le    intro i _    apply Nat.le_trans Polynomial.natDegree_mul_le    rcases i with ⟨i, hi⟩    simp    omega