awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
⊢ 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 : ∀ (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)]
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑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)
    (∑ i : ↥p.support, p.coeff (↑i : ℕ) * eval (↑n : F) (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 : ℕ) * (↑((n + d - (↑x : ℕ)).choose d) : F) : F)
Tactic: simp_rw [h]
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑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)
have 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))
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)]
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑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))
have 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))
Tactic: simp only [coeff_coe, coeff_mk]
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
⊢ 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))
have succ : Eq.{u_1 + 1} (α := F) (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))
  (∑ x ∈ Finset.range n.succ, p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F))
Tactic: symm
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
⊢ Eq.{u_1 + 1} (α := F) (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))
    (∑ x ∈ Finset.range n.succ, p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F))
have succ : ∀ (s : ℕ) (hs : s ∈ p.support), s ∈ Finset.range n.succ
Tactic: refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
succ : ∀ (s : ℕ) (hs : s ∈ p.support), s ∈ Finset.range n.succ
⊢ Eq.{u_1 + 1} (α := F) (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))
    (∑ x ∈ Finset.range n.succ, p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F))
have succ₁ : ∀ (x : ℕ) (hx : x ∈ Finset.range n.succ \ p.support),
  p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
Tactic: refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
succ : ∀ (s : ℕ) (hs : s ∈ p.support), s ∈ Finset.range n.succ
succ₁ :
  ∀ (x : ℕ) (hx : x ∈ Finset.range n.succ \ p.support),
    p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
⊢ Eq.{u_1 + 1} (α := F) (∑ i ∈ p.support, p.coeff i * (↑((n + d - i).choose d) : F))
    (∑ x ∈ Finset.range n.succ, p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F))
