Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.TISE

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction

The time-independent Schrodinger equation

@[expose] public section

Derivatives of the eigenfunctions

              

lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) =
    Complex.ofReal (- 1 / Q.ξ ^2) • Complex.ofReal * Q.eigenfunction 0 := byQ:HarmonicOscillator⊢ deriv (Q.eigenfunction 0) = ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0
  rw [eigenfunction_zeroQ:HarmonicOscillator⊢ (deriv fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillator⊢ (deriv fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))]Q:HarmonicOscillator⊢ (deriv fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))
  simp only [deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_neg, Algebra.smul_mul_assoc]Q:HarmonicOscillator⊢ (fun x => 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x) =
  (-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))
  ext xQ:HarmonicOscillatorx:ℝ⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
  have h1 : deriv (fun (x : ℝ) => Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2))) x =
      - x /Q.ξ^2 * Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2)) := byQ:HarmonicOscillator⊢ deriv (Q.eigenfunction 0) = ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
    rw [show (fun (x : ℝ) => Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2)))
          = Complex.exp ∘ (fun (x : ℝ) => - x ^ 2 / (2 * Q.ξ ^ 2)) from rfl,Q:HarmonicOscillatorx:ℝ⊢ deriv (Complex.exp ∘ fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝ⊢ deriv Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * deriv (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
      deriv_comp _ (byQ:HarmonicOscillatorx:ℝ⊢ DifferentiableAt ℂ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝ⊢ deriv Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * deriv (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x fun_propAll goals completed! 🐙Q:HarmonicOscillatorx:ℝ⊢ deriv Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * deriv (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x) (byQ:HarmonicOscillatorx:ℝ⊢ DifferentiableAt ℝ (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) xQ:HarmonicOscillatorx:ℝ⊢ deriv Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * deriv (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x fun_propAll goals completed! 🐙Q:HarmonicOscillatorx:ℝ⊢ deriv Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * deriv (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x)]Q:HarmonicOscillatorx:ℝ⊢ deriv Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * deriv (fun x => -↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) x =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
    simp only [Complex.deriv_exp, deriv_div_const, deriv.fun_neg']Q:HarmonicOscillatorx:ℝ⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
    have h1' : deriv (fun x => (Complex.ofReal x) ^ 2) x = 2 * x := byQ:HarmonicOscillator⊢ deriv (Q.eigenfunction 0) = ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0Q:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
      simp only [pow_two]Q:HarmonicOscillatorx:ℝ⊢ deriv (fun x => ↑x * ↑x) x = 2 * ↑xQ:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
      rw [deriv_fun_mul Complex.differentiableAt_ofReal Complex.differentiableAt_ofRealQ:HarmonicOscillatorx:ℝ⊢ deriv Complex.ofReal x * ↑x + ↑x * deriv Complex.ofReal x = 2 * ↑xQ:HarmonicOscillatorx:ℝ⊢ deriv Complex.ofReal x * ↑x + ↑x * deriv Complex.ofReal x = 2 * ↑xQ:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x]Q:HarmonicOscillatorx:ℝ⊢ deriv Complex.ofReal x * ↑x + ↑x * deriv Complex.ofReal x = 2 * ↑xQ:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
      simp only [Complex.deriv_ofReal, one_mul, mul_one]Q:HarmonicOscillatorx:ℝ⊢ ↑x + ↑x = 2 * ↑xQ:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
      ringQ:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) xQ:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-deriv (fun i => ↑i ^ 2) x / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
    rw [h1'Q:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-(2 * ↑x) / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-(2 * ↑x) / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x]Q:HarmonicOscillatorx:ℝh1':deriv (fun x => ↑x ^ 2) x = 2 * ↑x⊢ Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)) * (-(2 * ↑x) / (2 * ↑Q.ξ ^ 2)) =
  -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
    field_simpQ:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) xQ:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * fun x => 1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2)))) x
  simp only [Pi.smul_apply, Pi.mul_apply, smul_eq_mul]Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x =
  -↑1 / ↑(Q.ξ ^ 2) * (↑x * (1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))))
  rw [h1Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * (-↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  -↑1 / ↑(Q.ξ ^ 2) * (↑x * (1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))))Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * (-↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  -↑1 / ↑(Q.ξ ^ 2) * (↑x * (1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))))]Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ 1 / ↑√(√Real.pi * Q.ξ) * (-↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  -↑1 / ↑(Q.ξ ^ 2) * (↑x * (1 / ↑√(√Real.pi * Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))))
  simp only [Real.sqrt_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
    Complex.ofReal_one, Complex.ofReal_pow]Q:HarmonicOscillatorx:ℝh1:deriv (fun x => Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) x = -↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))⊢ (↑√Q.ξ)⁻¹ * (↑√√Real.pi)⁻¹ * (-↑x / ↑Q.ξ ^ 2 * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  -1 / ↑Q.ξ ^ 2 * (↑x * ((↑√Q.ξ)⁻¹ * (↑√√Real.pi)⁻¹ * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))))
  ringAll goals completed! 🐙

