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
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
⊢ Set.Infinite.{u_1} (α := F) {x : F | eval x h = eval x (p.hilbertPoly d)}
have h₁ : Subset.{u_1} (α := Set F) (Nat.cast '' Set.Ioi (max N p.natDegree)) {x : F | eval x h = eval x (p.hilbertPoly d)}
Tactic: apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono
-- 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]
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)
⊢ Membership.mem (γ := Set F) {x : F | eval x h = eval x (p.hilbertPoly d)} (↑n : F)
have hn₁ : N < n ∧ p.natDegree < n
Tactic: simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hn ⊢
Cleared hypotheses: hn
-- 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
n : ℕ
hn : N < n ∧ p.natDegree < n
⊢ eval (↑n : F) h = eval (↑n : F) (p.hilbertPoly d)
have h₁ : eval (↑n : F) h = (PowerSeries.coeff n : (a : F⟦X⟧) → F) ((↑p : F⟦X⟧) * (↑(invOneSubPow F d) : F⟦X⟧))
Tactic: rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]
-- 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
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⟧))
⊢ eval (↑n : F) h = eval (↑n : F) (p.hilbertPoly d)
have h₂ : eval (↑n : F) h = eval (↑n : F) h
Tactic: rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]
-- 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 : ℕ
⊢ (p * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + 1) = p.hilbertPoly d
have 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))
Tactic: apply eq_hilbertPoly_of_forall_coeff_eq_eval (p * (1 - X)).natDegree
-- 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]
d n : ℕ
hn : 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))
have heq : 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]
-- 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 : 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⟧)
⊢ (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))
have 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))
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]
-- 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 : 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))
⊢ (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))
have 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))
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]
-- 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 : 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))
⊢ (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))
have 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))
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]
-- 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 : 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))
⊢ (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))
have 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))
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]
-- 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 : 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))
⊢ (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))
have 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))
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]
-- 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 : 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))
⊢ (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))
have 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))
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]
-- 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 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
have 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
Tactic: rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
-- 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 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
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
have succ₁ : (p * (HSub.hSub (α := F[X]) 1 X ^ e * HSub.hSub (α := F[X]) 1 X)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
Tactic: rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
-- 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 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
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
have succ₂ : (p * HSub.hSub (α := F[X]) 1 X ^ e * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
Tactic: rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
-- 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 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
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
have succ₃ : (p * HSub.hSub (α := F[X]) 1 X ^ e * HSub.hSub (α := F[X]) 1 X).hilbertPoly (d + e + 1) = p.hilbertPoly d
Tactic: rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
-- 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 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
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d
have succ₅ : p.hilbertPoly d = p.hilbertPoly d
Tactic: rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
-- 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 e : ℕ
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ e).hilbertPoly (d + e) = p.hilbertPoly d
have zero : (p * HPow.hPow (β := ℕ) (HSub.hSub (α := F[X]) 1 X) 0).hilbertPoly (d + 0) = 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]
Cleared hypotheses: e
-- 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 e : ℕ
zero : (p * HPow.hPow (β := ℕ) (HSub.hSub (α := F[X]) 1 X) 0).hilbertPoly (d + 0) = p.hilbertPoly d
⊢ (p * HSub.hSub (α := F[X]) 1 X ^ e).hilbertPoly (d + e) = p.hilbertPoly d
have 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
Tactic: induction e with
  | zero => simp
  | succ e he => rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
Cleared hypotheses: e
-- 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 : ℕ
hdp : d ≤ rootMultiplicity 1 p
⊢ p.hilbertPoly d = 0
have pos : ∀ (hp : p = 0), p.hilbertPoly d = 0
Tactic: by_cases hp : p = 0
-- 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 : ℕ
hdp : d ≤ rootMultiplicity 1 p
pos : ∀ (hp : p = 0), p.hilbertPoly d = 0
⊢ p.hilbertPoly d = 0
have neg : ∀ (hp : ¬p = 0), p.hilbertPoly d = 0
Tactic: by_cases hp : p = 0
-- 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 : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : p = 0
⊢ p.hilbertPoly d = 0
have pos : Eq.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
Tactic: rw [hp, hilbertPoly_zero_left]
-- 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 : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : p = 0
pos : Eq.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
⊢ p.hilbertPoly d = 0
have pos₁ : Eq.{u_1 + 1} (α := F[X]) 0 0
Tactic: rw [hp, hilbertPoly_zero_left]
-- 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 : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
⊢ p.hilbertPoly d = 0
have 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
Tactic: rcases exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1 with ⟨q, hq1, hq2⟩
-- 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 : ℕ
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 * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
have simp : p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p
Tactic: simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]
-- 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 : ℕ
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
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
⊢ p.hilbertPoly d = 0
have neg : (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
    d =
  0
Tactic: rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc,
      hilbertPoly_mul_one_sub_pow_add, 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]
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
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
neg :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      d =
    0
⊢ p.hilbertPoly d = 0
have neg₁ : (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
    (0 + d) =
  0
Tactic: rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc,
      hilbertPoly_mul_one_sub_pow_add, 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]
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
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
neg :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      d =
    0
neg₁ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      (0 + d) =
    0
⊢ p.hilbertPoly d = 0
have neg₂ : (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
        HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d + d)).hilbertPoly
    (0 + d) =
  0
Tactic: rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc,
      hilbertPoly_mul_one_sub_pow_add, 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]
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
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
neg :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      d =
    0
neg₁ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      (0 + d) =
    0
neg₂ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
          HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d + d)).hilbertPoly
      (0 + d) =
    0
⊢ p.hilbertPoly d = 0
have neg₃ : (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
        (HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d) * HSub.hSub (α := F[X]) 1 X ^ d)).hilbertPoly
    (0 + d) =
  0
Tactic: rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc,
      hilbertPoly_mul_one_sub_pow_add, hilbertPoly]