awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
heq : d = (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree
⊢ (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree =
    (↑d ! : F)⁻¹
have _ : (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
    (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree =
  HSMul.hSMul (α := F) (↑d ! : F)⁻¹
    (comp (ascPochhammer F d)
        (HSub.hSub (α := F[X]) (β := F[X]) X
          ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff
Tactic: calc
  _ = (d ! : F)⁻¹ • ((ascPochhammer F d).comp (X - C ((k : F) - 1))).leadingCoeff := by
    simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]
  _ = (d ! : F)⁻¹ := by
    simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
      (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
heq : d = (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree
_ :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree =
    HSMul.hSMul (α := F) (↑d ! : F)⁻¹
      (comp (ascPochhammer F d)
          (HSub.hSub (α := F[X]) (β := F[X]) X
            ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff
⊢ (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree =
    (↑d ! : F)⁻¹
have _₁ : HSMul.hSMul (α := F) (↑d ! : F)⁻¹
    (comp (ascPochhammer F d)
        (HSub.hSub (α := F[X]) (β := F[X]) X
          ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff =
  (↑d ! : F)⁻¹
Tactic: calc
  _ = (d ! : F)⁻¹ • ((ascPochhammer F d).comp (X - C ((k : F) - 1))).leadingCoeff := by
    simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]
  _ = (d ! : F)⁻¹ := by
    simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
      (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
⊢ leadingCoeff (preHilbertPoly F d k) = (↑d ! : F)⁻¹
have rw : coeff (preHilbertPoly F d k) (natDegree (preHilbertPoly F d k)) = (↑d ! : F)⁻¹
Tactic: rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
rw : coeff (preHilbertPoly F d k) (natDegree (preHilbertPoly F d k)) = (↑d ! : F)⁻¹
⊢ leadingCoeff (preHilbertPoly F d k) = (↑d ! : F)⁻¹
have rw₁ : coeff (preHilbertPoly F d k) d = (↑d ! : F)⁻¹
Tactic: rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
rw : coeff (preHilbertPoly F d k) (natDegree (preHilbertPoly F d k)) = (↑d ! : F)⁻¹
rw₁ : coeff (preHilbertPoly F d k) d = (↑d ! : F)⁻¹
⊢ leadingCoeff (preHilbertPoly F d k) = (↑d ! : F)⁻¹
have rw₂ : Eq.{u_1 + 1} (α := F) (↑d ! : F)⁻¹ (↑d ! : F)⁻¹
Tactic: rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
have norm_cast : ¬d ! = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ eval (↑n : F) (preHilbertPoly F d k) = (↑((n - k + d).choose d) : F)
have this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
Tactic: have : (d ! : F) ≠ 0 := by norm_cast; positivity
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d) = (↑((n - k + d).choose d) : F)
have rw : HMul.hMul (α := F) (↑d ! : F)⁻¹ (↑((n - k + 1).ascFactorial d) : F) = (↑((n - k + d).choose d) : F)
Tactic: rw [ascPochhammer_nat_eq_natCast_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ eval (↑n : F) (preHilbertPoly F d k) = (↑((n - k + d).choose d) : F)
have _ : eval (↑n : F) (preHilbertPoly F d k) = (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d)
Tactic: calc
  _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbertPoly]
  _ = (n - k + d).choose d := by
    rw [ascPochhammer_nat_eq_natCast_ascFactorial];
    simp [field, ascFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
_ : eval (↑n : F) (preHilbertPoly F d k) = (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d)
⊢ eval (↑n : F) (preHilbertPoly F d k) = (↑((n - k + d).choose d) : F)
have _₁ : (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d) = (↑((n - k + d).choose d) : F)
Tactic: calc
  _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbertPoly]
  _ = (n - k + d).choose d := by
    rw [ascPochhammer_nat_eq_natCast_ascFactorial];
    simp [field, ascFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
d : ℕ
⊢ Eq.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
have delta : 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: delta hilbertPoly
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
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])
have 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])
Tactic: induction d with
  | zero => simp only
  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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])
⊢ 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])
have 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])
Tactic: induction d with
  | zero => simp only
  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
d : ℕ
⊢ (p + q).hilbertPoly d = p.hilbertPoly d + q.hilbertPoly d
have 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])
Tactic: delta hilbertPoly
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
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])
have 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])
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 ..)
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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])
⊢ (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])
have 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])
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 ..)
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
d : ℕ
⊢ (a • p).hilbertPoly d = a • p.hilbertPoly d
have 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])
Tactic: delta hilbertPoly
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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])
⊢ ∑ 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))
have 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))
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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
a : F
p : F[X]
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])
have 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])
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]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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])
⊢ (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])
have 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])
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]
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d n : ℕ
hn : p.natDegree < n
⊢ (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) (p.hilbertPoly d)
have 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)
Tactic: delta hilbertPoly
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
⊢ 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)
have zero : p.coeff n = 0
Tactic: simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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)
⊢ 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)
have 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)
Tactic: simp only [eval_finsetSum, eval_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Finset.sum_coe_sort]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (hypothesis)
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)
⊢ 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)
have h_le : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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)
have rw : Eq.{u_1 + 1} (α := F) (↑((n - (↑i : ℕ) + d).choose d) : F) (↑((n + d - (↑i : ℕ)).choose d) : F)
Tactic: rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
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)
⊢ eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
have rw₁ : Eq.{u_1 + 1} (α := F) (↑((n - (↑i : ℕ) + d).choose d) : F) (↑((n - (↑i : ℕ) + d).choose d) : F)
Tactic: rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]