lemma deriv_eigenfunction_zero' : deriv (Q.eigenfunction 0) =
    (- √2 / (2 * Q.ξ) : ℂ) • Q.eigenfunction 1 := byQ:HarmonicOscillator⊢ deriv (Q.eigenfunction 0) = (-↑√2 / (2 * ↑Q.ξ)) • Q.eigenfunction 1
  rw [deriv_eigenfunction_zeroQ:HarmonicOscillator⊢ ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0 = (-↑√2 / (2 * ↑Q.ξ)) • Q.eigenfunction 1Q:HarmonicOscillator⊢ ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0 = (-↑√2 / (2 * ↑Q.ξ)) • Q.eigenfunction 1]Q:HarmonicOscillator⊢ ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0 = (-↑√2 / (2 * ↑Q.ξ)) • Q.eigenfunction 1
  funext xQ:HarmonicOscillatorx:ℝ⊢ (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x = ((-↑√2 / (2 * ↑Q.ξ)) • Q.eigenfunction 1) x
  simp [eigenfunction_eq, physHermite_zero, physHermite_one, map_ofNat]Q:HarmonicOscillatorx:ℝ⊢ -1 / ↑Q.ξ ^ 2 * ↑x * ((↑√Q.ξ)⁻¹ * (↑√√Real.pi)⁻¹ * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))) =
  -↑√2 / (2 * ↑Q.ξ) *
    ((↑√2)⁻¹ * ((↑√Q.ξ)⁻¹ * (↑√√Real.pi)⁻¹) * (2 * (↑x / ↑Q.ξ) * Complex.exp (-↑x ^ 2 / (2 * ↑Q.ξ ^ 2))))
  ring_nfQ:HarmonicOscillatorx:ℝ⊢ -((↑Q.ξ)⁻¹ ^ 2 * ↑x * (↑√Q.ξ)⁻¹ * (↑√√Real.pi)⁻¹ * Complex.exp ((↑Q.ξ)⁻¹ ^ 2 * ↑x ^ 2 * (-1 / 2))) =
  -((↑Q.ξ)⁻¹ ^ 2 * ↑x * (↑√Q.ξ)⁻¹ * (↑√√Real.pi)⁻¹ * Complex.exp ((↑Q.ξ)⁻¹ ^ 2 * ↑x ^ 2 * (-1 / 2)) * ↑√2 * (↑√2)⁻¹)
  simpAll goals completed! 🐙

