awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
d : ℕ
h :
  Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) d with
      | 0 => 0
      | d.succ => ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
      F[X])
    (0 : F[X])
⊢ Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
      F[X])
    (0 : F[X])

Tactic:
simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

Premises used: Finset.sum_const_zero, zero_smul, Polynomial.coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
d : ℕ
zero :
  Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) 0 with
      | 0 => 0
      | d.succ => ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
      F[X])
    (0 : F[X])
succ :
  ∀ (d : ℕ),
    Eq.{u_1 + 1} (α := F[X])
        (match (motive := ℕ → F[X]) d with
          | 0 => 0
          | d.succ =>
            ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
          F[X])
        (0 : F[X]) →
      Eq.{u_1 + 1} (α := F[X])
        (match (motive := ℕ → F[X]) d + 1 with
          | 0 => 0
          | d.succ =>
            ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
          F[X])
        (0 : F[X])
⊢ Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) d with
      | 0 => 0
      | d.succ => ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
      F[X])
    (0 : F[X])

Tactic:
induction d with
  | zero => simp only
  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

Premises used: Finset.sum_const_zero, zero_smul, Polynomial.coeff_zero, Nat.zero, Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p : F[X]
⊢ p.hilbertPoly 0 = 0

Tactic:
rfl

Premises used: Polynomial.hilbertPoly, rfl
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p : F[X]
d : ℕ
⊢ p.hilbertPoly (d + 1) = ∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i)

Tactic:
rfl

