-- 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.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.coeff x = 0
⊢ p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) = 0

Tactic:
rw [hx.2, zero_mul]

Result:
no goals

Proof state:
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

Tactic:
rw [Finset.mem_range_succ_iff]

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 ≤ n

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)
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F (d + 1))) =
    ∑ x : { x // x ∈ p.support }, p.coeff ↑x * ↑((n + d - ↑x).choose d)

Tactic:
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)]

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
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ ∑ k ∈ Finset.range n.succ,
      (PowerSeries.coeff F (k, n - k).1) ↑p *
        (PowerSeries.coeff F (k, n - k).2) (mk fun n => ↑((d.succ - 1 + n).choose (d.succ - 1))) =
    ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d)

Proof state:
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))

Tactic:
rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]

Result:
no goals

Proof state:
case zero
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt hn

Result:
no goals

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)
⊢ ∑ k ∈ Finset.range n.succ,
      (PowerSeries.coeff F (k, n - k).1) ↑p *
        (PowerSeries.coeff F (k, n - k).2) (mk fun n => ↑((d.succ - 1 + n).choose (d.succ - 1))) =
    ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d)

Tactic:
simp only [coeff_coe, coeff_mk]

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
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ ∑ x ∈ Finset.range n.succ, p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) =
    ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d)

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
⊢ (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 (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)]

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
h : ∀ (i : { x // x ∈ p.support }), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F (d + 1))) =
    ∑ i : { x // x ∈ p.support }, p.coeff ↑i * eval (↑n) (preHilbertPoly F d ↑i)