lemma deriv_physHermite_characteristic_length (n : ℕ) :
    deriv (fun x => Complex.ofReal (physHermite n (x/Q.ξ))) = fun x =>
    Complex.ofReal (1/Q.ξ) * 2 * n * physHermite (n-1) (x/Q.ξ) := byQ:HarmonicOscillatorn:ℕ⊢ (deriv fun x => ↑(↑(physHermite n) (x / Q.ξ))) = fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))
  change deriv (fun x ↦ Complex.ofReal ((physHermite n ∘ fun x ↦ x / Q.ξ) x)) = _Q:HarmonicOscillatorn:ℕ⊢ (deriv fun x => ↑((↑(physHermite n) ∘ fun x => x / Q.ξ) x)) = fun x =>
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))
  funext xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑((↑(physHermite n) ∘ fun x => x / Q.ξ) x)) x =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))
  have hd : DifferentiableAt ℝ (physHermite n ∘ fun x ↦ x / Q.ξ) x := byQ:HarmonicOscillatorn:ℕ⊢ (deriv fun x => ↑(↑(physHermite n) (x / Q.ξ))) = fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ deriv (fun x => ↑((↑(physHermite n) ∘ fun x => x / Q.ξ) x)) x =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)) fun_propQ:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ deriv (fun x => ↑((↑(physHermite n) ∘ fun x => x / Q.ξ) x)) x =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ deriv (fun x => ↑((↑(physHermite n) ∘ fun x => x / Q.ξ) x)) x =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))
  rw [(hd.hasDerivAt.ofReal_comp).deriv,Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n) ∘ fun x => x / Q.ξ) x) = ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n)) (x / Q.ξ) * deriv (fun x => x / Q.ξ) x) =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)) deriv_comp _ (byQ:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ DifferentiableAt ℝ (↑(physHermite n)) (x / Q.ξ)Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n)) (x / Q.ξ) * deriv (fun x => x / Q.ξ) x) =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n)) (x / Q.ξ) * deriv (fun x => x / Q.ξ) x) =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) (byQ:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ DifferentiableAt ℝ (fun x => x / Q.ξ) xQ:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n)) (x / Q.ξ) * deriv (fun x => x / Q.ξ) x) =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n)) (x / Q.ξ) * deriv (fun x => x / Q.ξ) x) =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)))]Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ ↑(deriv (↑(physHermite n)) (x / Q.ξ) * deriv (fun x => x / Q.ξ) x) =
  ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))
  simp only [deriv_physHermite, Pi.mul_apply, Pi.ofNat_apply, Pi.natCast_apply, deriv_div_const,
    deriv_id'', Complex.ofReal_mul, Complex.ofReal_ofNat, Complex.ofReal_natCast]Q:HarmonicOscillatorn:ℕx:ℝhd:DifferentiableAt ℝ (↑(physHermite n) ∘ fun x => x / Q.ξ) x⊢ 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)) * ↑(1 / Q.ξ) = ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))
  ringAll goals completed! 🐙

