awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (hypothesis)
Goal:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ :=
  fun (n k : ℕ) ↦ HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + k).choose k) : ℤ)
⊢ (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)) : ℤ)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)
have 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)
Tactic: rw [← add_assoc, coeff_hermite_succ_succ, hermite_explicit_recur]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ (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)
have e_a : (hermite (2 * (n + 1) + k)).coeff k = hermite_explicit (n + 1) k
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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
⊢ (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)
have e_a₁ : (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ (hermite (2 * (n + 1) + k)).coeff k = hermite_explicit (n + 1) k
have e_a : HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(2 * (n + 1) - 1)‼ : ℤ) * (↑((2 * (n + 1) + k).choose k) : ℤ) =
  hermite_explicit (n + 1) k
Tactic: rw [coeff_hermite_explicit (n + 1) k]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)
have rw : 2 * (n + 1) + k = 2 * n + (k + 2)
Tactic: rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)
have e_a : (hermite (2 * n + (k + 2))).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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)
have e_a₁ : HPow.hPow (α := ℤ) (-1) n * (↑(2 * n - 1)‼ : ℤ) * (↑((2 * n + (k + 2)).choose (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)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
hnk : Even (n + k)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have inl : ∀ (h_le : k ≤ n),
  (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have inr : ∀ (h_lt : n < 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (hypothesis)
Goal:
n k : ℕ
hnk : Even (n + k)
h_le : k ≤ n
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have hnk₁ : Even (n - k)
Tactic: rw [Nat.even_add, ← Nat.even_sub h_le] at hnk
Cleared hypotheses: hnk, h_le
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
hnk : Even (n - k)
h_le : k ≤ n
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have inl : ∀ (m : ℕ) (hm : n - k = m + m),
  (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
Tactic: obtain ⟨m, hm⟩ := hnk
Cleared hypotheses: hnk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have rw : n = 2 * m + 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
rw : n = 2 * m + k
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have 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) : ℤ)
Tactic: rw [(by lia : n = 2 * m + k),
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have inl₁ : (hermite (2 * m + k)).coeff k =
  HPow.hPow (α := ℤ) (-1) (2 * m / 2) * (↑(2 * m - 1)‼ : ℤ) * (↑((2 * m + k).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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have inl₂ : (hermite (2 * m + k)).coeff k = HPow.hPow (α := ℤ) (-1) m * (↑(2 * m - 1)‼ : ℤ) * (↑((2 * m + k).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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
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) : ℤ)
⊢ (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
have 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) : ℤ)
Tactic: rw [(by lia : n = 2 * m + k),
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1), coeff_hermite_explicit]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
⊢ (hermite n).coeff k =
    if Even (n + k) then HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ) else 0
have pos : ∀ (h : Even (n + k)),
  (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Basic (goal)
Goal:
n k : ℕ
pos :
  ∀ (h : Even (n + k)),
    (hermite n).coeff k = HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ)
⊢ (hermite n).coeff k =
    if Even (n + k) then HPow.hPow (α := ℤ) (-1) ((n - k) / 2) * (↑(n - k - 1)‼ : ℤ) * (↑(n.choose k) : ℤ) else 0
have neg : ∀ (h : ¬Even (n + k)), (hermite n).coeff k = 0
Tactic: split_ifs with h
-- 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 =
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) (-1) n) ((aeval x : (a : ℤ[X]) → ℝ) (hermite n) : ℝ) *
      Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
have 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)))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
Goal:
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)))
have 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)))
Tactic: rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
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)))
⊢ 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)))
have zero₁ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
  1 * 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
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)))
⊢ 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)))
have zero₂ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
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)))
⊢ 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)))
have zero₄ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) =
  HMul.hMul (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) 1 : ℝ) (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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
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)))
⊢ 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)))
have zero₅ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) = 1 * 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (goal)
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))
⊢ 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)))
have zero₆ : Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2)) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (hypothesis)
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 : ℝ
⊢ 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 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)))
Tactic: replace ih : deriv^[n] _ = _ := _root_.funext ih
Cleared hypotheses: ih
-- 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 (fun (y : ℝ) ↦ Real.exp (-(HPow.hPow (β := ℕ) y 2 / 2))) x = -x * Real.exp (-(HPow.hPow (β := ℕ) x 2 / 2))
have 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))
Tactic: rw [deriv_exp (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Hermite.Gaussian (hypothesis)
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^[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 deriv_gaussian : 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]