awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
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 : ℝ
⊢ 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)))

Tactic:
replace ih : deriv^[n] _ = _ := _root_.funext ih
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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)))
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ -(HPow.hPow (β := ℕ) y 2 / 2)) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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)))
rw :
  Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) * deriv (fun (y : ℝ) ↦ -(HPow.hPow (β := ℕ) y 2 / 2)) x =
    -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
⊢ deriv (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))

Tactic:
rw [deriv_exp (by simp)]

Premises used: deriv_exp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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)))
⊢ Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) * deriv (fun (y : ℝ) ↦ -(HPow.hPow (β := ℕ) y 2 / 2)) x =
    -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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 (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))

Tactic:
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]
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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
succ₂ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 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:
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]

Premises used: Function.iterate_succ_apply', map_sub, deriv_fun_mul, pow_succ, Polynomial.deriv_aeval, Polynomial.hermite_succ, deriv_const_mul_field, map_mul, OfNat.ofNat, Neg.neg, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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))
⊢ 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:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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 : ℝ) ↦ (aeval x : (a : ℤ[X]) → ℝ) (hermite n)) x

Tactic:
apply Polynomial.differentiable_aeval

Premises used: Polynomial.differentiable_aeval
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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 : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -(HPow.hPow (β := ℕ) x 2 / 2)) x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))) x

Tactic:
apply DifferentiableAt.exp

Premises used: DifferentiableAt.exp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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 : ℝ) ↦ -(HPow.hPow (β := ℕ) x 2 / 2)) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
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)))
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)))
⊢ 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)))

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

Premises used: Function.iterate_succ_apply', Polynomial.C_1, map_sub, deriv_fun_mul, pow_succ, Polynomial.deriv_aeval, Polynomial.hermite_succ, Polynomial.differentiable_aeval, deriv_const_mul_field, pow_zero, map_mul, map_one, Polynomial.hermite_zero, DifferentiableAt.exp, Function.iterate_zero_apply, OfNat.ofNat, Neg.neg, one_mul, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
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))
⊢ (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))

Tactic:
rw [deriv_gaussian_eq_hermite_mul_gaussian]

Premises used: Polynomial.deriv_gaussian_eq_hermite_mul_gaussian
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
field_simp :
  (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (-1) n) 2)
⊢ (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:
field_simp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
rw :
  (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (α := ℝ) (-1) (n * 2))
⊢ (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (-1) n) 2)

Tactic:
rw [← pow_mul]

Premises used: pow_mul
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
⊢ (aeval x : (a : ℤ[X]) → ℝ) (hermite n) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) (HPow.hPow (α := ℝ) (-1) (n * 2))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
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)
⊢ (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)

Tactic:
rw [hermite_eq_deriv_gaussian, Real.exp_neg]

Premises used: Polynomial.hermite_eq_deriv_gaussian, Real.exp_neg
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
⊢ 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:
field
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
norm_cast : ¬d ! = 0
⊢ Ne.{u_1 + 1} (α := F) (↑d ! : F) 0

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
⊢ ¬d ! = 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
⊢ Ne.{u_1 + 1} (α := F) (↑d ! : F) 0

Tactic:
have hne : (d ! : F) ≠ 0 := by norm_cast; positivity
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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
rw₉ rw₁₀ : d = d
⊢ natDegree (preHilbertPoly F d k) = 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]

Premises used: Polynomial.natDegree_X, Polynomial.C_1, Polynomial.natDegree_smul, map_sub, Polynomial.natDegree_comp, ascPochhammer_natDegree, add_comm_sub, inv_ne_zero, mul_one, Polynomial.preHilbertPoly, Polynomial.natDegree_add_C
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ 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))
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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
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)⁻¹
⊢ (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)⁻¹