lemma deriv_eigenfunction_succ (n : ℕ) :
    deriv (Q.eigenfunction (n + 1)) = fun x =>
    Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1)!) * (1/Q.ξ)) •
    ((2 * (n + 1) * physHermite n (x/Q.ξ)
      - (x/Q.ξ) * physHermite (n + 1) (x/Q.ξ)) * Q.eigenfunction 0 x) := byQ:HarmonicOscillatorn:ℕ⊢ deriv (Q.eigenfunction (n + 1)) = fun x =>
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  funext xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (Q.eigenfunction (n + 1)) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  rw [eigenfunction_eq_mul_eigenfunction_zeroQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  rw [deriv_fun_mul (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x * Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x * Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)) (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (Q.eigenfunction 0) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x * Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x * Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x * Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  rw [deriv_fun_mul (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ (deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!))) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) *
      Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ (deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!))) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) *
      Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)) (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ (deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!))) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) *
      Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ (deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!))) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) *
      Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (deriv (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!))) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) *
      Q.eigenfunction 0 x +
    ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, one_div, mul_inv_rev, Complex.ofReal_mul,
    Complex.ofReal_inv, deriv_const', zero_mul, zero_add, smul_eq_mul]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x * Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  rw [deriv_physHermite_characteristic_length,Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ *
        (fun x => ↑(1 / Q.ξ) * 2 * ↑(n + 1) * ↑(↑(physHermite (n + 1 - 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * deriv (Q.eigenfunction 0) x =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ *
        (fun x => ↑(1 / Q.ξ) * 2 * ↑(n + 1) * ↑(↑(physHermite (n + 1 - 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) deriv_eigenfunction_zeroQ:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ *
        (fun x => ↑(1 / Q.ξ) * 2 * ↑(n + 1) * ↑(↑(physHermite (n + 1 - 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ *
        (fun x => ↑(1 / Q.ξ) * 2 * ↑(n + 1) * ↑(↑(physHermite (n + 1 - 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ *
        (fun x => ↑(1 / Q.ξ) * 2 * ↑(n + 1) * ↑(↑(physHermite (n + 1 - 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  simp only [one_div, Complex.ofReal_inv, cast_add, cast_one, add_tsub_cancel_right,
    Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_pow, Pi.mul_apply,
    Pi.smul_apply, smul_eq_mul]Q:HarmonicOscillatorn:ℕx:ℝ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ((↑Q.ξ)⁻¹ * 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) *
      Q.eigenfunction 0 x +
    (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      (-1 / ↑Q.ξ ^ 2 * ↑x * Q.eigenfunction 0 x) =
  (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * (↑Q.ξ)⁻¹ *
    ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  ringAll goals completed! 🐙

Second derivatives of the eigenfunctions.

              

lemma deriv_deriv_eigenfunction_zero (x : ℝ) : deriv (deriv (Q.eigenfunction 0)) x =
    (- 1 / Q.ξ^2) * (1 + ((- 1/ Q.ξ^2) * x ^ 2)) * Q.eigenfunction 0 x := byQ:HarmonicOscillatorx:ℝ⊢ deriv (deriv (Q.eigenfunction 0)) x = -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  simp only [deriv_eigenfunction_zero, Complex.ofReal_div, Complex.ofReal_neg,
    Algebra.smul_mul_assoc]Q:HarmonicOscillatorx:ℝ⊢ deriv ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * Q.eigenfunction 0)) x =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  trans deriv (fun x => (- (1/Q.ξ^2)) • (Complex.ofReal x * Q.eigenfunction 0 x)) xQ:HarmonicOscillatorx:ℝ⊢ deriv ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * Q.eigenfunction 0)) x =
  deriv (fun x => -(1 / Q.ξ ^ 2) • (↑x * Q.eigenfunction 0 x)) xQ:HarmonicOscillatorx:ℝ⊢ deriv (fun x => -(1 / Q.ξ ^ 2) • (↑x * Q.eigenfunction 0 x)) x =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  ·Q:HarmonicOscillatorx:ℝ⊢ deriv ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * Q.eigenfunction 0)) x =
  deriv (fun x => -(1 / Q.ξ ^ 2) • (↑x * Q.eigenfunction 0 x)) x congre_fQ:HarmonicOscillatorx:ℝ⊢ (-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * Q.eigenfunction 0) = fun x => -(1 / Q.ξ ^ 2) • (↑x * Q.eigenfunction 0 x)
    funext xe_fQ:HarmonicOscillatorx✝:ℝx:ℝ⊢ ((-↑1 / ↑(Q.ξ ^ 2)) • (Complex.ofReal * Q.eigenfunction 0)) x = -(1 / Q.ξ ^ 2) • (↑x * Q.eigenfunction 0 x)
    simp only [Complex.ofReal_one, Complex.ofReal_pow, Pi.smul_apply, Pi.mul_apply, smul_eq_mul,
      one_div, neg_smul, Complex.real_smul, Complex.ofReal_inv]e_fQ:HarmonicOscillatorx✝:ℝx:ℝ⊢ -1 / ↑Q.ξ ^ 2 * (↑x * Q.eigenfunction 0 x) = -((↑Q.ξ ^ 2)⁻¹ * (↑x * Q.eigenfunction 0 x))
    ringAll goals completed! 🐙
  simp only [Complex.real_smul, Complex.ofReal_neg, Complex.ofReal_div, deriv_const_mul_field']Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * deriv (fun x => ↑x * Q.eigenfunction 0 x) x =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  rw [deriv_fun_mul (byQ:HarmonicOscillatorx:ℝ⊢ DifferentiableAt ℝ Complex.ofReal xQ:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (deriv Complex.ofReal x * Q.eigenfunction 0 x + ↑x * deriv (Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x fun_propAll goals completed! 🐙Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (deriv Complex.ofReal x * Q.eigenfunction 0 x + ↑x * deriv (Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x) (byQ:HarmonicOscillatorx:ℝ⊢ DifferentiableAt ℝ (Q.eigenfunction 0) xQ:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (deriv Complex.ofReal x * Q.eigenfunction 0 x + ↑x * deriv (Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x fun_propAll goals completed! 🐙Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (deriv Complex.ofReal x * Q.eigenfunction 0 x + ↑x * deriv (Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x)]Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (deriv Complex.ofReal x * Q.eigenfunction 0 x + ↑x * deriv (Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  simp only [Complex.deriv_ofReal]Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (1 * Q.eigenfunction 0 x + ↑x * deriv (Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  rw [deriv_eigenfunction_zeroQ:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (1 * Q.eigenfunction 0 x + ↑x * (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 xQ:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (1 * Q.eigenfunction 0 x + ↑x * (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x]Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2)) * (1 * Q.eigenfunction 0 x + ↑x * (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  simp only [Complex.ofReal_div, Complex.ofReal_neg, Pi.mul_apply, Pi.smul_apply, smul_eq_mul,
    neg_mul]Q:HarmonicOscillatorx:ℝ⊢ -(↑1 / ↑(Q.ξ ^ 2) * (1 * Q.eigenfunction 0 x + ↑x * (-↑1 / ↑(Q.ξ ^ 2) * ↑x * Q.eigenfunction 0 x))) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  push_castQ:HarmonicOscillatorx:ℝ⊢ -(1 / ↑Q.ξ ^ 2 * (1 * Q.eigenfunction 0 x + ↑x * (-1 / ↑Q.ξ ^ 2 * ↑x * Q.eigenfunction 0 x))) =
  -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x
  ringAll goals completed! 🐙

lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) :
    deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
    Complex.ofReal (1/√(2 ^ (n + 1) * (n + 1) !) * (1/Q.ξ)) *
      ((2 * (↑n + 1) * deriv (fun x => ↑(physHermite n (x/Q.ξ))) x +
      (-(1/Q.ξ^2)) * (4 * (↑n + 1) * x) *
      (physHermite n (x/Q.ξ)) + (- (1/Q.ξ)) * (1 + (- (1/Q.ξ^2)) * x ^ 2) *
      (physHermite (n + 1) (x/Q.ξ))) * Q.eigenfunction 0 x) := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  rw [deriv_eigenfunction_succQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv
    (fun x =>
      (fun x =>
          ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
            ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
              Q.eigenfunction 0 x))
        x)
    x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv
    (fun x =>
      (fun x =>
          ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
            ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
              Q.eigenfunction 0 x))
        x)
    x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv
    (fun x =>
      (fun x =>
          ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) •
            ((2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
              Q.eigenfunction 0 x))
        x)
    x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x)
  simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, one_div, mul_inv_rev, Complex.ofReal_mul,
    Complex.ofReal_inv, smul_eq_mul, deriv_const_mul_field', neg_mul, mul_eq_mul_left_iff,
    _root_.mul_eq_zero, inv_eq_zero, Complex.ofReal_eq_zero, cast_nonneg, Real.sqrt_eq_zero,
    cast_eq_zero, ne_eq, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true,
    pow_eq_zero_iff, OfNat.ofNat_ne_zero, or_false, ξ_ne_zero]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv
      (fun x =>
        (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
          Q.eigenfunction 0 x)
      x =
    (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
        -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
      Q.eigenfunction 0 x ∨
  (n + 1)! = 0
  leftQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv
    (fun x =>
      (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        Q.eigenfunction 0 x)
    x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x
  rw [deriv_fun_mul (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ
  (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      deriv (Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      deriv (Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x) (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (Q.eigenfunction 0) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      deriv (Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      deriv (Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x)]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      deriv (Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x
  rw [deriv_eigenfunction_zeroQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x *
      Q.eigenfunction 0 x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      (↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0) x =
  (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) *
    Q.eigenfunction 0 x
  simp only [Complex.ofReal_div, Complex.ofReal_neg, Pi.mul_apply, Pi.smul_apply, smul_eq_mul, ←
    mul_assoc, ← add_mul, mul_eq_mul_right_iff]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
      (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
          (-↑1 / ↑(Q.ξ ^ 2)) *
        ↑x =
    2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
      -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) ∨
  Q.eigenfunction 0 x = 0
  leftQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  rw [deriv_fun_sub (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  rw [deriv_fun_mul (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => 2 * (↑n + 1)) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1)) x * ↑(↑(physHermite n) (x / Q.ξ)) +
        2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1)) x * ↑(↑(physHermite n) (x / Q.ξ)) +
        2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑(↑(physHermite n) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1)) x * ↑(↑(physHermite n) (x / Q.ξ)) +
        2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1)) x * ↑(↑(physHermite n) (x / Q.ξ)) +
        2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => 2 * (↑n + 1)) x * ↑(↑(physHermite n) (x / Q.ξ)) +
        2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  simp only [deriv_const', zero_mul, zero_add]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      deriv (fun x => ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  rw [deriv_fun_mul (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑x / ↑Q.ξ) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      (deriv (fun x => ↑x / ↑Q.ξ) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      (deriv (fun x => ↑x / ↑Q.ξ) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))) (byQ:HarmonicOscillatorn:ℕx:ℝ⊢ DifferentiableAt ℝ (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) xQ:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      (deriv (fun x => ↑x / ↑Q.ξ) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) fun_propAll goals completed! 🐙Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      (deriv (fun x => ↑x / ↑Q.ξ) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))))]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      (deriv (fun x => ↑x / ↑Q.ξ) x * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        (-↑1 / ↑(Q.ξ ^ 2)) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  simp only [deriv_div_const, Complex.deriv_ofReal, one_div, Complex.ofReal_one, Complex.ofReal_pow]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      ((↑Q.ξ)⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * deriv (fun x => ↑(↑(physHermite (n + 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) * (-1 / ↑Q.ξ ^ 2) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  nth_rewrite 2 [deriv_physHermite_characteristic_length]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      ((↑Q.ξ)⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * (fun x => ↑(1 / Q.ξ) * 2 * ↑(n + 1) * ↑(↑(physHermite (n + 1 - 1)) (x / Q.ξ))) x) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) * (-1 / ↑Q.ξ ^ 2) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  simp only [one_div, Complex.ofReal_inv, cast_add, cast_one, add_tsub_cancel_right]Q:HarmonicOscillatorn:ℕx:ℝ⊢ 2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x -
      ((↑Q.ξ)⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) +
        ↑x / ↑Q.ξ * ((↑Q.ξ)⁻¹ * 2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)))) +
    (2 * (↑n + 1) * ↑(↑(physHermite n) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) * (-1 / ↑Q.ξ ^ 2) *
      ↑x =
  2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
      -((↑Q.ξ ^ 2)⁻¹ * 4 * (↑n + 1) * ↑x * ↑(↑(physHermite n) (x / Q.ξ))) +
    -((↑Q.ξ)⁻¹ * (1 + -((↑Q.ξ ^ 2)⁻¹ * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)))
  ringAll goals completed! 🐙

lemma deriv_deriv_eigenfunction (n : ℕ) (x : ℝ) :
    deriv (fun x => deriv (Q.eigenfunction n) x) x = (- 1 / Q.ξ^2) * ((2 * n + 1)
    + ((- 1/ Q.ξ^2) * x ^ 2)) * Q.eigenfunction n x := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => deriv (Q.eigenfunction n) x) x =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x
  match n with
  | 0 =>Q:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => deriv (Q.eigenfunction 0) x) x =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑0 + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x simpa using Q.deriv_deriv_eigenfunction_zero xAll goals completed! 🐙
  | n + 1 =>Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑(n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction (n + 1) x
    trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !)) *
        (((- 1 / Q.ξ ^ 2) * (2 * (n + 1)
        + (1 + (- 1/ Q.ξ ^ 2) * x ^ 2)) *
        (physHermite (n + 1) (x/Q.ξ))) * Q.eigenfunction 0 x)Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑(n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction (n + 1) x
    ·Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) rw [deriv_deriv_eigenfunction_succQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)]Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!) * (1 / Q.ξ)) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)
      rw [Complex.ofReal_mul,Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(1 / Q.ξ) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (↑(1 / Q.ξ) *
      ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
            -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
          -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        Q.eigenfunction 0 x)) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) mul_assocQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (↑(1 / Q.ξ) *
      ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
            -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
          -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        Q.eigenfunction 0 x)) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (↑(1 / Q.ξ) *
      ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
            -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
          -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        Q.eigenfunction 0 x)) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)]Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (↑(1 / Q.ξ) *
      ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
            -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
          -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
        Q.eigenfunction 0 x)) =
  ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x)
      congr 1e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
    ((2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
    Q.eigenfunction 0 x
      rw [← mul_assoce_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
      (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
    Q.eigenfunction 0 x =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
    Q.eigenfunction 0 xe_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
      (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
    Q.eigenfunction 0 x =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
    Q.eigenfunction 0 x]e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
      (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
          -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
        -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) *
    Q.eigenfunction 0 x =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
    Q.eigenfunction 0 x
      congr 1e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * deriv (fun x => ↑(↑(physHermite n) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))
      rw [deriv_physHermite_characteristic_lengthe_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))]e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))
      have hr : (physHermite (n + 1) (x / Q.ξ) : ℝ) =
          2 * (x / Q.ξ) * physHermite n (x / Q.ξ) - 2 * n * physHermite (n - 1) (x / Q.ξ) := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ deriv (fun x => deriv (Q.eigenfunction n) x) x =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n xe_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))
        rw [physHermite_succ_apply'Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ 2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))]e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ))
      rw [hre_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) *
        ↑(2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) *
    ↑(2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ))e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) *
        ↑(2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) *
    ↑(2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ))]e_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ ↑(1 / Q.ξ) *
    (2 * (↑n + 1) * (fun x => ↑(1 / Q.ξ) * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) x +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) *
        ↑(2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) *
    ↑(2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ))
      push_caste_a.e_aQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕhr:↑(physHermite (n + 1)) (x / Q.ξ) =
  2 * (x / Q.ξ) * ↑(physHermite n) (x / Q.ξ) - 2 * ↑n * ↑(physHermite (n - 1)) (x / Q.ξ)⊢ 1 / ↑Q.ξ *
    (2 * (↑n + 1) * (1 / ↑Q.ξ * 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ))) +
        -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑(↑(physHermite n) (x / Q.ξ)) +
      -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) *
        (2 * (↑x / ↑Q.ξ) * ↑(↑(physHermite n) (x / Q.ξ)) - 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)))) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) *
    (2 * (↑x / ↑Q.ξ) * ↑(↑(physHermite n) (x / Q.ξ)) - 2 * ↑n * ↑(↑(physHermite (n - 1)) (x / Q.ξ)))
      ringAll goals completed! 🐙
    ·Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑(n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction (n + 1) x rw [Q.eigenfunction_eq_mul_eigenfunction_zero (n + 1)Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑(n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) *
    (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x) xQ:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑(n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) *
    (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x) x]Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * ↑(n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) *
    (fun x => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1)!)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x) x
      simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, one_div, mul_inv_rev, Complex.ofReal_mul,
        Complex.ofReal_inv, cast_add, cast_one]Q:HarmonicOscillatorn✝:ℕx:ℝn:ℕ⊢ (↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ *
    (-1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2)) * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) *
      Q.eigenfunction 0 x) =
  -1 / ↑Q.ξ ^ 2 * (2 * (↑n + 1) + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) *
    ((↑√↑(n + 1)!)⁻¹ * (↑√(2 ^ (n + 1)))⁻¹ * ↑(↑(physHermite (n + 1)) (x / Q.ξ)) * Q.eigenfunction 0 x)
      ringAll goals completed! 🐙