have succ₂ : ∀ (x : ℕ) (hx : x ∈ p.support),
  p.coeff x * (↑((n + d - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
Tactic: refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
s : ℕ
hs : s ∈ p.support
⊢ s ∈ Finset.range n.succ
have succ : s ≤ n
Tactic: rw [Finset.mem_range_succ_iff]
-- 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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
x : ℕ
hx : x ∈ Finset.range n.succ \ p.support
⊢ p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
have hx₁ : x ∈ Finset.range n.succ ∧ p.coeff x = 0
Tactic: simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
Cleared hypotheses: hx
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
x : ℕ
hx : x ∈ Finset.range n.succ ∧ p.coeff x = 0
⊢ p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
have succ : HMul.hMul (α := F) 0 (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
Tactic: rw [hx.2, zero_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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
x : ℕ
hx : x ∈ Finset.range n.succ ∧ p.coeff x = 0
succ : HMul.hMul (α := F) 0 (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
⊢ p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0
have succ₁ : Eq.{u_1 + 1} (α := F) 0 0
Tactic: rw [hx.2, zero_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)
h_le : ∀ (i : ↥p.support), (↑i : ℕ) ≤ n
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * (↑((n + d - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
have succ : p.coeff x * (↑((d + n - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
Tactic: rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
x : ℕ
hx : x ∈ p.support
succ : p.coeff x * (↑((d + n - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
⊢ p.coeff x * (↑((n + d - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
have succ₁ : p.coeff x * (↑((d + (n - (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ p.support) x hx) : ℕ))).choose d) : F) =
  p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
Tactic: rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
-- 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
h : ∀ (i : ↥p.support), eval (↑n : F) (preHilbertPoly F d (↑i : ℕ)) = (↑((n + d - (↑i : ℕ)).choose d) : F)
x : ℕ
hx : x ∈ p.support
succ : p.coeff x * (↑((d + n - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
succ₁ :
  p.coeff x * (↑((d + (n - (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ p.support) x hx) : ℕ))).choose d) : F) =
    p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
succ₂ :
  p.coeff x * (↑((d + (n - (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ p.support) x hx) : ℕ))).choose d) : F) =
    p.coeff x * (↑((d + 1 - 1 + (n - x)).choose (d + 1 - 1)) : F)
⊢ p.coeff x * (↑((n + d - x).choose d) : F) = p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F)
have succ₃ : p.coeff x * (↑((d + (n - (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ p.support) x hx) : ℕ))).choose d) : F) =
  p.coeff x * (↑((d + (n - x)).choose d) : F)
Tactic: rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
-- 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
⊢ 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)
have zero : 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: induction d with
  | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
            exact coeff_eq_zero_of_natDegree_lt hn
  | succ d hd =>
      simp only [eval_finsetSum, eval_smul, smul_eq_mul]
      rw [← Finset.sum_coe_sort]
      have h_le (i : p.support) : (i : ℕ) ≤ n :=
        le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
      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)]
      simp_rw [h]
      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)]
      simp only [coeff_coe, coeff_mk]
      symm
      refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
      · rw [Finset.mem_range_succ_iff]
        exact h_le ⟨s, hs⟩
      · simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
        rw [hx.2, zero_mul]
      · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
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
zero :
  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)
⊢ 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)
have succ : ∀ (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)
Tactic: induction d with
  | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
            exact coeff_eq_zero_of_natDegree_lt hn
  | succ d hd =>
      simp only [eval_finsetSum, eval_smul, smul_eq_mul]
      rw [← Finset.sum_coe_sort]
      have h_le (i : p.support) : (i : ℕ) ≤ n :=
        le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
      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)]
      simp_rw [h]
      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)]
      simp only [coeff_coe, coeff_mk]
      symm
      refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
      · rw [Finset.mem_range_succ_iff]
        exact h_le ⟨s, hs⟩
      · simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
        rw [hx.2, zero_mul]
      · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
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 : ℕ
⊢ ∃! h : F[X],
    ∃ (N : ℕ),
      ∀ n > N, (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h
have h : (fun (h : F[X]) ↦
      ∃ (N : ℕ),
        ∀ n > N, (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
    (p.hilbertPoly d) ∧
  ∀ (y : F[X]),
    (fun (h : F[X]) ↦
          ∃ (N : ℕ),
            ∀ n > N,
              (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
        y →
      y = p.hilbertPoly d
Tactic: use hilbertPoly p 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 : ℕ
⊢ (fun (h : F[X]) ↦
        ∃ (N : ℕ),
          ∀ n > N,
            (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
      (p.hilbertPoly d) ∧
    ∀ (y : F[X]),
      (fun (h : F[X]) ↦
            ∃ (N : ℕ),
              ∀ n > N,
                (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
          y →
        y = p.hilbertPoly d
have h : (fun (h : F[X]) ↦
    ∃ (N : ℕ),
      ∀ n > N, (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
  (p.hilbertPoly d)
Tactic: constructor
-- 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 : ℕ
h :
  (fun (h : F[X]) ↦
      ∃ (N : ℕ),
        ∀ n > N, (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
    (p.hilbertPoly d)
⊢ (fun (h : F[X]) ↦
        ∃ (N : ℕ),
          ∀ n > N,
            (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
      (p.hilbertPoly d) ∧
    ∀ (y : F[X]),
      (fun (h : F[X]) ↦
            ∃ (N : ℕ),
              ∀ n > N,
                (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
          y →
        y = p.hilbertPoly d
have h₁ : ∀ (y : F[X]),
  (fun (h : F[X]) ↦
        ∃ (N : ℕ),
          ∀ n > N,
            (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
      y →
    y = p.hilbertPoly d
Tactic: constructor
-- 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 : ℕ
⊢ (fun (h : F[X]) ↦
      ∃ (N : ℕ),
        ∀ n > N, (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h)
    (p.hilbertPoly d)
have h : ∀ n > p.natDegree,
  (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) (p.hilbertPoly d)
Tactic: use p.natDegree
-- 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 : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) = eval (↑n : F) h
⊢ h = p.hilbertPoly d
have h₁ : Set.Infinite.{u_1} (α := F) {x : F | eval x h = eval x (p.hilbertPoly d)}
Tactic: apply eq_of_infinite_eval_eq h (hilbertPoly p d)