awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
h :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + 0).choose 0) : ℤ) =
    -(hermite (2 * n + 1)).coeff 1
⊢ (hermite (2 * (n + 1) + 0)).coeff 0 =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + 0).choose 0) : ℤ)

Tactic:
convert! coeff_hermite_succ_zero (2 * n + 1) using 1

Premises used: HMul.hMul, Polynomial.coeff_hermite_succ_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
h :
  HPow.hPow (α := ℤ) (-1) n * -1 * (↑((2 * n + 1) * (2 * n - 1)‼) : ℤ) * (↑1 : ℤ) =
    -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑(2 * n + 1) : ℤ))
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + 0).choose 0) : ℤ) =
    -(hermite (2 * n + 1)).coeff 1

Tactic:
rw [coeff_hermite_explicit n 1, (by grind : 2 * (n + 1) - 1 = 2 * n + 1),
      Nat.doubleFactorial_add_one, Nat.choose_zero_right,
      Nat.choose_one_right, pow_succ]

Premises used: pow_succ, Nat.choose_one_right, Nat.doubleFactorial_add_one, OfNat.ofNat, Nat.choose_zero_right
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n : ℕ
⊢ HPow.hPow (α := ℤ) (-1) n * -1 * ((HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) * (↑(2 * n - 1)‼ : ℤ)) * 1 =
    -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1))

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
simp :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) -
      HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 *
        (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ))
⊢ hermite_explicit (n + 1) (k + 1) =
    hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)

Tactic:
simp only [hermite_explicit]
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
rw :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
      -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
          HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) -
      HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 *
        (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ))

Tactic:
rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]

Premises used: sub_eq_add_neg, HAdd.hAdd, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
nth_rw :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
      -1 *
        (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
          HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
      -(HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
          HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)

Tactic:
nth_rw 3 [neg_eq_neg_one_mul]

Premises used: neg_eq_neg_one_mul
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
simp :
  -1 *
      (HPow.hPow (α := ℤ) (-1) n *
        HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ)) =
    -1 *
      (HPow.hPow (α := ℤ) (-1) n *
        (HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
          (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)))
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) +
      -1 *
        (HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) *
          HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)

Tactic:
simp only [mul_assoc, ← mul_add, pow_succ']

Premises used: mul_assoc, mul_add, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
      (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)
⊢ -1 *
      (HPow.hPow (α := ℤ) (-1) n *
        HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ)) =
    -1 *
      (HPow.hPow (α := ℤ) (-1) n *
        (HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
          (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)))

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
⊢ HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(2 * (n + 1) - 1)‼ : ℤ) (↑((2 * (n + 1) + k).choose k) : ℤ) +
      (↑(2 * n - 1)‼ : ℤ) * ((↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) * HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ 2 * (n + 1) - 1 = 2 * n + 1

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + k).choose k +
      (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
⊢ (2 * (n + 1) - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * (n + 1) - 1)‼ * (2 * (n + 1) + k).choose k + (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
rw [(by grind : 2 * (n + 1) - 1 = 2 * n + 1),
        Nat.doubleFactorial_add_one, mul_comm (2 * n + 1)]

Premises used: HMul.hMul, HAdd.hAdd, Nat.doubleFactorial_add_one, mul_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1)) =
    (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2))
⊢ (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + k).choose k +
      (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
simp only [mul_assoc, ← mul_add]

Premises used: mul_assoc, mul_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)
⊢ (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1)) =
    (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ 2 * (n + 1) + k = 2 * n + 1 + (k + 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ 2 * n + (k + 2) = 2 * n + 1 + (k + 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)
⊢ (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)

Tactic:
rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1),
        (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
        (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
e_a :
  (2 * n + 1) * ((2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1)) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1) * (2 * n + 1)
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)

Tactic:
rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel]

Premises used: Nat.choose, HMul.hMul, Nat.choose_succ_right_eq, HAdd.hAdd, Nat.add_sub_cancel, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n_1 k_1 : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
n k : ℕ
⊢ (2 * n + 1) * ((2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1)) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1) * (2 * n + 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
⊢ ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)

Tactic:
have hermite_explicit_recur :
      ∀ n k : ℕ,
        hermite_explicit (n + 1) (k + 1) =
          hermite_explicit (n + 1) k - (k + 2) * hermite_explicit n (k + 2) := by
      intro n k
      simp only [hermite_explicit]
      -- Factor out (-1)'s.
      rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
      nth_rw 3 [neg_eq_neg_one_mul]
      simp only [mul_assoc, ← mul_add, pow_succ']
      congr 2
      -- Factor out double factorials.
      norm_cast
      rw [(by grind : 2 * (n + 1) - 1 = 2 * n + 1),
        Nat.doubleFactorial_add_one, mul_comm (2 * n + 1)]
      simp only [mul_assoc, ← mul_add]
      congr 1
      -- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
      rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1),
        (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
        (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
      rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel]
      ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
hermite_explicit_recur :
  ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
change : (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + (k + 1)).choose (k + 1)) : ℤ)

Tactic:
change _ = hermite_explicit _ _
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
hermite_explicit_recur :
  ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
rw :
  (hermite (2 * (n + 1) + k)).coeff k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * (hermite (2 * (n + 1) + k)).coeff (k + 2) =
    hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)

Tactic:
rw [← add_assoc, coeff_hermite_succ_succ, hermite_explicit_recur]

