-- Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean
theorem deriv_gaussian_eq_hermite_mul_gaussian (n : ℕ) (x : ℝ) :
    deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1 : ℝ) ^ n * aeval x (hermite n) * Real.exp (-(x ^ 2 / 2))

Proof state:
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))

Tactic:
rw [deriv_exp (by simp)]

Result:
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * deriv (fun y => -(y ^ 2 / 2)) x = -x * Real.exp (-(x ^ 2 / 2))

Proof state:
case succ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv^[n + 1] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Tactic:
rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_mul, pow_succ (-1 : ℝ),
  deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, Polynomial.deriv_aeval]

Result:
case succ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      ((aeval x) (derivative (hermite n)) * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 * ((x * (aeval x) (hermite n) - (aeval x) (derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))

case succ.hc
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => (aeval x) (hermite n)) x

case succ.hd
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => Real.exp (-(x ^ 2 / 2))) x

Proof state:
case zero
x : ℝ
⊢ deriv^[0] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ 0 * ((aeval x) (hermite 0) * Real.exp (-(x ^ 2 / 2)))

Tactic:
rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]

Result:
no goals

Proof state:
case succ.hc
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => (aeval x) (hermite n)) x

Tactic:
apply Polynomial.differentiable_aeval

Result:
no goals

Proof state:
case succ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv^[n + 1] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Tactic:
have deriv_gaussian :
  deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
  rw [deriv_exp (by simp)]; simp; ring

Result:
case succ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv^[n + 1] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Proof state:
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ DifferentiableAt ℝ (fun y => -(y ^ 2 / 2)) x

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * deriv (fun y => -(y ^ 2 / 2)) x = -x * Real.exp (-(x ^ 2 / 2))

Tactic:
simp

Result:
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * x = x * Real.exp (-(x ^ 2 / 2))

Proof state:
case succ
n : ℕ
ih :
  ∀ (x : ℝ),
    deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
x : ℝ
⊢ deriv^[n + 1] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Tactic:
replace ih : deriv^[n] _ = _ := _root_.funext ih

Result:
case succ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv^[n + 1] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Proof state:
case succ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      ((aeval x) (derivative (hermite n)) * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 * ((x * (aeval x) (hermite n) - (aeval x) (derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))

Tactic:
ring

Result:
no goals

Proof state:
case succ.hd
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => Real.exp (-(x ^ 2 / 2))) x

Tactic:
apply DifferentiableAt.exp

Result:
case succ.hd.hc
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => -(x ^ 2 / 2)) x

Proof state:
case succ.hd.hc
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => -(x ^ 2 / 2)) x

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * x = x * Real.exp (-(x ^ 2 / 2))

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))

Tactic:
rw [mul_assoc]

Result:
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))

Proof state:
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))

Tactic:
induction' n with n ih generalizing x

Result:
case zero
x : ℝ
⊢ deriv^[0] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ 0 * ((aeval x) (hermite 0) * Real.exp (-(x ^ 2 / 2)))

case succ
n : ℕ
ih :
  ∀ (x : ℝ),
    deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
x : ℝ
⊢ deriv^[n + 1] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))