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

Tactic:
simp_rw [h]

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

Tactic:
rw [← Finset.sum_coe_sort]

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

Proof state:
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
i : { x // x ∈ p.support }
⊢ eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)

Tactic:
rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]

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)
⊢ ∑ 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)

Tactic:
symm

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)
⊢ ∑ 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))

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

Tactic:
simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx

Result:
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

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

Tactic:
simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]

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

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))) =
    eval (↑n)
      (match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)

Tactic:
simp only [eval_finset_sum, eval_smul, smul_eq_mul]

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

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : p.natDegree < n
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) (p.hilbertPoly d)

Tactic:
delta hilbertPoly

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : p.natDegree < n
⊢ (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)

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

Tactic:
exact h_le ⟨s, hs⟩

Result:
no goals