Premises used: Polynomial.hilbertPoly, rfl
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
d k : ℕ
⊢ Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) d + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (HPow.hPow (α := F[X]) X k).support,
          HSMul.hSMul (β := F[X]) ((HPow.hPow (α := F[X]) X k).coeff i) (preHilbertPoly F d i) :
      F[X])
    (preHilbertPoly F d k : F[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p q : F[X]
d : ℕ
delta :
  (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
    HAdd.hAdd (α := F[X]) (β := F[X])
      (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[X])
      (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
        F[X])
⊢ (p + q).hilbertPoly d = p.hilbertPoly d + q.hilbertPoly d

Tactic:
delta hilbertPoly

Premises used: Polynomial.hilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p q : F[X]
⊢ (match (motive := ℕ → F[X]) 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
    HAdd.hAdd (α := F[X]) (β := F[X])
      (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[X])
      (match (motive := ℕ → F[X]) 0 with
        | 0 => 0
        | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
        F[X])

Tactic:
simp only [add_zero]

Premises used: add_zero
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p q : F[X]
d : ℕ
h :
  (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
    HAdd.hAdd (α := F[X]) (β := F[X])
      (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[X])
      (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
        F[X])
⊢ ((p + q).sum fun (x : ℕ) (r : F) ↦ HSMul.hSMul (β := F[X]) r (preHilbertPoly F d x)) =
    HAdd.hAdd (α := F[X]) (∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i))
      (∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i))

Tactic:
sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

Premises used: Polynomial.sum, zero_smul, Polynomial.sum_add_index, add_smul, Polynomial.preHilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p q : F[X]
d : ℕ
h :
  (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
    HAdd.hAdd (α := F[X]) (β := F[X])
      (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[X])
      (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
        F[X])
⊢ ((p + q).sum fun (x : ℕ) (r : F) ↦ HSMul.hSMul (β := F[X]) r (preHilbertPoly F d x)) =
    HAdd.hAdd (α := F[X]) (∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i))
      (∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i))

Tactic:
exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

Premises used: zero_smul, Polynomial.sum_add_index, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
p q : F[X]
d : ℕ
zero :
  (match (motive := ℕ → F[X]) 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
    HAdd.hAdd (α := F[X]) (β := F[X])
      (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[X])
      (match (motive := ℕ → F[X]) 0 with
        | 0 => 0
        | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
        F[X])
succ :
  ∀ (d : ℕ),
    (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
        HAdd.hAdd (α := F[X]) (β := F[X])
          (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[X])
          (match (motive := ℕ → F[X]) d with
            | 0 => 0
            | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
            F[X]) →
      (match (motive := ℕ → F[X]) d + 1 with
        | 0 => 0
        | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
        HAdd.hAdd (α := F[X]) (β := F[X])
          (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[X])
          (match (motive := ℕ → F[X]) d + 1 with
            | 0 => 0
            | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
            F[X])
⊢ (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (p + q).support, HSMul.hSMul (β := F[X]) ((p + q).coeff i) (preHilbertPoly F d i)) =
    HAdd.hAdd (α := F[X]) (β := F[X])
      (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[X])
      (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ q.support, HSMul.hSMul (β := F[X]) (q.coeff i) (preHilbertPoly F d i) :
        F[X])

Tactic:
induction d with
  | zero => simp only [add_zero]
  | succ d _ =>
      simp only
      rw [← sum_def _ fun _ r => r • _]
      exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

Premises used: zero_smul, Polynomial.sum_add_index, Polynomial.sum_def, Nat.zero, HSMul.hSMul, add_zero, OfNat.ofNat, Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
d : ℕ
delta :
  (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
    HSMul.hSMul (β := F[X]) a
      (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[X])
⊢ (a • p).hilbertPoly d = a • p.hilbertPoly d

Tactic:
delta hilbertPoly

Premises used: Polynomial.hilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
⊢ (match (motive := ℕ → F[X]) 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
    HSMul.hSMul (β := F[X]) a
      (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[X])

Tactic:
simp only [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
d : ℕ
h :
  (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
    HSMul.hSMul (β := F[X]) a
      (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[X])
succ :
  Eq (α := F[X]) (p.sum fun (n : ℕ) (a_1 : F) ↦ HSMul.hSMul (β := F[X]) (a • a_1) (preHilbertPoly F d n))
    (p.sum fun (n : ℕ) (a_1 : F) ↦ a • HSMul.hSMul (β := F[X]) a_1 (preHilbertPoly F d n))
⊢ ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i) =
    HSMul.hSMul (β := F[X]) a (∑ i ∈ p.support, HSMul.hSMul (β := F[X]) (p.coeff i) (preHilbertPoly F d i))

Tactic:
rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
        sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]

Premises used: Polynomial.sum_smul_index', Polynomial.smul_sum, Polynomial.sum_def, HSMul.hSMul
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
d : ℕ
h :
  (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
    HSMul.hSMul (β := F[X]) a
      (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[X])
⊢ Eq (α := F[X]) (p.sum fun (n : ℕ) (a_1 : F) ↦ HSMul.hSMul (β := F[X]) (a • a_1) (preHilbertPoly F d n))
    (p.sum fun (n : ℕ) (a_1 : F) ↦ a • HSMul.hSMul (β := F[X]) a_1 (preHilbertPoly F d n))

Tactic:
simp only [smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
d : ℕ
zero :
  (match (motive := ℕ → F[X]) 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
    HSMul.hSMul (β := F[X]) a
      (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[X])
succ :
  ∀ (d : ℕ),
    (match (motive := ℕ → F[X]) d with
        | 0 => 0
        | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
        HSMul.hSMul (β := F[X]) a
          (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[X]) →
      (match (motive := ℕ → F[X]) d + 1 with
        | 0 => 0
        | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
        HSMul.hSMul (β := F[X]) a
          (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[X])
⊢ (match (motive := ℕ → F[X]) d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, HSMul.hSMul (β := F[X]) ((a • p).coeff i) (preHilbertPoly F d i)) =
    HSMul.hSMul (β := F[X]) a
      (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[X])

Tactic:
induction d with
  | zero => simp only [smul_zero]
  | succ d _ =>
      simp only
      rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
        sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]
      simp only [smul_assoc]

Premises used: Polynomial.sum_smul_index', smul_assoc, smul_zero, Polynomial.smul_sum, Polynomial.sum_def, Nat.zero, HSMul.hSMul, Nat.succ
-- 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
delta :
  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)
⊢ (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) (p.hilbertPoly d)

Tactic:
delta hilbertPoly

Premises used: Polynomial.hilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
zero : p.coeff n = 0
⊢ 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)

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

Premises used: PowerSeries.invOneSubPow_zero, Polynomial.eval_zero, Units.val_one, mul_one, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = 0

Tactic:
coeff_eq_zero_of_natDegree_lt hn

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt hn

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
succ :
  Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
    (∑ x ∈ p.support, p.coeff x * eval (↑n : F) (preHilbertPoly F d x) : 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)

Tactic:
simp only [eval_finsetSum, eval_smul, smul_eq_mul]

Premises used: Polynomial.eval_finsetSum, Polynomial.eval_smul, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
succ :
  Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
    (∑ i : ↥p.support, p.coeff (↑i : ℕ) * eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) : F)
⊢ Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
    (∑ x ∈ p.support, p.coeff x * eval (↑n : F) (preHilbertPoly F d x) : F)

Tactic:
rw [← Finset.sum_coe_sort]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
⊢ ∀ (i : ↥p.support), (↑i : ℕ) ≤ n

Tactic:
have h_le (i : p.support) : (i : ℕ) ≤ n :=
        le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
i : ↥p.support
rw : Eq.{u_1 + 1} (α := F) (↑((n - (↑i : ℕ) + d).choose d) : F) (↑((n + d - (↑i : ℕ)).choose d) : F)
rw₁ rw₂ : Eq.{u_1 + 1} (α := F) (↑((n - (↑i : ℕ) + d).choose d) : F) (↑((n - (↑i : ℕ) + d).choose d) : F)
⊢ eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)

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

Premises used: Nat.sub_add_comm, Polynomial.preHilbertPoly_eq_choose_sub_add
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
⊢ ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)

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)]
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
succ :
  Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
    (∑ x : ↥p.support, p.coeff (↑x : ℕ) * (↑((n + d - (↑x : ℕ)).choose d) : F) : F)
⊢ Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
    (∑ i : ↥p.support, p.coeff (↑i : ℕ) * eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) : F)

Tactic:
simp_rw [h]
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
succ :
  Eq.{u_1 + 1} (α := F)
    (∑ k ∈ Finset.range n.succ,
      HMul.hMul (α := F) (β := F) ((PowerSeries.coeff (k, n - k).1 : (a : F⟦X⟧) → F) (↑p : F⟦X⟧) : F)
        ((PowerSeries.coeff (k, n - k).2 : (a : F⟦X⟧) → F)
            (mk fun (n : ℕ) ↦ (↑((d.succ - 1 + n).choose (d.succ - 1)) : F)) :
          F))
    (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))
⊢ Eq (α := F) ((PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) : F)
    (∑ x : ↥p.support, p.coeff (↑x : ℕ) * (↑((n + d - (↑x : ℕ)).choose d) : F) : F)

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

Premises used: Nat.choose, HMul.hMul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Nat.zero_lt_succ, HSub.hSub, Nat.cast, Polynomial.coeff, PowerSeries.coeff_mul, HAdd.hAdd, PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos, Finset.sum_coe_sort
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
succ :
  Eq.{u_1 + 1} (α := F) (∑ x ∈ Finset.range n.succ, p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F))
    (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))
⊢ Eq.{u_1 + 1} (α := F)
    (∑ k ∈ Finset.range n.succ,
      HMul.hMul (α := F) (β := F) ((PowerSeries.coeff (k, n - k).1 : (a : F⟦X⟧) → F) (↑p : F⟦X⟧) : F)
        ((PowerSeries.coeff (k, n - k).2 : (a : F⟦X⟧) → F)
            (mk fun (n : ℕ) ↦ (↑((d.succ - 1 + n).choose (d.succ - 1)) : F)) :
          F))
    (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))

Tactic:
simp only [coeff_coe, coeff_mk]

Premises used: PowerSeries.coeff_mk, Polynomial.coeff_coe