awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
ih :
  Eq (α := ℝ → ℝ) (deriv^[n] fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) fun (x : ℝ) ↦
    HPow.hPow (α := ℝ) (-1) n *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
deriv_gaussian :
  deriv (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
⊢ deriv^[n + 1] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (-1) (n + 1) *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite (n + 1)) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
have succ : HPow.hPow (α := ℝ) (-1) n *
    (HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) : ℝ)
        (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) +
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (-x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))) =
  HPow.hPow (α := ℝ) (-1) n * -1 *
    (HSub.hSub (β := ℝ) (HMul.hMul (β := ℝ) x ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ))
        ((aeval x : (a : ℤ[X]) → ℝ) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) : ℝ) *
      Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
Tactic: rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ),
      deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
ih :
  Eq (α := ℝ → ℝ) (deriv^[n] fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) fun (x : ℝ) ↦
    HPow.hPow (α := ℝ) (-1) n *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
deriv_gaussian :
  deriv (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
succ :
  HPow.hPow (α := ℝ) (-1) n *
      (HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) : ℝ)
          (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) +
        HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ)
          (-x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))) =
    HPow.hPow (α := ℝ) (-1) n * -1 *
      (HSub.hSub (β := ℝ) (HMul.hMul (β := ℝ) x ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ))
          ((aeval x : (a : ℤ[X]) → ℝ) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) : ℝ) *
        Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
⊢ deriv^[n + 1] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (-1) (n + 1) *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite (n + 1)) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
have succ₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (aeval x : (a : ℤ[X]) → ℝ) (hermite n)) x
Tactic: rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ),
      deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
ih :
  Eq (α := ℝ → ℝ) (deriv^[n] fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) fun (x : ℝ) ↦
    HPow.hPow (α := ℝ) (-1) n *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
deriv_gaussian :
  deriv (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
succ :
  HPow.hPow (α := ℝ) (-1) n *
      (HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) : ℝ)
          (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) +
        HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ)
          (-x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))) =
    HPow.hPow (α := ℝ) (-1) n * -1 *
      (HSub.hSub (β := ℝ) (HMul.hMul (β := ℝ) x ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ))
          ((aeval x : (a : ℤ[X]) → ℝ) ((derivative : (a : ℤ[X]) → ℤ[X]) (hermite n) : ℤ[X]) : ℝ) *
        Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
succ₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (aeval x : (a : ℤ[X]) → ℝ) (hermite n)) x
⊢ deriv^[n + 1] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (-1) (n + 1) *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite (n + 1)) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
have succ₂ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) x
Tactic: rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ),
      deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
ih :
  Eq (α := ℝ → ℝ) (deriv^[n] fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) fun (x : ℝ) ↦
    HPow.hPow (α := ℝ) (-1) n *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
deriv_gaussian :
  deriv (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) x
have succ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -(HPow.hPow (β := ℕ) x 2 / 2)) x
Tactic: apply DifferentiableAt.exp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
⊢ deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (-1) n *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
have zero : ∀ (x : ℝ),
  deriv^[0] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 0 *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite 0) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
Tactic: induction n generalizing x with
  | zero => rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
  | succ n ih =>
    replace ih : deriv^[n] _ = _ := _root_.funext ih
    have deriv_gaussian :
      deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [mul_comm, ← neg_mul]`
      rw [deriv_exp (by simp)]
      simp [mul_comm]
    rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ),
      deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
    · ring
    · apply Polynomial.differentiable_aeval
    · apply DifferentiableAt.exp; simp
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
zero :
  ∀ (x : ℝ),
    deriv^[0] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
      HPow.hPow (α := ℝ) (β := ℕ) (-1) 0 *
        HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite 0) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
⊢ deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (-1) n *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (x : ℝ),
      deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
        HPow.hPow (α := ℝ) (-1) n *
          HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))))
  (x : ℝ),
  deriv^[n + 1] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HPow.hPow (α := ℝ) (-1) (n + 1) *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite (n + 1)) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
Tactic: induction n generalizing x with
  | zero => rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
  | succ n ih =>
    replace ih : deriv^[n] _ = _ := _root_.funext ih
    have deriv_gaussian :
      deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [mul_comm, ← neg_mul]`
      rw [deriv_exp (by simp)]
      simp [mul_comm]
    rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_fun_mul, pow_succ (-1 : ℝ),
      deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]
    · ring
    · apply Polynomial.differentiable_aeval
    · apply DifferentiableAt.exp; simp
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
⊢ (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n)
        (deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x : ℝ) /
      Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
