-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
theorem coeff_mul_invOneSubPow_eq_hilbertPoly_eval
    {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) :
    PowerSeries.coeff F n (p * invOneSubPow F d) = (hilbertPoly p d).eval (n : F)

Proof state:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : { x // x ∈ p.support }), ↑i ≤ n
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d) =
    ∑ x ∈ Finset.range n.succ, p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))

Tactic:
refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Result:
case succ.refine_1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : { x // x ∈ p.support }), ↑i ≤ n
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
s : ℕ
hs : s ∈ p.support
⊢ s ∈ Finset.range n.succ

case succ.refine_2
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : { x // x ∈ p.support }), ↑i ≤ n
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ Finset.range n.succ \ p.support
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

case succ.refine_3
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : { x // x ∈ p.support }), ↑i ≤ n
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((n + d - x).choose d) = p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))

Proof state:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F (d + 1))) =
    ∑ i : { x // x ∈ p.support }, p.coeff ↑i * eval (↑n) (preHilbertPoly F d ↑i)

Tactic:
have h_le (i : p.support) : (i : ℕ) ≤ n :=
  le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le

Result:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : { x // x ∈ p.support }), ↑i ≤ n
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F (d + 1))) =
    ∑ i : { x // x ∈ p.support }, p.coeff ↑i * eval (↑n) (preHilbertPoly F d ↑i)