Premises used: Polynomial.coeff_hermite_succ_succ, add_assoc
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
hermite_explicit_recur :
  ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
e_a : (hermite (2 * (n + 1) + k)).coeff k = hermite_explicit (n + 1) k
e_a₁ : (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * (hermite (2 * (n + 1) + k)).coeff (k + 2) =
    hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
hermite_explicit_recur :
  ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
e_a e_a₁ :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) =
    hermite_explicit (n + 1) k
⊢ (hermite (2 * (n + 1) + k)).coeff k = hermite_explicit (n + 1) k

Tactic:
rw [coeff_hermite_explicit (n + 1) k]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
hermite_explicit_recur :
  ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
⊢ 2 * (n + 1) + k = 2 * n + (k + 2)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
hermite_explicit_recur :
  ∀ (n k : ℕ),
    hermite_explicit (n + 1) (k + 1) =
      hermite_explicit (n + 1) k - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2 * hermite_explicit n (k + 2)
rw : 2 * (n + 1) + k = 2 * n + (k + 2)
e_a : (hermite (2 * n + (k + 2))).coeff (k + 2) = hermite_explicit n (k + 2)
e_a₁ e_a₂ :
  HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (k + 2)) : ℤ) =
    hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)

Tactic:
rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : Even (n + k)
inl :
  ∀ (h_le : k ≤ n),
    (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
inr :
  ∀ (h_lt : n < k),
    (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)

Tactic:
rcases le_or_gt k n with h_le | h_lt

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ Even (n - k)

Tactic:
rw [Nat.even_add, ← Nat.even_sub h_le] at hnk

Premises used: Nat.even_add, Nat.even_sub
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
hnk₁ : Even (n - k)
⊢ k ≤ n

Tactic:
rw [Nat.even_add, ← Nat.even_sub h_le] at hnk

Premises used: Nat.even_add, Nat.even_sub
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : Even (n - k)
h_le : k ≤ n
inl :
  ∀ (m : ℕ) (hm : n - k = m + m),
    (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)

Tactic:
obtain ⟨m, hm⟩ := hnk
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ n = 2 * m + k

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
rw : n = 2 * m + k
inl :
  (hermite (2 * m + k)).coeff k =
    HPow.hPow (α := ℤ) (-1) ((2 * m + k - k) / 2) * (↑(2 * m + k - k - 1)‼ : ℤ) * (↑((2 * m + k).choose k) : ℤ)
inl₁ :
  (hermite (2 * m + k)).coeff k =
    HPow.hPow (α := ℤ) (-1) (2 * m / 2) * (↑(2 * m - 1)‼ : ℤ) * (↑((2 * m + k).choose k) : ℤ)
inl₂ : (hermite (2 * m + k)).coeff k = HPow.hPow (α := ℤ) (-1) m * (↑(2 * m - 1)‼ : ℤ) * (↑((2 * m + k).choose k) : ℤ)
inl₃ inl₄ :
  HPow.hPow (α := ℤ) (-1) m * (↑(2 * m - 1)‼ : ℤ) * (↑((2 * m + k).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(2 * m - 1)‼ : ℤ) * (↑((2 * m + k).choose k) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)

Tactic:
rw [(by lia : n = 2 * m + k),
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]

Premises used: Nat.mul_div_cancel_left, Polynomial.coeff_hermite_explicit, Nat.succ_pos, Nat.add_sub_cancel, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)

Tactic:
simp [Nat.choose_eq_zero_of_lt h_lt, coeff_hermite_of_lt h_lt]

Premises used: Nat.choose_eq_zero_of_lt, Polynomial.coeff_hermite_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
pos :
  ∀ (h : Even (n + k)),
    (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
neg : ∀ (h : ¬Even (n + k)), (hermite n).coeff k = 0
⊢ (hermite n).coeff k =
    if Even (n + k) then HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
h : Even (n + k)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)

Tactic:
coeff_hermite_of_even_add h

Premises used: Polynomial.coeff_hermite_of_even_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
h : Even (n + k)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)

Tactic:
exact coeff_hermite_of_even_add h

Premises used: Polynomial.coeff_hermite_of_even_add
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
coeff_hermite_of_odd_add (Nat.not_even_iff_odd.1 h)

Premises used: Nat.not_even_iff_odd, Polynomial.coeff_hermite_of_odd_add, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Basic
Goal:
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
exact coeff_hermite_of_odd_add (Nat.not_even_iff_odd.1 h)

Premises used: Nat.not_even_iff_odd, Polynomial.coeff_hermite_of_odd_add, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
n : ℕ
x : ℝ
rw :
  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)))
⊢ deriv^[n] (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x =
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) *
      Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Goal:
x : ℝ
zero :
  Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
    HPow.hPow (α := ℝ) (β := ℕ) (-1) 0 *
      HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite 0) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
zero₁ :
  Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
    1 * HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite 0) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
zero₂ :
  Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) (hermite 0) : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
zero₃ :
  Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) ((C : (a : ℤ) → ℤ[X]) 1) : ℝ)
      (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
zero₄ :
  Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
    HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) 1 : ℝ) (Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)))
zero₅ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) = 1 * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
zero₆ zero₇ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) = Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
⊢ 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:
rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]

Premises used: Polynomial.C_1, pow_zero, map_one, Polynomial.hermite_zero, Function.iterate_zero_apply, one_mul