have rw : (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
  HPow.hPow (α := ℝ) (-1) n *
      (HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) *
        Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) /
    Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
Tactic: rw [deriv_gaussian_eq_hermite_mul_gaussian]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
⊢ (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HPow.hPow (α := ℝ) (-1) n *
        (HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) *
          Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) /
      Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
have field_simp : (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
  HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (-1) n) 2)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
⊢ (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (-1) n) 2)
have rw : (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
  HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (α := ℝ) (-1) (n * 2))
Tactic: rw [← pow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
n : ℕ
x : ℝ
⊢ (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n)
        (deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x : ℝ) *
      Real.exp (HPow.hPow (β := ℕ) x 2 / 2)
have rw : HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n)
      (deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x : ℝ) /
    (Real.exp (HPow.hPow (β := ℕ) x 2 / 2))⁻¹ =
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n)
      (deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x : ℝ) *
    Real.exp (HPow.hPow (β := ℕ) x 2 / 2)
Tactic: rw [hermite_eq_deriv_gaussian, Real.exp_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
⊢ 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 : ℕ
⊢ natDegree (preHilbertPoly F d k) = d
have hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
Tactic: have hne : (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 : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ natDegree (preHilbertPoly F d k) = d
have rw : (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
      (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
  d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₄ : d * (X + HSub.hSub (α := F[X]) 1 ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₄ : d * (X + HSub.hSub (α := F[X]) 1 ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₅ : d * (X + HSub.hSub (α := F[X]) ((C : (a : F) → F[X]) 1) ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₄ : d * (X + HSub.hSub (α := F[X]) 1 ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₅ : d * (X + HSub.hSub (α := F[X]) ((C : (a : F) → F[X]) 1) ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₆ : d * (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (HSub.hSub (α := F) 1 (↑k : F)) : F[X])).natDegree = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₄ : d * (X + HSub.hSub (α := F[X]) 1 ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₅ : d * (X + HSub.hSub (α := F[X]) ((C : (a : F) → F[X]) 1) ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₆ :
  d * (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (HSub.hSub (α := F) 1 (↑k : F)) : F[X])).natDegree = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₇ : d * natDegree.{u_1} (R := F) X = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₄ : d * (X + HSub.hSub (α := F[X]) 1 ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₅ : d * (X + HSub.hSub (α := F[X]) ((C : (a : F) → F[X]) 1) ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₆ :
  d * (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (HSub.hSub (α := F) 1 (↑k : F)) : F[X])).natDegree = d
rw₇ : d * natDegree.{u_1} (R := F) X = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₈ : d * 1 = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, 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
rw :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
        (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).natDegree =
    d
rw₁ : (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree = d
rw₂ : natDegree (ascPochhammer F d) * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₃ : d * (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1).natDegree = d
rw₄ : d * (X + HSub.hSub (α := F[X]) 1 ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₅ : d * (X + HSub.hSub (α := F[X]) ((C : (a : F) → F[X]) 1) ((C : (a : F) → F[X]) (↑k : F))).natDegree = d
rw₆ :
  d * (HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (HSub.hSub (α := F) 1 (↑k : F)) : F[X])).natDegree = d
rw₇ : d * natDegree.{u_1} (R := F) X = d
rw₈ : d * 1 = d
⊢ natDegree (preHilbertPoly F d k) = d
have rw₉ : d = d
Tactic: rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree,
    add_comm_sub, ← C_1, ← map_sub, natDegree_add_C, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
⊢ (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      d =
    (↑d ! : F)⁻¹
have hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
Tactic: have hne : (d ! : F) ≠ 0 := by norm_cast; positivity
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.HilbertPoly (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      d =
    (↑d ! : F)⁻¹
have heq : d = (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree
Tactic: have heq : d = ((ascPochhammer F d).comp (X - C (k : F) + 1)).natDegree :=
    (natDegree_preHilbertPoly F d k).symm.trans (natDegree_smul _ (inv_ne_zero hne))
-- 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
      d =
    (↑d ! : F)⁻¹
have nth_rw : (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)⁻¹
Tactic: nth_rw 3 [heq]