awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (∑ 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))
⊢ 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:
symm
-- 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)
⊢ 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:
Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Premises used: Finset.sum_subset_zero_on_sdiff
-- 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 : ∀ (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
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)
⊢ 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:
refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Premises used: Finset.sum_subset_zero_on_sdiff
-- 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)
s : ℕ
hs : s ∈ p.support
succ : s ≤ n
⊢ s ∈ Finset.range n.succ

Tactic:
rw [Finset.mem_range_succ_iff]

Premises used: Finset.mem_range_succ_iff
-- 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)
s : ℕ
hs : s ∈ p.support
⊢ s ≤ n

Tactic:
h_le ⟨s, hs⟩

Premises used: Subtype.mk
-- 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)
s : ℕ
hs : s ∈ p.support
⊢ s ≤ n

Tactic:
exact h_le ⟨s, hs⟩

Premises used: Subtype.mk
-- 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)
x : ℕ
hx : x ∈ Finset.range n.succ \ p.support
⊢ x ∈ Finset.range n.succ ∧ p.coeff x = 0

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

Premises used: Classical.not_not, Polynomial.mem_support_iff, Finset.mem_sdiff
-- 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)
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
succ₁ succ₂ : Eq.{u_1 + 1} (α := F) 0 0
⊢ p.coeff x * (↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) : F) = 0

Tactic:
rw [hx.2, zero_mul]

Premises used: MulZeroClass.zero_mul, And.right
-- 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)
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)
succ₃ 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)
⊢ p.coeff x * (↑((n + d - 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]

Premises used: Nat.succ_eq_add_one, Nat.add_sub_assoc, add_comm, Subtype.mk, add_tsub_cancel_right
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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) ∧
    ∀ (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
⊢ ∃! 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

Tactic:
use hilbertPoly p d

Premises used: Polynomial.hilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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)
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
⊢ (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:
constructor
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
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)
⊢ (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:
use p.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
⊢ ∀ 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:
fun n => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d

Premises used: Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
⊢ ∀ 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:
exact fun n => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d

Premises used: Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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₁ : Set.Infinite.{u_1} (α := F) {x : F | eval x h = eval x (p.hilbertPoly d)}
⊢ h = p.hilbertPoly d

Tactic:
apply eq_of_infinite_eval_eq h (hilbertPoly p d)

Premises used: Polynomial.hilbertPoly, Polynomial.eq_of_infinite_eval_eq
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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₁ : Subset.{u_1} (α := Set F) (Nat.cast '' Set.Ioi (max N p.natDegree)) {x : F | eval x h = eval x (p.hilbertPoly d)}
⊢ Set.Infinite.{u_1} (α := F) {x : F | eval x h = eval x (p.hilbertPoly d)}

Tactic:
apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono

Premises used: Set.Infinite.mono, Set.Infinite.image, Function.Injective.injOn, Set.Ioi_infinite, Max.max, Polynomial.natDegree, Nat.cast_injective
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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
n : ℕ
hn : n ∈ Set.Ioi (max N p.natDegree)
⊢ N < n ∧ p.natDegree < n

Tactic:
simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hn ⊢

Premises used: Set.mem_Ioi, Set.mem_setOf_eq, sup_lt_iff
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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
n : ℕ
hn : N < n ∧ p.natDegree < n
h₁ : eval (↑n : F) h = (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧))
h₂ h₃ : eval (↑n : F) h = eval (↑n : F) h
⊢ eval (↑n : F) h = eval (↑n : F) (p.hilbertPoly d)

Tactic:
rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]

Premises used: Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, And.right, And.left
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p h : F[X]
d 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

Tactic:
ExistsUnique.unique (existsUnique_hilbertPoly p d) ⟨N, hhN⟩
    ⟨p.natDegree, fun _ x => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d x⟩

Premises used: Polynomial.existsUnique_hilbertPoly, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, Exists.intro, ExistsUnique.unique, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
apply :
  ∀ n > (p * HSub.hSub (α := F[X]) 1 X).natDegree,
    (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) =
      eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
⊢ (p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1) = p.hilbertPoly d

Tactic:
apply eq_hilbertPoly_of_forall_coeff_eq_eval (p * (1 - X)).natDegree

Premises used: Polynomial.eq_hilbertPoly_of_forall_coeff_eq_eval
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * HSub.hSub (α := F[X]) 1 X).natDegree
⊢ HSub.hSub (α := F⟦X⟧) 1 PowerSeries.X = (↑(HSub.hSub (α := F[X]) 1 X) : F⟦X⟧)

Tactic:
simp only [coe_sub, coe_one, coe_X]

Premises used: Polynomial.coe_one, Polynomial.coe_X, Polynomial.coe_sub
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * HSub.hSub (α := F[X]) 1 X).natDegree
⊢ HSub.hSub (α := F⟦X⟧) 1 PowerSeries.X = (↑(HSub.hSub (α := F[X]) 1 X) : F⟦X⟧)

