-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d n : ℕ
hn : p.natDegree < n
zero :
  Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F 0) : F⟦X⟧)) : F)
    (eval (↑n : F)
        (match (motive := ℕ → F[X]) 0 with
        | 0 => 0
        | d.succ => ∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i)) :
      F)
succ :
  ∀ (d : ℕ)
    (hd :
      Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) : F)
        (eval (↑n : F)
            (match (motive := ℕ → F[X]) d with
            | 0 => 0
            | d.succ => ∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i)) :
          F)),
    Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
      (eval (↑n : F)
          (match (motive := ℕ → F[X]) d + 1 with
          | 0 => 0
          | d.succ => ∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i)) :
        F)
⊢ Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) : F)
    (eval (↑n : F)
        (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i)) :
      F)

Tactic:
induction d with
  | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
            exact coeff_eq_zero_of_natDegree_lt hn
  | succ d hd =>
      simp only [eval_finsetSum, eval_smul, smul_eq_mul]
      rw [← Finset.sum_coe_sort]
      have h_le (i : p.support) : (i : ℕ) ≤ n :=
        le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
      have h (i : p.support) : eval ↑n (preHilbertPoly F d ↑i) = (n + d - ↑i).choose d := by
        rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]
      simp_rw [h]
      rw [Finset.sum_coe_sort _ (fun x => (p.coeff ↑x) * (_ + d - ↑x).choose _),
        PowerSeries.coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk,
        invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ (zero_lt_succ d)]
      simp only [coeff_coe, coeff_mk]
      symm
      refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
      · rw [Finset.mem_range_succ_iff]
        exact h_le ⟨s, hs⟩
      · simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
        rw [hx.2, zero_mul]
      · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]

Premises used: PowerSeries.invOneSubPow_zero, Nat.choose, HMul.hMul, Nat.succ_eq_add_one, Classical.not_not, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, MulZeroClass.zero_mul, Nat.zero_lt_succ, Finset.mem_range_succ_iff, HSub.hSub, Polynomial.mem_support_iff, PowerSeries.coeff_mk, Polynomial.eval_zero, Nat.cast, Polynomial.eval_finsetSum, add_comm, Polynomial.coeff, Finset.mem_sdiff, PowerSeries.coeff_mul, HAdd.hAdd, PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos, Polynomial.coeff_eq_zero_of_natDegree_lt, Units.val_one, Nat.zero, Polynomial.eval_smul, add_tsub_cancel_right, smul_eq_mul, mul_one, Nat.succ, Finset.sum_coe_sort, Polynomial.coeff_coe, Finset.sum_subset_zero_on_sdiff