Application of the schrodingerOperator

The nth eigenfunction satisfies the time-independent Schrodinger equation with respect to the nth eigenvalue. That is to say for Q a harmonic oscillator,

Q.schrodingerOperator (Q.eigenfunction n) x = Q.eigenValue n * Q.eigenfunction n x.

The proof of this result is done by explicit calculation of derivatives.


lemma schrodingerOperator_eigenfunction (n : ℕ) (x : ℝ) :
    Q.schrodingerOperator (Q.eigenfunction n) x = Q.eigenValue n * Q.eigenfunction n x := byQ:HarmonicOscillatorn:ℕx:ℝ⊢ Q.schrodingerOperator (Q.eigenfunction n) x = ↑(Q.eigenValue n) * Q.eigenfunction n x
  simp only [schrodingerOperator_eq_ξ, one_div]Q:HarmonicOscillatorn:ℕx:ℝ⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) * (-deriv (deriv (Q.eigenfunction n)) x + (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑(Q.eigenValue n) * Q.eigenfunction n x
  rw [Q.deriv_deriv_eigenfunctionQ:HarmonicOscillatorn:ℕx:ℝ⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑(Q.eigenValue n) * Q.eigenfunction n xQ:HarmonicOscillatorn:ℕx:ℝ⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑(Q.eigenValue n) * Q.eigenfunction n x]Q:HarmonicOscillatorn:ℕx:ℝ⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑(Q.eigenValue n) * Q.eigenfunction n x
  have hm' := Complex.ofReal_ne_zero.mpr (Ne.symm (_root_.ne_of_lt Q.hm))Q:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑(Q.eigenValue n) * Q.eigenfunction n x
  have hℏ' := Complex.ofReal_ne_zero.mpr ℏ_ne_zeroQ:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑(Q.eigenValue n) * Q.eigenfunction n x
  rw [eigenValueQ:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑((↑n + 1 / 2) * ↑ℏ * Q.ω) * Q.eigenfunction n xQ:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑((↑n + 1 / 2) * ↑ℏ * Q.ω) * Q.eigenfunction n x]Q:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.ξ ^ 2)⁻¹ ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  ↑((↑n + 1 / 2) * ↑ℏ * Q.ω) * Q.eigenfunction n x
  simp only [← Complex.ofReal_pow, ξ_sq]Q:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ ↑(↑ℏ ^ 2) / (2 * ↑Q.m) *
    (-(-1 / ↑(↑ℏ / (Q.m * Q.ω)) * (2 * ↑n + 1 + -1 / ↑(↑ℏ / (Q.m * Q.ω)) * ↑(x ^ 2)) * Q.eigenfunction n x) +
      (↑(↑ℏ / (Q.m * Q.ω)))⁻¹ ^ 2 * ↑(x ^ 2) * Q.eigenfunction n x) =
  ↑((↑n + 1 / 2) * ↑ℏ * Q.ω) * Q.eigenfunction n x
  simp only [Complex.ofReal_pow, Complex.ofReal_div, Complex.ofReal_mul, inv_div, one_div,
    Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_inv, Complex.ofReal_ofNat]Q:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ ↑↑ℏ ^ 2 / (2 * ↑Q.m) *
    (-(-1 / (↑↑ℏ / (↑Q.m * ↑Q.ω)) * (2 * ↑n + 1 + -1 / (↑↑ℏ / (↑Q.m * ↑Q.ω)) * ↑x ^ 2) * Q.eigenfunction n x) +
      (↑Q.m * ↑Q.ω / ↑↑ℏ) ^ 2 * ↑x ^ 2 * Q.eigenfunction n x) =
  (↑n + 2⁻¹) * ↑↑ℏ * ↑Q.ω * Q.eigenfunction n x
  field_simpQ:HarmonicOscillatorn:ℕx:ℝhm':↑Q.m ≠ 0hℏ':↑↑ℏ ≠ 0⊢ Q.eigenfunction n x * (↑↑ℏ * (2 * ↑n + 1) + -(↑Q.m * ↑Q.ω * ↑x ^ 2) + ↑Q.m * ↑Q.ω * ↑x ^ 2) =
  ↑↑ℏ * (2 * ↑n + 1) * Q.eigenfunction n x
  ringAll goals completed! 🐙