Tactic:
have heq : 1 - PowerSeries.X = ((1 - X : F[X]) : F⟦X⟧) := by simp only [coe_sub, coe_one, coe_X]
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * HSub.hSub (α := F[X]) 1 X).natDegree
heq : HSub.hSub (α := F⟦X⟧) 1 PowerSeries.X = (↑(HSub.hSub (α := F[X]) 1 X) : F⟦X⟧)
rw :
  (PowerSeries.coeff n : (a : F⟦X⟧) → F)
      ((↑p : F⟦X⟧) *
        (HPow.hPow (β := ℕ) (HSub.hSub (α := F⟦X⟧) 1 PowerSeries.X) 1 * (↑(invOneSubPow F (d + 1)) : F⟦X⟧))) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
rw₁ :
  (PowerSeries.coeff n : (a : F⟦X⟧) → F)
      ((↑p : F⟦X⟧) * (HSub.hSub (α := F⟦X⟧) 1 PowerSeries.X * (↑(invOneSubPow F (d + 1)) : F⟦X⟧))) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
rw₂ :
  (PowerSeries.coeff n : (a : F⟦X⟧) → F)
      ((↑p : F⟦X⟧) * HSub.hSub (α := F⟦X⟧) 1 PowerSeries.X * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
rw₃ :
  (PowerSeries.coeff n : (a : F⟦X⟧) → F)
      ((↑p : F⟦X⟧) * (↑(HSub.hSub (α := F[X]) 1 X) : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
rw₄ :
  (PowerSeries.coeff n : (a : F⟦X⟧) → F)
      ((↑(p * HSub.hSub (α := F[X]) 1 X) : F⟦X⟧) * (↑(invOneSubPow F (d + 1)) : F⟦X⟧)) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
rw₅ rw₆ :
  eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1)) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))
⊢ (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧)) =
    eval (↑n : F) ((p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1))

Tactic:
rw [← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one, ← mul_assoc, heq,
    ← coe_mul, coeff_mul_invOneSubPow_eq_hilbertPoly_eval (d + 1) hn]

Premises used: mul_assoc, PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, HAdd.hAdd, Polynomial.coe_mul, pow_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
⊢ (p * HPow.hPow (β := ℕ) (HSub.hSub (α := F[X]) 1 X) 0).hilbertPoly (d + 0) = p.hilbertPoly d

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d e : ℕ
he : (p * HSub.hSub (α := F[X]) 1 X ^ e).hilbertPoly (d + e) = p.hilbertPoly d
succ :
  (p * (HSub.hSub (α := F[X]) 1 X ^ e * HPow.hPow (β := ℕ) (HSub.hSub (α := F[X]) 1 X) 1)).hilbertPoly (d + (e + 1)) =
    p.hilbertPoly d
succ₁ : (p * (HSub.hSub (α := F[X]) 1 X ^ e * HSub.hSub (α := F[X]) 1 X)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
succ₂ : (p * HSub.hSub (α := F[X]) 1 X ^ e * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
succ₃ : (p * HSub.hSub (α := F[X]) 1 X ^ e * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + e + 1) = p.hilbertPoly d
succ₄ : (p * HSub.hSub (α := F[X]) 1 X ^ e).hilbertPoly (d + e) = p.hilbertPoly d
succ₅ succ₆ : p.hilbertPoly d = p.hilbertPoly d
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d

Tactic:
rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]

Premises used: add_assoc, mul_assoc, pow_add, Polynomial.hilbertPoly_mul_one_sub_succ, pow_one
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d e : ℕ
zero : (p * HPow.hPow (β := ℕ) (HSub.hSub (α := F[X]) 1 X) 0).hilbertPoly (d + 0) = p.hilbertPoly d
succ :
  ∀ (e : ℕ) (he : (p * HSub.hSub (α := F[X]) 1 X ^ e).hilbertPoly (d + e) = p.hilbertPoly d),
    (p * HSub.hSub (α := F[X]) 1 X ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ e).hilbertPoly (d + e) = p.hilbertPoly d

Tactic:
induction e with
  | zero => simp
  | succ e he => rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]

Premises used: add_assoc, mul_assoc, pow_add, Polynomial.hilbertPoly_mul_one_sub_succ, pow_one, Nat.zero, Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
pos : ∀ (hp : p = 0), p.hilbertPoly d = 0
neg : ∀ (hp : ¬p = 0), p.hilbertPoly d = 0
⊢ p.hilbertPoly d = 0

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : p = 0
pos : Eq.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
pos₁ pos₂ : Eq.{u_1 + 1} (α := F[X]) 0 0
⊢ p.hilbertPoly d = 0

Tactic:
rw [hp, hilbertPoly_zero_left]

Premises used: Polynomial.hilbertPoly_zero_left
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
neg :
  ∀ (q : F[X]) (hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q)
    (hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q), p.hilbertPoly d = 0
⊢ p.hilbertPoly d = 0

Tactic:
rcases exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1 with ⟨q, hq1, hq2⟩

Premises used: Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
simp : p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p
⊢ p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p

Tactic:
simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]

Premises used: neg_sub, mul_assoc, neg_mul, mul_pow, one_mul
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
⊢ p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p

Tactic:
hq1.trans (mul_comm _ _)

Premises used: mul_comm, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
⊢ p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p

Tactic:
exact hq1.trans (mul_comm _ _)

Premises used: mul_comm, Eq.trans