Tactic:
nth_rw 3 [heq]
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
heq : d = (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree
⊢ (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree =
    HSMul.hSMul (α := F) (↑d ! : F)⁻¹
      (comp (ascPochhammer F d)
          (HSub.hSub (α := F[X]) (β := F[X]) X
            ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff

Tactic:
simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]

Premises used: sub_add, Polynomial.C_1, map_sub, Polynomial.coeff_natDegree, Polynomial.coeff_smul
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
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]) (β := F[X]) X
            ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff =
    (↑d ! : F)⁻¹

Tactic:
simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
      (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]

Premises used: one_pow, ne_of_eq_of_ne, monic_ascPochhammer, Polynomial.natDegree_X_sub_C, Polynomial.leadingCoeff_comp, Polynomial.leadingCoeff_X_sub_C, Iff.mp, Polynomial.Monic.def, smul_eq_mul, mul_one, one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
hne : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
heq : d = (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree
_ :
  (HSMul.hSMul (α := F) (↑d ! : F)⁻¹
          (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1))).coeff
      (comp (ascPochhammer F d) (HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) (↑k : F)) + 1)).natDegree =
    HSMul.hSMul (α := F) (↑d ! : F)⁻¹
      (comp (ascPochhammer F d)
          (HSub.hSub (α := F[X]) (β := F[X]) X
            ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff
_₁ :
  HSMul.hSMul (α := F) (↑d ! : F)⁻¹
      (comp (ascPochhammer F d)
          (HSub.hSub (α := F[X]) (β := F[X]) X
            ((C : (a : F) → F[X]) (HSub.hSub (α := F) (↑k : F) 1) : F[X]))).leadingCoeff =
    (↑d ! : F)⁻¹
⊢ (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:
calc
  _ = (d ! : F)⁻¹ • ((ascPochhammer F d).comp (X - C ((k : F) - 1))).leadingCoeff := by
    simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]
  _ = (d ! : F)⁻¹ := by
    simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
      (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]

Premises used: Polynomial.C, ascPochhammer, HSub.hSub, Polynomial.leadingCoeff, Nat.cast, Nat.factorial, OfNat.ofNat, Polynomial.X, Polynomial.comp, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k : ℕ
rw : coeff (preHilbertPoly F d k) (natDegree (preHilbertPoly F d k)) = (↑d ! : F)⁻¹
rw₁ : coeff (preHilbertPoly F d k) d = (↑d ! : F)⁻¹
rw₂ rw₃ : Eq.{u_1 + 1} (α := F) (↑d ! : F)⁻¹ (↑d ! : F)⁻¹
⊢ leadingCoeff (preHilbertPoly F d k) = (↑d ! : F)⁻¹

Tactic:
rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_preHilbertPoly, Polynomial.coeff_preHilbertPoly_self
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
norm_cast : ¬d ! = 0
⊢ Ne.{u_1 + 1} (α := F) (↑d ! : F) 0

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ¬d ! = 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ Ne.{u_1 + 1} (α := F) (↑d ! : F) 0

Tactic:
have : (d ! : F) ≠ 0 := by norm_cast; positivity
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ eval (↑n : F) (preHilbertPoly F d k) = (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d)

Tactic:
simp [cast_sub hkn, preHilbertPoly]

Premises used: Nat.cast_sub, Polynomial.preHilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
rw : HMul.hMul (α := F) (↑d ! : F)⁻¹ (↑((n - k + 1).ascFactorial d) : F) = (↑((n - k + d).choose d) : F)
⊢ (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d) = (↑((n - k + d).choose d) : F)

Tactic:
rw [ascPochhammer_nat_eq_natCast_ascFactorial]

Premises used: ascPochhammer_nat_eq_natCast_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
⊢ HMul.hMul (α := F) (↑d ! : F)⁻¹ (↑((n - k + 1).ascFactorial d) : F) = (↑((n - k + d).choose d) : F)

Tactic:
simp [field, ascFactorial_eq_factorial_mul_choose]

Premises used: Nat.ascFactorial_eq_factorial_mul_choose
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
d k n : ℕ
hkn : k ≤ n
this : Ne.{u_1 + 1} (α := F) (↑d ! : F) 0
_ : eval (↑n : F) (preHilbertPoly F d k) = (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d)
_₁ : (↑d ! : F)⁻¹ * eval (↑(n - k + 1) : F) (ascPochhammer F d) = (↑((n - k + d).choose d) : F)
⊢ eval (↑n : F) (preHilbertPoly F d k) = (↑((n - k + d).choose d) : F)

Tactic:
calc
  _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbertPoly]
  _ = (n - k + d).choose d := by
    rw [ascPochhammer_nat_eq_natCast_ascFactorial];
    simp [field, ascFactorial_eq_factorial_mul_choose]

Premises used: Polynomial.eval, Nat.choose, ascPochhammer, HSub.hSub, HAdd.hAdd
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
d : ℕ
delta :
  Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) d with
      | 0 => 0
      | d.succ => ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
      F[X])
    (0 : F[X])
⊢ Eq.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0

Tactic:
delta hilbertPoly

Premises used: Polynomial.hilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
⊢ Eq.{u_1 + 1} (α := F[X])
    (match (motive := ℕ → F[X]) 0 with
      | 0 => 0
      | d.succ => ∑ i ∈ support.{u_1} (R := F) 0, HSMul.hSMul (α := F) (β := F[X]) (coeff 0 i) (preHilbertPoly F d i) :
      F[X])
    (0 : F[X])

Tactic:
simp only