diff --git a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean
index e427644e..6a613a1c 100644
--- a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean
+++ b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean
@@ -22,6 +22,7 @@ namespace PhysLean
 
   `physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n)`.
 
+  This polynomial will often be cast as a function `ℝ → ℝ` by evaluating the polynomial at `X`.
 -/
 noncomputable def physHermite : ℕ → Polynomial ℤ
   | 0 => 1
@@ -96,8 +97,8 @@ lemma coeff_physHermite_self_succ (n : ℕ) : coeff (physHermite n) n = 2 ^ n :=
   | zero => exact coeff_C
   | succ n ih =>
     rw [coeff_physHermite_succ_succ, ih, coeff_physHermite_of_lt, mul_zero, sub_zero]
-    rw [← Int.pow_succ']
-    omega
+    · rw [← Int.pow_succ']
+    · omega
 
 @[simp]
 lemma degree_physHermite (n : ℕ) : degree (physHermite n) = n := by
@@ -144,81 +145,78 @@ lemma physHermite_ne_zero {n : ℕ} : physHermite n ≠ 0 := by
   refine leadingCoeff_ne_zero.mp ?_
   simp
 
-/-- The function `physHermiteFun` from `ℝ` to `ℝ` is defined by evaulation of
- `physHermite` in `ℝ`. -/
-noncomputable def physHermiteFun (n : ℕ) : ℝ → ℝ := fun x => aeval x (physHermite n)
+instance : CoeFun (Polynomial ℤ) (fun _ ↦ ℝ → ℝ)where
+  coe p := fun x => p.aeval x
 
-@[simp]
-lemma physHermiteFun_zero_apply (x : ℝ) : physHermiteFun 0 x = 1 := by
-  simp [physHermiteFun, aeval]
-
-lemma physHermiteFun_pow (n m : ℕ) (x : ℝ) :
-    physHermiteFun n x ^ m = aeval x (physHermite n ^ m) := by
-  simp [physHermiteFun]
+lemma physHermite_zero_apply (x : ℝ) : physHermite 0 x = 1 := by
+  simp [aeval]
 
-lemma physHermiteFun_eq_aeval_physHermite (n : ℕ) :
-    physHermiteFun n = fun x => aeval x (physHermite n) := rfl
+lemma physHermite_pow (n m : ℕ) (x : ℝ) :
+    physHermite n x ^ m = aeval x (physHermite n ^ m) := by
+  simp
 
-lemma physHermiteFun_succ_fun (n : ℕ) :
-    physHermiteFun (n + 1) = 2 • (fun x => x) *
-    physHermiteFun n - (2 * n : ℝ) • physHermiteFun (n - 1) := by
+lemma physHermite_succ_fun (n : ℕ) :
+    (physHermite (n + 1) : ℝ → ℝ) = 2 • (fun x => x) *
+    (physHermite n : ℝ → ℝ)- (2 * n : ℝ) • (physHermite (n - 1) : ℝ → ℝ) := by
   ext x
-  simp [physHermite_succ', aeval, physHermiteFun, mul_assoc]
+  simp [physHermite_succ', aeval, mul_assoc]
 
-lemma physHermiteFun_succ (n : ℕ) :
-    physHermiteFun (n + 1) = fun x => 2 • x *
-    physHermiteFun n x -
-    (2 * n : ℝ) • physHermiteFun (n - 1) x := by
+lemma physHermite_succ_fun' (n : ℕ) :
+    (physHermite (n + 1) : ℝ → ℝ) = fun x => 2 • x *
+    physHermite n x -
+    (2 * n : ℝ) • physHermite (n - 1) x := by
   ext x
-  simp [physHermite_succ', aeval, mul_assoc, physHermiteFun]
+  simp [physHermite_succ', aeval, mul_assoc]
 
-lemma iterated_deriv_physHermiteFun_eq_aeval (n : ℕ) : (m : ℕ) →
-    deriv^[m] (physHermiteFun n) = fun x => (derivative^[m] (physHermite n)).aeval x
+lemma iterated_deriv_physHermite_eq_aeval (n : ℕ) : (m : ℕ) →
+    deriv^[m] (physHermite n) = fun x => (derivative^[m] (physHermite n)).aeval x
   | 0 => by
-    simp [physHermiteFun_eq_aeval_physHermite]
+    simp
   | m + 1 => by
     simp only [Function.iterate_succ_apply', Function.comp_apply]
-    rw [iterated_deriv_physHermiteFun_eq_aeval n m]
+    rw [iterated_deriv_physHermite_eq_aeval n m]
     funext x
     rw [Polynomial.deriv_aeval]
 
 @[fun_prop]
-lemma physHermiteFun_differentiableAt (n : ℕ) (x : ℝ) :
-    DifferentiableAt ℝ (physHermiteFun n) x := Polynomial.differentiableAt_aeval (physHermite n)
+lemma physHermite_differentiableAt (n : ℕ) (x : ℝ) :
+    DifferentiableAt ℝ (physHermite n) x := Polynomial.differentiableAt_aeval (physHermite n)
 
 @[fun_prop]
-lemma deriv_physHermiteFun_differentiableAt (n m : ℕ) (x : ℝ) :
-    DifferentiableAt ℝ (deriv^[m] (physHermiteFun n)) x := by
-  rw [iterated_deriv_physHermiteFun_eq_aeval]
+lemma deriv_physHermite_differentiableAt (n m : ℕ) (x : ℝ) :
+    DifferentiableAt ℝ (deriv^[m] (physHermite n)) x := by
+  rw [iterated_deriv_physHermite_eq_aeval]
   exact Polynomial.differentiableAt_aeval _
 
-lemma deriv_physHermiteFun (n : ℕ) :
-    deriv (physHermiteFun n) = 2 * n * (physHermiteFun (n - 1)) := by
+lemma deriv_physHermite (n : ℕ) :
+    deriv (physHermite n) = 2 * n * (physHermite (n - 1)) := by
   ext x
-  rw [physHermiteFun_eq_aeval_physHermite]
   rw [Polynomial.deriv_aeval (physHermite n)]
   rw [derivative_physHermite]
-  simp [aeval, mul_assoc, physHermiteFun_eq_aeval_physHermite]
+  simp [aeval, mul_assoc]
 
-lemma fderiv_physHermiteFun
+lemma fderiv_physHermite
     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E)
     (f : E → ℝ) (hf : DifferentiableAt ℝ f x) (n : ℕ) :
-    fderiv ℝ (fun x => physHermiteFun n (f x)) x
-    = (2 * n * physHermiteFun (n - 1) (f x)) • fderiv ℝ f x := by
-  have h := fderiv_comp (𝕜 := ℝ) (g := physHermiteFun n) (f := f) (hg := by fun_prop)
+    fderiv ℝ (fun x => physHermite n (f x)) x
+    = (2 * n * physHermite (n - 1) (f x)) • fderiv ℝ f x := by
+  have h := fderiv_comp (𝕜 := ℝ) (g := physHermite n) (f := f) (hg := by fun_prop)
     (hf := by fun_prop)
-  simp +unfoldPartialApp [Function.comp] at h
+  simp +unfoldPartialApp only [Function.comp] at h
   ext dx
-  simp [deriv_physHermiteFun,h]
+  simp only [h, Polynomial.fderiv_aeval, derivative_physHermite, nsmul_eq_mul, map_mul, map_natCast,
+    ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.smulRight_apply,
+    ContinuousLinearMap.one_apply, smul_eq_mul, ContinuousLinearMap.coe_smul', Pi.smul_apply]
+  simp only [aeval, eval₂AlgHom'_apply, eval₂_ofNat]
   ring
 
 @[simp]
-lemma deriv_physHermiteFun' (x : ℝ)
+lemma deriv_physHermite' (x : ℝ)
     (f : ℝ → ℝ) (hf : DifferentiableAt ℝ f x) (n : ℕ) :
-    deriv (fun x => physHermiteFun n (f x)) x
-    = (2 * n * physHermiteFun (n - 1) (f x)) * deriv f x := by
+    deriv (fun x => physHermite n (f x)) x
+    = (2 * n * physHermite (n - 1) (f x)) * deriv f x := by
   unfold deriv
-  rw [fderiv_physHermiteFun (hf := by fun_prop)]
+  rw [fderiv_physHermite (hf := by fun_prop)]
   rfl
 
 /-!
@@ -227,39 +225,42 @@ lemma deriv_physHermiteFun' (x : ℝ)
 
 -/
 
-lemma deriv_gaussian_eq_physHermiteFun_mul_gaussian (n : ℕ) (x : ℝ) :
+lemma deriv_gaussian_eq_physHermite_mul_gaussian (n : ℕ) (x : ℝ) :
     deriv^[n] (fun y => Real.exp (- y ^ 2)) x =
-    (-1 : ℝ) ^ n * physHermiteFun n x * Real.exp (- x ^ 2) := by
+    (-1 : ℝ) ^ n * physHermite n x * Real.exp (- x ^ 2) := by
   rw [mul_assoc]
   induction' n with n ih generalizing x
-  · rw [Function.iterate_zero_apply, pow_zero, one_mul, physHermiteFun_zero_apply, one_mul]
+  · rw [Function.iterate_zero_apply, pow_zero, one_mul, physHermite_zero_apply, one_mul]
   · replace ih : deriv^[n] _ = _ := _root_.funext ih
     have deriv_gaussian :
       deriv (fun y => Real.exp (-(y ^ 2))) x = -2 * x * Real.exp (-(x ^ 2)) := by
       rw [deriv_exp (by simp)]; simp; ring
     rw [Function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_mul, pow_succ (-1 : ℝ),
-      deriv_gaussian, physHermiteFun_succ]
-    · rw [deriv_physHermiteFun]
+      deriv_gaussian, physHermite_succ]
+    · rw [derivative_physHermite,]
       simp only [Pi.natCast_def, Pi.mul_apply, Pi.ofNat_apply, cast_ofNat, neg_mul, mul_neg,
         mul_one, nsmul_eq_mul, smul_eq_mul]
+      simp only [Polynomial.deriv_aeval, derivative_physHermite, nsmul_eq_mul, map_mul, map_natCast,
+        map_sub, aeval_X]
+      simp only [aeval, eval₂AlgHom'_apply, eval₂_ofNat]
       ring
     · apply Polynomial.differentiable_aeval
     · apply DifferentiableAt.exp
       simp
 
-lemma physHermiteFun_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
-    physHermiteFun n x = (-1 : ℝ) ^ n * deriv^[n]
+lemma physHermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
+    physHermite n x = (-1 : ℝ) ^ n * deriv^[n]
     (fun y => Real.exp (- y ^ 2)) x / Real.exp (- x ^ 2) := by
-  rw [deriv_gaussian_eq_physHermiteFun_mul_gaussian]
+  rw [deriv_gaussian_eq_physHermite_mul_gaussian]
   field_simp [Real.exp_ne_zero]
   rw [← @smul_eq_mul ℝ _ ((-1) ^ n), ← inv_smul_eq_iff₀, mul_assoc, smul_eq_mul, ← inv_pow, ←
     neg_inv, inv_one]
   exact pow_ne_zero _ (by norm_num)
 
-lemma physHermiteFun_eq_deriv_gaussian' (n : ℕ) (x : ℝ) :
-    physHermiteFun n x = (-1 : ℝ) ^ n * deriv^[n] (fun y => Real.exp (- y ^ 2)) x *
+lemma physHermite_eq_deriv_gaussian' (n : ℕ) (x : ℝ) :
+    physHermite n x = (-1 : ℝ) ^ n * deriv^[n] (fun y => Real.exp (- y ^ 2)) x *
     Real.exp (x ^ 2) := by
-  rw [physHermiteFun_eq_deriv_gaussian, Real.exp_neg]
+  rw [physHermite_eq_deriv_gaussian, Real.exp_neg]
   field_simp [Real.exp_ne_zero]
 
 @[fun_prop]
@@ -277,8 +278,8 @@ lemma guassian_integrable_polynomial {b : ℝ} (hb : 0 < b) (P : Polynomial ℤ)
   rw [h2]
   refine MeasureTheory.Integrable.smul (P.coeff i : ℝ) ?_
   apply integrable_rpow_mul_exp_neg_mul_sq (s := i)
-  exact hb
-  exact gt_of_ge_of_gt (Nat.cast_nonneg' i) neg_one_lt_zero
+  · exact hb
+  · exact gt_of_ge_of_gt (Nat.cast_nonneg' i) neg_one_lt_zero
 
 @[fun_prop]
 lemma guassian_integrable_polynomial_cons {b c : ℝ} (hb : 0 < b) (P : Polynomial ℤ) :
@@ -296,18 +297,18 @@ lemma guassian_integrable_polynomial_cons {b c : ℝ} (hb : 0 < b) (P : Polynomi
   rw [h2]
   refine MeasureTheory.Integrable.smul (c ^ i * P.coeff i : ℝ) ?_
   apply integrable_rpow_mul_exp_neg_mul_sq (s := i)
-  exact hb
-  exact gt_of_ge_of_gt (Nat.cast_nonneg' i) neg_one_lt_zero
+  · exact hb
+  · exact gt_of_ge_of_gt (Nat.cast_nonneg' i) neg_one_lt_zero
 
 @[fun_prop]
-lemma physHermiteFun_gaussian_integrable (n p m : ℕ) :
-    MeasureTheory.Integrable (deriv^[m] (physHermiteFun p) * deriv^[n] fun x => Real.exp (-x ^ 2))
+lemma physHermite_gaussian_integrable (n p m : ℕ) :
+    MeasureTheory.Integrable (deriv^[m] (physHermite p) * deriv^[n] fun x => Real.exp (-x ^ 2))
     MeasureTheory.volume := by
-  have h1 : (deriv^[m] (physHermiteFun p) * deriv^[n] fun x => Real.exp (-x ^ 2))
-    = deriv^[m] (physHermiteFun p) *
-    ((-1 : ℝ) ^ n • physHermiteFun n * (fun x => Real.exp (- x ^ 2))) := by
+  have h1 : (deriv^[m] (physHermite p) * deriv^[n] fun x => Real.exp (-x ^ 2))
+    = deriv^[m] (physHermite p) *
+    ((-1 : ℝ) ^ n • physHermite n * (fun x => Real.exp (- x ^ 2))) := by
     funext x
-    simp only [Pi.mul_apply, deriv_gaussian_eq_physHermiteFun_mul_gaussian, Algebra.smul_mul_assoc,
+    simp only [Pi.mul_apply, deriv_gaussian_eq_physHermite_mul_gaussian, Algebra.smul_mul_assoc,
       Pi.smul_apply, smul_eq_mul, mul_eq_mul_left_iff]
     ring_nf
     left
@@ -315,9 +316,9 @@ lemma physHermiteFun_gaussian_integrable (n p m : ℕ) :
   rw [h1]
   simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
   refine MeasureTheory.Integrable.smul ((-1) ^ n) ?_
-  have h2 : deriv^[m] (physHermiteFun p) * physHermiteFun n =
+  have h2 : deriv^[m] (physHermite p) * (physHermite n : ℝ → ℝ) =
       fun x => (derivative^[m] (physHermite p) * physHermite n).aeval x := by
-    rw [iterated_deriv_physHermiteFun_eq_aeval, physHermiteFun_eq_aeval_physHermite]
+    rw [iterated_deriv_physHermite_eq_aeval]
     funext x
     simp
   conv =>
@@ -333,30 +334,30 @@ lemma physHermiteFun_gaussian_integrable (n p m : ℕ) :
   apply guassian_integrable_polynomial
   exact Real.zero_lt_one
 
-lemma integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_exp (n m : ℕ) :
-    ∫ x : ℝ, (physHermiteFun n x * physHermiteFun m x) * Real.exp (-x ^ 2) =
-    (-1 : ℝ) ^ m * ∫ x : ℝ, (physHermiteFun n x * (deriv^[m] fun x => Real.exp (-x ^ 2)) x) := by
-  have h1 (x : ℝ) : (physHermiteFun n x * physHermiteFun m x) * Real.exp (-x ^ 2)
-    = (-1 : ℝ) ^ m * (physHermiteFun n x * (deriv^[m] fun x => Real.exp (-x ^ 2)) x) := by
+lemma integral_physHermite_mul_physHermite_eq_integral_deriv_exp (n m : ℕ) :
+    ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (-x ^ 2) =
+    (-1 : ℝ) ^ m * ∫ x : ℝ, (physHermite n x * (deriv^[m] fun x => Real.exp (-x ^ 2)) x) := by
+  have h1 (x : ℝ) : (physHermite n x * physHermite m x) * Real.exp (-x ^ 2)
+    = (-1 : ℝ) ^ m * (physHermite n x * (deriv^[m] fun x => Real.exp (-x ^ 2)) x) := by
     conv_lhs =>
       enter [1, 2]
-      rw [physHermiteFun_eq_deriv_gaussian']
+      rw [physHermite_eq_deriv_gaussian']
     rw [mul_assoc, mul_assoc, ← Real.exp_add]
     simp only [add_neg_cancel, Real.exp_zero, mul_one]
     ring
   simp [h1]
   exact MeasureTheory.integral_mul_left ((-1) ^ m) fun a =>
-      physHermiteFun n a * deriv^[m] (fun x => Real.exp (-x ^ 2)) a
+      physHermite n a * deriv^[m] (fun x => Real.exp (-x ^ 2)) a
 
-lemma integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_inductive (n m : ℕ) :
+lemma integral_physHermite_mul_physHermite_eq_integral_deriv_inductive (n m : ℕ) :
     (p : ℕ) → (hpm : p ≤ m) →
-    ∫ x : ℝ, (physHermiteFun n x * physHermiteFun m x) * Real.exp (- x ^ 2) =
-    (-1 : ℝ) ^ (m - p) * ∫ x : ℝ, (deriv^[p] (physHermiteFun n) x *
+    ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (- x ^ 2) =
+    (-1 : ℝ) ^ (m - p) * ∫ x : ℝ, (deriv^[p] (physHermite n) x *
     (deriv^[m - p] fun x => Real.exp (-x ^ 2)) x)
   | 0, h => by
-    exact integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_exp n m
+    exact integral_physHermite_mul_physHermite_eq_integral_deriv_exp n m
   | p + 1, h => by
-    rw [integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_inductive n m p]
+    rw [integral_physHermite_mul_physHermite_eq_integral_deriv_inductive n m p (by omega)]
     have h1 : m - p = m - (p + 1) + 1 := by omega
     rw [h1]
     rw [Function.iterate_succ_apply']
@@ -367,9 +368,9 @@ lemma integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_inductive (n
       simp
     rw [h1, mul_assoc]
     congr
-    have hl : ∫ (x : ℝ), deriv^[p] (physHermiteFun n) x *
+    have hl : ∫ (x : ℝ), deriv^[p] (physHermite n) x *
         deriv (deriv^[m - (p + 1)] fun x => Real.exp (-x ^ 2)) x =
-        - ∫ (x : ℝ), deriv (deriv^[p] (physHermiteFun n)) x *
+        - ∫ (x : ℝ), deriv (deriv^[p] (physHermite n)) x *
         deriv^[m - (p + 1)] (fun x => Real.exp (-x ^ 2)) x := by
       apply MeasureTheory.integral_mul_deriv_eq_deriv_mul_of_integrable
       · intro x
@@ -378,62 +379,61 @@ lemma integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_inductive (n
       · intro x
         simp only [hasDerivAt_deriv_iff]
         have h1 : (deriv^[m - (p + 1)] fun x => Real.exp (-x ^ 2)) =
-            fun x => (-1 : ℝ) ^ (m - (p + 1)) * physHermiteFun (m - (p + 1)) x *
+            fun x => (-1 : ℝ) ^ (m - (p + 1)) * physHermite (m - (p + 1)) x *
             Real.exp (- x ^ 2) := by
           funext x
-          exact deriv_gaussian_eq_physHermiteFun_mul_gaussian (m - (p + 1)) x
+          exact deriv_gaussian_eq_physHermite_mul_gaussian (m - (p + 1)) x
         rw [h1]
         fun_prop
       · rw [← Function.iterate_succ_apply' deriv]
-        exact physHermiteFun_gaussian_integrable _ _ _
+        exact physHermite_gaussian_integrable _ _ _
       · rw [← Function.iterate_succ_apply' deriv]
-        exact physHermiteFun_gaussian_integrable _ _ _
+        exact physHermite_gaussian_integrable _ _ _
       · fun_prop
     rw [hl]
     simp only [mul_neg, neg_mul, one_mul, neg_neg]
-    omega
 
-lemma integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv (n m : ℕ) :
-    ∫ x : ℝ, (physHermiteFun n x * physHermiteFun m x) * Real.exp (- x ^ 2) =
-    ∫ x : ℝ, (deriv^[m] (physHermiteFun n) x * (Real.exp (-x ^ 2))) := by
-  rw [integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv_inductive n m m (by rfl)]
+lemma integral_physHermite_mul_physHermite_eq_integral_deriv (n m : ℕ) :
+    ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (- x ^ 2) =
+    ∫ x : ℝ, (deriv^[m] (physHermite n) x * (Real.exp (-x ^ 2))) := by
+  rw [integral_physHermite_mul_physHermite_eq_integral_deriv_inductive n m m (by rfl)]
   simp
 
-lemma physHermiteFun_orthogonal_lt {n m : ℕ} (hnm : n < m) :
-    ∫ x : ℝ, (physHermiteFun n x * physHermiteFun m x) * Real.exp (- x ^ 2) = 0 := by
-  rw [integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv]
-  rw [iterated_deriv_physHermiteFun_eq_aeval, iterate_derivative_physHermite_of_gt hnm]
+lemma physHermite_orthogonal_lt {n m : ℕ} (hnm : n < m) :
+    ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (- x ^ 2) = 0 := by
+  rw [integral_physHermite_mul_physHermite_eq_integral_deriv]
+  rw [iterated_deriv_physHermite_eq_aeval, iterate_derivative_physHermite_of_gt hnm]
   simp
 
-theorem physHermiteFun_orthogonal {n m : ℕ} (hnm : n ≠ m) :
-    ∫ x : ℝ, (physHermiteFun n x * physHermiteFun m x) * Real.exp (- x ^ 2) = 0 := by
+theorem physHermite_orthogonal {n m : ℕ} (hnm : n ≠ m) :
+    ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (- x ^ 2) = 0 := by
   by_cases hnm' : n < m
-  · exact physHermiteFun_orthogonal_lt hnm'
+  · exact physHermite_orthogonal_lt hnm'
   · have hmn : m < n := by omega
     conv_lhs =>
       enter [2, x, 1]
       rw [mul_comm]
-    rw [physHermiteFun_orthogonal_lt hmn]
+    rw [physHermite_orthogonal_lt hmn]
 
-lemma physHermiteFun_orthogonal_cons {n m : ℕ} (hnm : n ≠ m) (c : ℝ) :
-    ∫ x : ℝ, (physHermiteFun n (c * x) * physHermiteFun m (c * x)) *
+lemma physHermite_orthogonal_cons {n m : ℕ} (hnm : n ≠ m) (c : ℝ) :
+    ∫ x : ℝ, (physHermite n (c * x) * physHermite m (c * x)) *
     Real.exp (- c ^ 2 * x ^ 2) = 0 := by
-  trans ∫ x : ℝ, (fun x => (physHermiteFun n x * physHermiteFun m x) * Real.exp (- x^2)) (c * x)
+  trans ∫ x : ℝ, (fun x => (physHermite n x * physHermite m x) * Real.exp (- x^2)) (c * x)
   · congr
     funext x
     simp only [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp, neg_inj, _root_.mul_eq_zero]
     left
     exact Eq.symm (mul_pow c x 2)
   rw [MeasureTheory.Measure.integral_comp_mul_left
-    (fun x => physHermiteFun n x * physHermiteFun m x * Real.exp (-x ^ 2)) c]
-  rw [physHermiteFun_orthogonal hnm]
+    (fun x => physHermite n x * physHermite m x * Real.exp (-x ^ 2)) c]
+  rw [physHermite_orthogonal hnm]
   simp
 
-theorem physHermiteFun_norm (n : ℕ) :
-    ∫ x : ℝ, (physHermiteFun n x * physHermiteFun n x) * Real.exp (- x ^ 2) =
+theorem physHermite_norm (n : ℕ) :
+    ∫ x : ℝ, (physHermite n x * physHermite n x) * Real.exp (- x ^ 2) =
     ↑n ! * 2 ^ n * √Real.pi := by
-  rw [integral_physHermiteFun_mul_physHermiteFun_eq_integral_deriv]
-  rw [iterated_deriv_physHermiteFun_eq_aeval]
+  rw [integral_physHermite_mul_physHermite_eq_integral_deriv]
+  rw [iterated_deriv_physHermite_eq_aeval]
   simp only [iterate_derivative_physHermite_self,
     Int.cast_pow, Int.cast_ofNat, map_pow]
   conv_lhs =>
@@ -448,22 +448,22 @@ theorem physHermiteFun_norm (n : ℕ) :
     simp
   rw [h1]
 
-lemma physHermiteFun_norm_cons (n : ℕ) (c : ℝ) :
-    ∫ x : ℝ, (physHermiteFun n (c * x) * physHermiteFun n (c * x)) * Real.exp (- c ^ 2 * x ^ 2) =
+lemma physHermite_norm_cons (n : ℕ) (c : ℝ) :
+    ∫ x : ℝ, (physHermite n (c * x) * physHermite n (c * x)) * Real.exp (- c ^ 2 * x ^ 2) =
     |c⁻¹| • (↑n ! * 2 ^ n * √Real.pi) := by
-  trans ∫ x : ℝ, (fun x => (physHermiteFun n x * physHermiteFun n x) * Real.exp (- x^2)) (c * x)
+  trans ∫ x : ℝ, (fun x => (physHermite n x * physHermite n x) * Real.exp (- x^2)) (c * x)
   · congr
     funext x
     simp only [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp, neg_inj, _root_.mul_eq_zero, or_self]
     left
     exact Eq.symm (mul_pow c x 2)
   rw [MeasureTheory.Measure.integral_comp_mul_left
-    (fun x => physHermiteFun n x * physHermiteFun n x * Real.exp (-x ^ 2)) c]
-  rw [physHermiteFun_norm]
+    (fun x => physHermite n x * physHermite n x * Real.exp (-x ^ 2)) c]
+  rw [physHermite_norm]
 
-lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : ℕ) →
+lemma polynomial_mem_physHermite_span_induction (P : Polynomial ℤ) : (n : ℕ) →
     (hn : P.natDegree = n) →
-    (fun x => P.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun)
+    (P : ℝ → ℝ) ∈ Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ)))
   | 0, h => by
     rw [natDegree_eq_zero] at h
     obtain ⟨x, rfl⟩ := h
@@ -476,16 +476,17 @@ lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : 
     · subst hP0
       simp only [map_zero]
       change 0 ∈ _
-      exact Submodule.zero_mem (Submodule.span ℝ (Set.range physHermiteFun))
+      exact Submodule.zero_mem (Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ))))
     let P' := ((coeff (physHermite (n + 1)) (n + 1)) • P -
         (coeff P (n + 1)) • physHermite (n + 1))
-    have hP'mem : (fun x => P'.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun) := by
+    have hP'mem : (fun x => P'.aeval x) ∈ Submodule.span ℝ
+        (Set.range (fun n => (physHermite n : ℝ → ℝ))) := by
       by_cases hP' : P' = 0
       · rw [hP']
         simp only [map_zero]
         change 0 ∈ _
-        exact Submodule.zero_mem (Submodule.span ℝ (Set.range physHermiteFun))
-      · exact polynomial_mem_physHermiteFun_span_induction P' P'.natDegree (by rfl)
+        exact Submodule.zero_mem (Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ))))
+      · exact polynomial_mem_physHermite_span_induction P' P'.natDegree (by rfl)
     simp only [P'] at hP'mem
     have hl : (fun x => (aeval x) ((physHermite (n + 1)).coeff (n + 1) • P -
         P.coeff (n + 1) • physHermite (n + 1)))
@@ -498,47 +499,45 @@ lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : 
       simp [aeval]
     rw [hl] at hP'mem
     rw [Submodule.sub_mem_iff_left] at hP'mem
-    rw [Submodule.smul_mem_iff] at hP'mem
-    exact hP'mem
-    simp only [ne_eq, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true,
-      pow_eq_zero_iff, OfNat.ofNat_ne_zero, P']
+    · rw [Submodule.smul_mem_iff] at hP'mem
+      · exact hP'mem
+      · simp
     apply Submodule.smul_mem _
     refine Finsupp.mem_span_range_iff_exists_finsupp.mpr ?_
     use Finsupp.single (n + 1) 1
     simp
-    rfl
 decreasing_by
   rw [Polynomial.natDegree_lt_iff_degree_lt]
-  apply (Polynomial.degree_lt_iff_coeff_zero _ _).mpr
-  intro m hm'
-  simp only [coeff_physHermite_self_succ, Int.cast_pow, Int.cast_ofNat, coeff_sub,
-      Int.cast_id]
-  change n + 1 ≤ m at hm'
-  rw [coeff_smul, coeff_smul]
-  by_cases hm : m = n + 1
-  · subst hm
-    simp only [smul_eq_mul, coeff_physHermite_self_succ]
-    ring
-  · rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt (n := m)]
-    simp only [smul_eq_mul, mul_zero, sub_self]
-    · rw [← Polynomial.natDegree_lt_iff_degree_lt]
-      simp only [natDegree_physHermite]
-      omega
-      simp
-    · rw [← Polynomial.natDegree_lt_iff_degree_lt]
-      omega
-      exact hP0
+  · apply (Polynomial.degree_lt_iff_coeff_zero _ _).mpr
+    intro m hm'
+    simp only [coeff_physHermite_self_succ, Int.cast_pow, Int.cast_ofNat, coeff_sub,
+        Int.cast_id]
+    change n + 1 ≤ m at hm'
+    rw [coeff_smul, coeff_smul]
+    by_cases hm : m = n + 1
+    · subst hm
+      simp only [smul_eq_mul, coeff_physHermite_self_succ]
+      ring
+    · rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt (n := m)]
+      · simp only [smul_eq_mul, mul_zero, sub_self]
+      · rw [← Polynomial.natDegree_lt_iff_degree_lt]
+        · simp only [natDegree_physHermite]
+          omega
+        · simp
+      · rw [← Polynomial.natDegree_lt_iff_degree_lt]
+        · omega
+        · exact hP0
   · exact hP'
 
-lemma polynomial_mem_physHermiteFun_span (P : Polynomial ℤ) :
-    (fun x => P.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun) := by
-  exact polynomial_mem_physHermiteFun_span_induction P P.natDegree rfl
+lemma polynomial_mem_physHermite_span (P : Polynomial ℤ) :
+    (P : ℝ → ℝ) ∈ Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ))) :=
+  polynomial_mem_physHermite_span_induction P P.natDegree rfl
 
-lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) :
+lemma cos_mem_physHermite_span_topologicalClosure (c : ℝ) :
     (fun (x : ℝ) => Real.cos (c * x)) ∈
-    (Submodule.span ℝ (Set.range physHermiteFun)).topologicalClosure := by
+    (Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ)))).topologicalClosure := by
   change (fun (x : ℝ) => Real.cos (c * x)) ∈
-    closure (Submodule.span ℝ (Set.range physHermiteFun))
+    closure (Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ))))
   have h1 := Real.hasSum_cos
   simp [HasSum] at h1
   have h1 : Filter.Tendsto
@@ -546,7 +545,7 @@ lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) :
     Filter.atTop (nhds (fun x => Real.cos (c * x))) := by
     exact tendsto_pi_nhds.mpr fun x => h1 (c * x)
   have h2 (z : Finset ℕ) : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) ∈
-      ↑(Submodule.span ℝ (Set.range physHermiteFun)) := by
+      ↑(Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ)))) := by
     have h0 : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) =
       ∑ x ∈ z, (((-1) ^ x * c ^ (2 * x) / ↑(2 * x)!) • fun (y : ℝ) => (y) ^ (2 * x)) := by
       funext y
@@ -563,7 +562,7 @@ lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) :
       funext y
       simp [P]
     rw [hy]
-    exact polynomial_mem_physHermiteFun_span P
+    exact polynomial_mem_physHermite_span P
   refine mem_closure_of_tendsto h1 ?_
   simp [h2]
 
diff --git a/PhysLean/PerturbationTheory/Koszul/KoszulSign.lean b/PhysLean/PerturbationTheory/Koszul/KoszulSign.lean
index 1c90cc55..dc18e111 100644
--- a/PhysLean/PerturbationTheory/Koszul/KoszulSign.lean
+++ b/PhysLean/PerturbationTheory/Koszul/KoszulSign.lean
@@ -73,17 +73,15 @@ lemma koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 
     simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
       List.getElem_cons_zero, Fin.isValue, List.eraseIdx_zero, List.tail_cons, koszulSign]
     intro h
-    rw [koszulSignInsert_boson]
+    rw [koszulSignInsert_boson _ _ _ h]
     simp only [one_mul]
-    exact h
   | φ :: φs, ⟨n + 1, h⟩ => by
     simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
       List.eraseIdx_cons_succ]
     intro h'
-    rw [koszulSign, koszulSign, koszulSign_erase_boson q le φs ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
+    rw [koszulSign, koszulSign, koszulSign_erase_boson q le φs ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
     congr 1
     rw [koszulSignInsert_erase_boson q le φ φs ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
-    exact h'
 
 lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
     (φs : List 𝓕) → (n : ℕ) → (hn : n ≤ φs.length) →
@@ -101,7 +99,7 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
     simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
     rw [koszulSign]
     trans koszulSign q le (φ1 :: φs) * koszulSignInsert q le φ (φ1 :: φs)
-    ring
+    · ring
     simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
       orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso,
       PhysLean.Fin.equivCons_trans,
@@ -123,7 +121,7 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
     conv_lhs =>
       rw [List.insertIdx_succ_cons]
       rw [koszulSign]
-    rw [koszulSign_insertIdx]
+    rw [koszulSign_insertIdx _ _ _ (Nat.le_of_lt_succ h)]
     conv_rhs =>
       rhs
       simp only [List.insertIdx_succ_cons]
@@ -154,7 +152,7 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
       ⟨n, hnsL⟩
     let nro : Fin (rs.length + 1) :=
       ⟨↑(orderedInsertPos le rs φ1), orderedInsertPos_lt_length le rs φ1⟩
-    rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
+    rw [koszulSignInsert_insertIdx _ _ _ _ _ _ (Nat.le_of_lt_succ h), koszulSignInsert_cons]
     trans koszulSignInsert q le φ1 φs * (koszulSignCons q le φ1 φ *
       𝓢(q φ, ofList q (rs.take ni)))
     · simp only [rs, ni]
@@ -189,13 +187,11 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
       rw [exchangeSign_symm]
     · simp only [hn, ↓reduceIte, Fin.val_succ]
       rw [ofList_take_insertIdx_le, map_mul, ← mul_assoc]
-      congr 1
-      rw [exchangeSign_mul_self, koszulSignCons]
-      simp only [hc2 hn, ↓reduceIte]
-      exact Nat.le_of_not_lt hn
-      exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le rs φ1)
-    · exact Nat.le_of_lt_succ h
-    · exact Nat.le_of_lt_succ h
+      · congr 1
+        rw [exchangeSign_mul_self, koszulSignCons]
+        simp only [hc2 hn, ↓reduceIte]
+      · exact Nat.le_of_not_lt hn
+      · exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le rs φ1)
 
 lemma insertIdx_eraseIdx {I : Type} : (n : ℕ) → (r : List I) → (hn : n < r.length) →
     List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
@@ -292,7 +288,7 @@ lemma koszulSign_eq_rel_eq_stat_append {ψ φ : 𝓕} [IsTrans 𝓕 le]
   simp only [koszulSign, ← mul_assoc]
   trans 1 * koszulSign q le φs
   swap
-  simp only [one_mul]
+  · simp only [one_mul]
   congr
   simp only [koszulSignInsert, ite_mul, neg_mul]
   simp_all only [and_self, ite_true]
@@ -311,13 +307,9 @@ lemma koszulSign_eq_rel_eq_stat {ψ φ : 𝓕} [IsTrans 𝓕 le]
     simp only [mul_eq_mul_right_iff]
     left
     trans koszulSignInsert q le φ'' (φ :: ψ :: (φs' ++ φs))
-    apply koszulSignInsert_eq_perm
-    refine List.Perm.symm (List.perm_cons_append_cons φ ?_)
-    exact List.Perm.symm List.perm_middle
-    rw [koszulSignInsert_eq_remove_same_stat_append q le]
-    exact h1
-    exact h2
-    exact hq
+    · apply koszulSignInsert_eq_perm
+      exact (List.perm_cons_append_cons φ List.perm_middle.symm).symm
+    · rw [koszulSignInsert_eq_remove_same_stat_append q le h1 h2 hq]
 
 lemma koszulSign_of_sorted : (φs : List 𝓕)
     → (hs : List.Sorted le φs) → koszulSign q le φs = 1
@@ -348,9 +340,9 @@ lemma koszulSign_of_append_eq_insertionSort_left [IsTotal 𝓕 le] [IsTrans 𝓕
         List.insertIdx (List.insertionSort le φs).length φ (List.insertionSort le φs ++ φs') := by
       rw [insertIdx_length_fst_append]
     rw [h1, h2]
-    rw [koszulSign_insertIdx]
+    rw [koszulSign_insertIdx _ _ _ _ _ (by simp)]
     simp only [instCommGroup.eq_1, List.take_left', List.length_insertionSort]
-    rw [koszulSign_insertIdx]
+    rw [koszulSign_insertIdx _ _ _ _ _ (by simp)]
     simp only [mul_assoc, instCommGroup.eq_1, List.length_insertionSort, List.take_left',
       ofList_insertionSort, mul_eq_mul_left_iff]
     left
@@ -376,8 +368,6 @@ lemma koszulSign_of_append_eq_insertionSort_left [IsTotal 𝓕 le] [IsTrans 𝓕
       rw [insertIdx_length_fst_append]
       symm
       apply insertionSort_insertionSort_append
-    · simp
-    · simp
 
 lemma koszulSign_of_append_eq_insertionSort [IsTotal 𝓕 le] [IsTrans 𝓕 le] : (φs'' φs φs' : List 𝓕) →
     koszulSign q le (φs'' ++ φs ++ φs') =
@@ -419,8 +409,8 @@ lemma koszulSign_perm_eq_append [IsTrans 𝓕 le] (φ : 𝓕) (φs φs' φs2 : L
   · intro x y l h
     simp_all only [List.mem_cons, forall_eq_or_imp, List.cons_append]
     apply Wick.koszulSign_swap_eq_rel_cons
-    exact IsTrans.trans y φ x h.1.2 h.2.1.1
-    exact IsTrans.trans x φ y h.2.1.2 h.1.1
+    · exact IsTrans.trans y φ x h.1.2 h.2.1.1
+    · exact IsTrans.trans x φ y h.2.1.2 h.1.1
   · intro l1 l2 l3 h1 h2 ih1 ih2 h
     simp_all only [and_self, implies_true, nonempty_prop, forall_const, motive]
     refine (ih2 ?_)
diff --git a/PhysLean/PerturbationTheory/Koszul/KoszulSignInsert.lean b/PhysLean/PerturbationTheory/Koszul/KoszulSignInsert.lean
index d1cf2c60..553acf09 100644
--- a/PhysLean/PerturbationTheory/Koszul/KoszulSignInsert.lean
+++ b/PhysLean/PerturbationTheory/Koszul/KoszulSignInsert.lean
@@ -92,8 +92,8 @@ lemma koszulSignInsert_eq_filter (φ : 𝓕) : (φs : List 𝓕) →
       simp only [Fin.isValue, h, ↓reduceIte]
       rw [koszulSignInsert_eq_filter]
       congr
-      simp only [decide_not]
-      simp
+      · simp only [decide_not]
+      · simp
 
 lemma koszulSignInsert_eq_cons [IsTotal 𝓕 le] (φ : 𝓕) (φs : List 𝓕) :
     koszulSignInsert q le φ φs = koszulSignInsert q le φ (φ :: φs) := by
@@ -131,10 +131,10 @@ lemma koszulSignInsert_eq_grade (φ : 𝓕) (φs : List 𝓕) :
           simpa [ofList] using ih
       · simp [hr1]
     · rw [List.filter_cons_of_neg]
-      simp only [decide_not, Fin.isValue]
-      rw [koszulSignInsert_eq_filter] at ih
-      simpa [ofList] using ih
-      simpa using hr1
+      · simp only [decide_not, Fin.isValue]
+        rw [koszulSignInsert_eq_filter] at ih
+        simpa [ofList] using ih
+      · simpa using hr1
 
 lemma koszulSignInsert_eq_perm (φs φs' : List 𝓕) (φ : 𝓕) (h : φs.Perm φs') :
     koszulSignInsert q le φ φs = koszulSignInsert q le φ φs' := by
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
index 2fe732db..3d8acce1 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean
@@ -78,14 +78,14 @@ variable (Q : HarmonicOscillator)
 @[simp]
 lemma m_mul_ω_div_two_ℏ_pos : 0 < Q.m * Q.ω / (2 * Q.ℏ) := by
   apply div_pos
-  exact mul_pos Q.hm Q.hω
-  exact mul_pos (by norm_num) Q.hℏ
+  · exact mul_pos Q.hm Q.hω
+  · exact mul_pos (by norm_num) Q.hℏ
 
 @[simp]
 lemma m_mul_ω_div_ℏ_pos : 0 < Q.m * Q.ω / Q.ℏ := by
   apply div_pos
-  exact mul_pos Q.hm Q.hω
-  exact Q.hℏ
+  · exact mul_pos Q.hm Q.hω
+  · exact Q.hℏ
 
 lemma m_ne_zero : Q.m ≠ 0 := by
   have h1 := Q.hm
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
index 08f56119..6c162369 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean
@@ -52,11 +52,11 @@ lemma mul_eigenfunction_integrable (f : ℝ → ℂ) (hf : MemHS f) :
     funext x
     simp
 
-lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
-    MeasureTheory.Integrable (fun x => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+lemma mul_physHermite_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
+    MeasureTheory.Integrable (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by
   have h2 : (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) • (fun (x : ℝ) =>
-      (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) *
+      (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) *
       (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) = fun x =>
       Q.eigenfunction n x * f x := by
     funext x
@@ -67,7 +67,7 @@ lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
   have h1 := Q.mul_eigenfunction_integrable f hf (n := n)
   rw [← h2] at h1
   rw [IsUnit.integrable_smul_iff] at h1
-  exact h1
+  · exact h1
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
     isUnit_iff_ne_zero, ne_eq, _root_.mul_eq_zero, inv_eq_zero, Complex.ofReal_eq_zero, cast_nonneg,
     Real.sqrt_eq_zero, cast_eq_zero, pow_eq_zero_iff', OfNat.ofNat_ne_zero, false_and, or_false,
@@ -80,14 +80,14 @@ lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
     · apply mul_pos Real.pi_pos Q.hℏ
 
 lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial ℤ) :
-    MeasureTheory.Integrable (fun x => ((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    MeasureTheory.Integrable (fun x => (P (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (f x * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)))) volume := by
-  have h1 := polynomial_mem_physHermiteFun_span P
+  have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1
-  have h2 : (fun x => ↑((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) *
+  have h2 : (fun x => ↑(P (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))))
-    = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by
     funext x
     rw [← ha]
@@ -100,9 +100,9 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial
   intro i hi
   simp only [mul_assoc]
   have hf' : (fun a_1 =>
-    ↑(a i) * (↑(physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * a_1)) *
+    ↑(a i) * (↑(physHermite i (√(Q.m * Q.ω / Q.ℏ) * a_1)) *
     (f a_1 * ↑(Real.exp (- Q.m * (Q.ω * a_1 ^ 2) / (2 * Q.ℏ))))))
-    = fun x => (a i) • ((physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    = fun x => (a i) • ((physHermite i (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by
     funext x
     simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -112,7 +112,7 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial
     simp_all
   rw [hf']
   apply MeasureTheory.Integrable.smul
-  exact Q.mul_physHermiteFun_integrable f hf i
+  exact Q.mul_physHermite_integrable f hf i
 
 lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
     MeasureTheory.Integrable (fun x => x ^ r *
@@ -130,8 +130,9 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
         Complex.ofReal_pow, Complex.ofReal_ofNat, Pi.smul_apply, smul_eq_mul]
       ring
     rw [h2] at h1
-    rw [IsUnit.integrable_smul_iff] at h1
-    simpa using h1
+    suffices h2 : IsUnit (↑(√(Q.m * Q.ω / Q.ℏ) ^ r : ℂ)) by
+      rw [IsUnit.integrable_smul_iff h2] at h1
+      simpa using h1
     simp only [isUnit_iff_ne_zero, ne_eq, pow_eq_zero_iff', Complex.ofReal_eq_zero, not_and,
       Decidable.not_not]
     have h1 : √(Q.m * Q.ω / Q.ℏ) ≠ 0 := by
@@ -142,7 +143,7 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
     simp [h1]
   · simp only [ne_eq, Decidable.not_not] at hr
     subst hr
-    simpa using Q.mul_physHermiteFun_integrable f hf 0
+    simpa using Q.mul_physHermite_integrable f hf 0
 
 /-!
 
@@ -164,16 +165,16 @@ local notation "hm" => Q.hm
 local notation "hℏ" => Q.hℏ
 local notation "hω" => Q.hω
 
-lemma orthogonal_physHermiteFun_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
+lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (n : ℕ) :
-    ∫ (x : ℝ), (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    ∫ (x : ℝ), (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
     = 0 := by
   have h1 := Q.orthogonal_eigenfunction_of_mem_orthogonal f hf hOrth n
   have h2 : (fun (x : ℝ) =>
           (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) *
-            (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) * f x *
+            (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) * f x *
             Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
     = fun x => Q.eigenfunction n x * f x := by
     funext x
@@ -207,14 +208,14 @@ lemma orthogonal_physHermiteFun_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS
 lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (P : Polynomial ℤ) :
-    ∫ x : ℝ, ((fun x => P.aeval x) (√(m * ω / ℏ) * x)) *
+    ∫ x : ℝ, (P (√(m * ω / ℏ) * x)) *
       (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by
-  have h1 := polynomial_mem_physHermiteFun_span P
+  have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1
-  have h2 : (fun x => ↑((fun x => P.aeval x) (√(m * ω / ℏ) * x)) *
+  have h2 : (fun x => ↑(P (√(m * ω / ℏ) * x)) *
     (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))))
-    = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(m * ω / ℏ) * x)) *
+    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (√(m * ω / ℏ) * x)) *
     (f x * Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) := by
     funext x
     rw [← ha]
@@ -231,7 +232,7 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     rw [integral_mul_left]
     simp only [_root_.mul_eq_zero, Complex.ofReal_eq_zero]
     right
-    rw [← Q.orthogonal_physHermiteFun_of_mem_orthogonal f hf hOrth x]
+    rw [← Q.orthogonal_physHermite_of_mem_orthogonal f hf hOrth x]
     congr
     funext x
     simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -243,9 +244,9 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     ring
   · /- Integrablility -/
     intro i hi
-    have hf' : (fun x => ↑(a i) * ↑(physHermiteFun i (√(m * ω / ℏ) * x)) *
+    have hf' : (fun x => ↑(a i) * ↑(physHermite i (√(m * ω / ℏ) * x)) *
         (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))))
-        = a i • (fun x => (physHermiteFun i (√(m * ω / ℏ) * x)) *
+        = a i • (fun x => (physHermite i (√(m * ω / ℏ) * x)) *
         (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) := by
       funext x
       simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -254,7 +255,7 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       ring
     rw [hf']
     apply Integrable.smul
-    exact Q.mul_physHermiteFun_integrable f hf i
+    exact Q.mul_physHermite_integrable f hf i
 
 /-- If `f` is a function `ℝ → ℂ` satisfying `MemHS f` such that it is orthogonal
   to all `eigenfunction n` then it is orthogonal to
@@ -296,7 +297,7 @@ lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     subst hr
     simp only [pow_zero, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
       Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, one_mul]
-    rw [← Q.orthogonal_physHermiteFun_of_mem_orthogonal f hf hOrth 0]
+    rw [← Q.orthogonal_physHermite_of_mem_orthogonal f hf hOrth 0]
     congr
     funext x
     simp
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
index 1b1ea08a..a93a5dc2 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
@@ -21,20 +21,20 @@ open Nat
 open PhysLean
 open HilbertSpace
 
-/-- The `n`th  eigenfunction of the Harmonic oscillator is defined as the function `ℝ → ℂ`
+/-- The `n`th eigenfunction of the Harmonic oscillator is defined as the function `ℝ → ℂ`
   taking `x : ℝ` to
 
-  `1/√(2^n n!) (m ω /(π ℏ))^(1/4) * physHermiteFun n (√(m ω /ℏ) x) * e ^ (- m ω x^2/2ℏ)`.
+  `1/√(2^n n!) (m ω /(π ℏ))^(1/4) * physHermite n (√(m ω /ℏ) x) * e ^ (- m ω x^2/2ℏ)`.
 
 -/
 noncomputable def eigenfunction (n : ℕ) : ℝ → ℂ := fun x =>
   1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
-  physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))
+  physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))
 
 lemma eigenfunction_eq (n : ℕ) :
     Q.eigenfunction n = fun (x : ℝ) =>
     ((1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-    Complex.ofReal (physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) *
+    Complex.ofReal (physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) *
     Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by
   funext x
   simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div,
@@ -46,11 +46,11 @@ lemma eigenfunction_zero : Q.eigenfunction 0 = fun (x : ℝ) =>
     (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
     Complex.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
   funext x
-  simp [eigenfunction, physHermiteFun]
+  simp [eigenfunction]
 
 lemma eigenfunction_eq_mul_eigenfunction_zero (n : ℕ) :
     Q.eigenfunction n = fun x => Complex.ofReal (1/Real.sqrt (2 ^ n * n !))
-    * Complex.ofReal (physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))
+    * Complex.ofReal (physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))
     * Q.eigenfunction 0 x := by
   match n with
   | 0 =>
@@ -60,13 +60,13 @@ lemma eigenfunction_eq_mul_eigenfunction_zero (n : ℕ) :
     rw [eigenfunction, eigenfunction_zero]
     repeat rw [mul_assoc]
     congr 1
-    simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
-      Complex.ofReal_inv]
-    rw [mul_comm, mul_assoc]
-    congr 1
-    simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
-      Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat]
-    ring_nf
+    · simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
+        Complex.ofReal_inv]
+    · rw [mul_comm, mul_assoc]
+      congr 1
+      simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
+        Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat]
+      ring_nf
 
 /-!
 
@@ -81,18 +81,17 @@ lemma eigenfunction_integrable (n : ℕ) : MeasureTheory.Integrable (Q.eigenfunc
   apply MeasureTheory.Integrable.const_mul
   apply MeasureTheory.Integrable.ofReal
   change MeasureTheory.Integrable
-    (fun x => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) MeasureTheory.volume
-  have h1 : (fun x => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+  have h1 : (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) =
-      (fun x => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+      (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (Real.exp (- (Q.m * Q.ω / (2* Q.ℏ)) * x ^ 2))) := by
     funext x
     simp only [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp]
     left
     field_simp
   rw [h1]
-  rw [physHermiteFun_eq_aeval_physHermite]
   apply guassian_integrable_polynomial_cons
   simp
 
@@ -101,13 +100,12 @@ lemma eigenfunction_integrable (n : ℕ) : MeasureTheory.Integrable (Q.eigenfunc
 lemma eigenfunction_conj (n : ℕ) (x : ℝ) :
     (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x := by
   rw [eigenfunction_eq]
-  simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
-    neg_mul, map_mul, map_inv₀, Complex.conj_ofReal]
+  simp [-Complex.ofReal_exp]
 
 lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
     ‖Q.eigenfunction n x‖ = (1/Real.sqrt (2 ^ n * n !) *
     Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-    (|physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)| *
+    (|physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)| *
     Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))) := by
   rw [eigenfunction_eq]
   simp only [neg_mul, Complex.ofReal_mul, Complex.norm_eq_abs]
@@ -124,17 +122,17 @@ lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) :
 lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) :
     ‖Q.eigenfunction n x‖ ^ 2 = (1/Real.sqrt (2 ^ n * n !) *
     Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) ^ 2 *
-    ((physHermiteFun n
+    ((physHermite n
     (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) ^ 2 * Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
   trans (1/Real.sqrt (2 ^ n * n !) *
     Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) ^ 2 *
-    ((|physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)|) ^ 2 *
+    ((|physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)|) ^ 2 *
     (Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) ^ (2 : ℝ)))
   · simp only [Real.rpow_two]
     rw [eigenfunction_point_norm]
     ring
   · congr 2
-    · exact sq_abs (physHermiteFun n _)
+    · exact sq_abs (physHermite n _)
     · rw [← Real.exp_mul]
       congr 1
       ring
@@ -150,7 +148,7 @@ lemma eigenfunction_square_integrable (n : ℕ) :
   conv =>
     enter [1, x]
     rw [eigenfunction_point_norm_sq]
-    rw [physHermiteFun_pow, h0]
+    rw [physHermite_pow, h0]
   apply MeasureTheory.Integrable.const_mul
   apply guassian_integrable_polynomial_cons
   simp
@@ -158,9 +156,8 @@ lemma eigenfunction_square_integrable (n : ℕ) :
 /-- The eigenfunctions are almost everywhere strongly measurable. -/
 @[fun_prop]
 lemma eigenfunction_aeStronglyMeasurable (n : ℕ) :
-    MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) := by
-  apply MeasureTheory.Integrable.aestronglyMeasurable
-  exact Q.eigenfunction_integrable n
+    MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) :=
+  (Q.eigenfunction_integrable n).aestronglyMeasurable
 
 /-- The eigenfunctions are members of the Hilbert space. -/
 lemma eigenfunction_memHS (n : ℕ) : MemHS (Q.eigenfunction n) := by
@@ -187,14 +184,14 @@ lemma eigenfunction_mul (n p : ℕ) :
     (Q.eigenfunction n x) * (Q.eigenfunction p x) =
     ((1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) *
     ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))))) *
-    Complex.ofReal ((physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
-    physHermiteFun p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) * (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ))) := by
+    Complex.ofReal ((physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
+    physHermite p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) * (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ))) := by
   calc Q.eigenfunction n x * Q.eigenfunction p x
     _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) *
       (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
       Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
-        physHermiteFun p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) *
+      (physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
+        physHermite p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) *
       (Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
       simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul,
         one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -202,8 +199,8 @@ lemma eigenfunction_mul (n p : ℕ) :
       ring
     _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) *
       ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
-        physHermiteFun p (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) *
+      (physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) *
+        physHermite p (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) *
       (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by
       congr 1
       · congr 1
@@ -226,13 +223,13 @@ lemma eigenfunction_mul (n p : ℕ) :
 lemma eigenfunction_mul_self (n : ℕ) :
     (Q.eigenfunction n x) * (Q.eigenfunction n x) =
     ((1/ (2 ^ n * n !)) * (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-    Complex.ofReal ((physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x))^2 *
+    Complex.ofReal ((physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x))^2 *
     (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ))) := by
   calc Q.eigenfunction n x * Q.eigenfunction n x
     _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ n * n !)) *
       (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) *
       Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x))^2 *
+      (physHermite n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x))^2 *
       (Real.exp (-Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by
       simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul,
         one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -240,7 +237,7 @@ lemma eigenfunction_mul_self (n : ℕ) :
       ring
     _ = (1/ (2 ^ n * n !)) *
       ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) *
-      (physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))^2 *
+      (physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))^2 *
       (Real.exp (- Q.m * Q.ω * x^2 /Q.ℏ)) := by
       congr 1
       · congr 1
@@ -251,10 +248,9 @@ lemma eigenfunction_mul_self (n : ℕ) :
             trans Complex.ofReal ((2 ^ n * ↑n !))
             · congr 1
               refine Real.mul_self_sqrt ?_
-              refine Left.mul_nonneg ?_ ?_
+              refine Left.mul_nonneg ?_ (cast_nonneg' n !)
               refine pow_nonneg ?_ n
               simp only [ofNat_nonneg]
-              exact cast_nonneg' n !
             simp
           · rw [← Complex.ofReal_mul]
             congr
@@ -290,10 +286,10 @@ lemma eigenfunction_normalized (n : ℕ) :
     refine div_nonneg ?_ ?_
     exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
     exact le_of_lt Q.hℏ
-  have hc : (∫ (x : ℝ), physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) ^ 2 *
+  have hc : (∫ (x : ℝ), physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) ^ 2 *
       Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ))
-      = ∫ (x : ℝ), (physHermiteFun n (c * x) *
-      physHermiteFun n (c * x)) * Real.exp (- c^2 * x ^ 2) := by
+      = ∫ (x : ℝ), (physHermite n (c * x) *
+      physHermite n (c * x)) * Real.exp (- c^2 * x ^ 2) := by
     congr
     funext x
     congr
@@ -301,7 +297,7 @@ lemma eigenfunction_normalized (n : ℕ) :
       exact pow_two _
     simp only [neg_mul, h1, c]
     field_simp
-  rw [hc, physHermiteFun_norm_cons]
+  rw [hc, physHermite_norm_cons]
   simp only [one_div, mul_inv_rev, smul_eq_mul, Complex.ofReal_mul, Complex.ofReal_natCast,
     Complex.ofReal_pow, Complex.ofReal_ofNat, c]
   ring_nf
@@ -342,8 +338,9 @@ lemma eigenfunction_normalized (n : ℕ) :
     exact Real.pi_pos
   rw [h1]
   simp only [one_mul, c]
-  rw [mul_comm, ← IsUnit.eq_mul_inv_iff_mul_eq]
-  simp only [one_mul, c]
+  suffices h2 : IsUnit (↑√(Q.m * Q.ω * Q.ℏ⁻¹) : ℂ) by
+    rw [mul_comm, ← IsUnit.eq_mul_inv_iff_mul_eq h2]
+    simp only [one_mul, c]
   simp only [isUnit_iff_ne_zero, ne_eq, Complex.ofReal_eq_zero, c]
   refine Real.sqrt_ne_zero'.mpr ?_
   rw [propext (lt_mul_inv_iff₀ Q.hℏ)]
@@ -369,20 +366,18 @@ lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) :
     refine div_nonneg ?_ ?_
     exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
     exact le_of_lt Q.hℏ
-  have hc : (∫ (x : ℝ), (physHermiteFun n (c * x) * physHermiteFun p (c * x)) *
+  have hc : (∫ (x : ℝ), (physHermite n (c * x) * physHermite p (c * x)) *
       Real.exp (-Q.m * Q.ω * x ^ 2 / Q.ℏ))
-      = ∫ (x : ℝ), (physHermiteFun n (c * x) * physHermiteFun p (c * x)) *
+      = ∫ (x : ℝ), (physHermite n (c * x) * physHermite p (c * x)) *
       Real.exp (- c^2 * x ^ 2) := by
     congr
     funext x
     congr
     simp only [neg_mul, h1, c]
     field_simp
-  rw [hc]
-  rw [physHermiteFun_orthogonal_cons]
+  rw [hc, physHermite_orthogonal_cons hnp]
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
-    mul_one, Complex.ofReal_zero, mul_zero, c]
-  exact hnp
+      mul_one, Complex.ofReal_zero, mul_zero, c]
 
 /-- The eigenfunctions are orthonormal within the Hilbert space. -/
 lemma eigenfunction_orthonormal :
diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean
index f10d9af7..a2efe323 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean
@@ -92,35 +92,34 @@ lemma schrodingerOperator_eigenfunction_zero (x : ℝ) :
   field_simp
   ring
 
-lemma deriv_physHermiteFun_succ (n : ℕ) :
-    deriv (fun x => Complex.ofReal (physHermiteFun (n + 1) (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))) =
+lemma deriv_physHermite_succ (n : ℕ) :
+    deriv (fun x => Complex.ofReal (physHermite (n + 1) (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))) =
     fun x =>
     Complex.ofReal (Real.sqrt (Q.m * Q.ω / Q.ℏ)) * 2 * (n + 1) *
-    physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) := by
+    physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x) := by
   funext x
-  trans deriv (Complex.ofReal ∘ physHermiteFun (n + 1) ∘
+  trans deriv (Complex.ofReal ∘ physHermite (n + 1) ∘
     fun (x : ℝ) => (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) x
   · rfl
-  rw [fderiv_comp_deriv]
-  rw [fderiv_comp_deriv]
+  rw [fderiv_comp_deriv _ (by fun_prop) (by fun_prop)]
+  rw [fderiv_comp_deriv _ (by fun_prop) (by fun_prop)]
   simp only [Function.comp_apply, fderiv_eq_smul_deriv, smul_eq_mul, Complex.deriv_ofReal,
     Complex.real_smul, Complex.ofReal_mul, mul_one]
-  rw [deriv_mul]
+  rw [deriv_mul (by fun_prop) (by fun_prop)]
   simp only [deriv_const', zero_mul, deriv_id'', mul_one, zero_add]
-  rw [deriv_physHermiteFun]
+  rw [deriv_physHermite]
   simp only [Pi.natCast_def, Pi.mul_apply, Pi.ofNat_apply, cast_ofNat, Pi.add_apply, Pi.one_apply,
     Complex.ofReal_mul, Complex.ofReal_ofNat, Complex.ofReal_add, Complex.ofReal_natCast,
     Complex.ofReal_one]
   simp only [cast_add, cast_one, add_tsub_cancel_right]
   ring
-  all_goals fun_prop
 
 lemma deriv_eigenfunction_succ (n : ℕ) :
     deriv (Q.eigenfunction (n + 1)) = fun x =>
     Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !)) •
     (((Real.sqrt (Q.m * Q.ω / Q.ℏ)) * 2 * (↑n + 1) *
-      ↑(physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))
-      + ↑(physHermiteFun (n + 1) (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) *
+      ↑(physHermite n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))
+      + ↑(physHermite (n + 1) (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) *
       (-(Q.m * Q.ω) / Q.ℏ * ↑x)) * Q.eigenfunction 0 x) := by
   funext x
   rw [eigenfunction_eq_mul_eigenfunction_zero]
@@ -129,7 +128,7 @@ lemma deriv_eigenfunction_succ (n : ℕ) :
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, one_div, mul_inv_rev, Complex.ofReal_mul,
     Complex.ofReal_inv, differentiableAt_const, deriv_mul, deriv_const', zero_mul, mul_zero,
     add_zero, zero_add, smul_eq_mul]
-  rw [deriv_physHermiteFun_succ, deriv_eigenfunction_zero]
+  rw [deriv_physHermite_succ, deriv_eigenfunction_zero]
   simp only [neg_mul, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_mul, Pi.mul_apply,
     Pi.smul_apply, smul_eq_mul]
   ring
@@ -138,11 +137,11 @@ lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) :
     deriv (fun x => deriv (Q.eigenfunction (n + 1)) x) x =
     Complex.ofReal (1/Real.sqrt (2 ^ (n + 1) * (n + 1) !)) *
       ((↑√(Q.m * Q.ω / Q.ℏ) * 2 * (↑n + 1) *
-      deriv (fun x => ↑(physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) x +
+      deriv (fun x => ↑(physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))) x +
       (-(↑Q.m * ↑Q.ω) / ↑Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ) * (4 * (↑n + 1) * x) *
-      (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) +
+      (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) +
       (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-      (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x))) * Q.eigenfunction 0 x) := by
+      (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x))) * Q.eigenfunction 0 x) := by
   rw [deriv_eigenfunction_succ]
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, one_div, mul_inv_rev, Complex.ofReal_mul,
     Complex.ofReal_inv, smul_eq_mul, differentiableAt_const, deriv_const_mul_field',
@@ -161,7 +160,7 @@ lemma deriv_deriv_eigenfunction_succ (n : ℕ) (x : ℝ) :
     deriv_add, zero_add]
   rw [deriv_mul (by fun_prop) (by fun_prop)]
   simp only [deriv_mul_const_field', Complex.deriv_ofReal, mul_one]
-  rw [deriv_physHermiteFun_succ]
+  rw [deriv_physHermite_succ]
   simp only
   ring
 
@@ -173,7 +172,7 @@ lemma deriv_deriv_eigenfunction_one (x : ℝ) :
         (2 * (√(Q.m * Q.ω / Q.ℏ) * x)))) * Q.eigenfunction 0 x) := by
   rw [deriv_deriv_eigenfunction_succ]
   congr 2
-  simp [physHermiteFun_eq_aeval_physHermite, physHermite_one, Polynomial.aeval]
+  simp [physHermite_one, Polynomial.aeval]
 
 lemma schrodingerOperator_eigenfunction_one (x : ℝ) :
     Q.schrodingerOperator (Q.eigenfunction 1) x=
@@ -186,7 +185,7 @@ lemma schrodingerOperator_eigenfunction_one (x : ℝ) :
   have hℏ' := Complex.ofReal_ne_zero.mpr Q.ℏ_ne_zero
   rw [Q.eigenfunction_eq_mul_eigenfunction_zero 1]
   simp only [pow_one, factorial_one, cast_one, mul_one, one_div, Complex.ofReal_inv,
-    physHermiteFun_eq_aeval_physHermite, Polynomial.aeval, physHermite_one,
+    Polynomial.aeval, physHermite_one,
     Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_mul, Polynomial.eval₂_ofNat, Polynomial.eval₂_X,
     Complex.ofReal_mul, Complex.ofReal_ofNat]
   ring_nf
@@ -201,46 +200,51 @@ lemma deriv_deriv_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
   trans Complex.ofReal (1/Real.sqrt (2 ^ (n + 1 + 1) * (n + 1 + 1) !)) *
         (((- Q.m * Q.ω / Q.ℏ) * (2 * (n + 2)
         + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2)) *
-        (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) * Q.eigenfunction 0 x)
-  rw [deriv_deriv_eigenfunction_succ]
-  congr 2
-  trans (√(Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (√(Q.m * Q.ω / Q.ℏ) *
-    2 * (n + 1) * (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) +
-    (-(Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) *
-    (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) +
-    (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-    (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
-  · rw [deriv_physHermiteFun_succ]
-    simp
-  trans ((Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (2 * (n + 1) *
-      (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) +
-      (- (Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) *
-      (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) +
+        (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) * Q.eigenfunction 0 x)
+  · rw [deriv_deriv_eigenfunction_succ]
+    congr 2
+    trans (√(Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (√(Q.m * Q.ω / Q.ℏ) *
+      2 * (n + 1) * (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))) +
+      (-(Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) *
+      (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) +
       (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
-      (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
-  · congr 2
-    trans (↑√(Q.m * Q.ω / Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ)) * 2 * (↑n + 1 + 1) *
-    (2 * (↑n + 1) * ↑(physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)))
+      (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
+    · rw [deriv_physHermite_succ]
+      simp
+    trans ((Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (2 * (n + 1) *
+        (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x))) +
+        (- (Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) *
+        (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) +
+        (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) *
+        (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
+    · congr 2
+      trans (↑√(Q.m * Q.ω / Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ)) * 2 * (↑n + 1 + 1) *
+      (2 * (↑n + 1) * ↑(physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)))
+      · ring
+      congr 3
+      rw [← Complex.ofReal_mul, ← Complex.ofReal_mul, ← Complex.ofReal_div]
+      congr 1
+      refine Real.mul_self_sqrt ?_
+      refine div_nonneg ?_ (le_of_lt Q.hℏ)
+      exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
+    trans (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 1 + 1) *
+          (2 * (√(Q.m * Q.ω / Q.ℏ) * x) * (physHermite (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) -
+          2 * (n + 1) * (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)))
+          + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
     · ring
-    congr 3
-    rw [← Complex.ofReal_mul, ← Complex.ofReal_mul, ← Complex.ofReal_div]
-    congr 1
-    refine Real.mul_self_sqrt ?_
-    refine div_nonneg ?_ ?_
-    exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω)
-    exact le_of_lt Q.hℏ
-  trans (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 1 + 1) *
-        (2 * (√(Q.m * Q.ω / Q.ℏ) * x) * (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) -
-        2 * (n + 1) * (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)))
-        + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
-  · ring
-  trans (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 1 + 1) * (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))
-        + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
-  · congr
-    conv_rhs =>
-      rw [physHermiteFun_succ]
-    simp
-  ring
+    trans (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 1 + 1) * (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))
+          + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermite (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x)))
+    · congr
+      conv_rhs =>
+        rw [physHermite_succ]
+      simp only [nsmul_eq_mul, cast_ofNat, derivative_physHermite, add_tsub_cancel_right, cast_add,
+        cast_one, map_sub, map_mul, Polynomial.aeval_X, map_add, map_natCast, map_one,
+        Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_add, Complex.ofReal_natCast,
+        Complex.ofReal_one]
+      simp only [Polynomial.aeval, Polynomial.eval₂AlgHom'_apply, Polynomial.eval₂_ofNat,
+        Complex.ofReal_ofNat, sub_right_inj]
+      ring
+    ring
   · rw [Q.eigenfunction_eq_mul_eigenfunction_zero (n + 2)]
     ring
 
@@ -258,7 +262,7 @@ lemma schrodingerOperator_eigenfunction_succ_succ (n : ℕ) (x : ℝ) :
 /-- The `n`th eigenfunction satisfies the time-independent Schrodinger equation with
   respect to the `n`th eigenvalue. That is to say for `Q` a harmonic scillator,
 
-  `Q.schrodingerOperator (Q.eigenfunction n) x =  Q.eigenValue n * Q.eigenfunction n x`.
+  `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.
 -/
diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean
index 31eaf780..4dd56e8d 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean
@@ -46,18 +46,16 @@ lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔
   rw [MemHS]
   simp only [Memℒp, Complex.norm_eq_abs, and_congr_right_iff]
   intro h1
-  rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top]
+  rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top
+    (Ne.symm (NeZero.ne' 2)) ENNReal.ofNat_ne_top]
   simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat, Integrable]
   have h0 : MeasureTheory.AEStronglyMeasurable
     (fun x => Complex.abs (f x) ^ 2) MeasureTheory.volume := by
     apply MeasureTheory.AEStronglyMeasurable.pow
-    refine Continuous.comp_aestronglyMeasurable ?_ h1
-    exact Complex.continuous_abs
+    exact Continuous.comp_aestronglyMeasurable Complex.continuous_abs h1
   simp only [h0, true_and]
   simp only [HasFiniteIntegral, enorm_pow]
   simp only [enorm, nnnorm, Complex.norm_eq_abs, Real.norm_eq_abs, Complex.abs_abs]
-  exact Ne.symm (NeZero.ne' 2)
-  exact ENNReal.ofNat_ne_top
 
 lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume) :
     AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := by
@@ -111,7 +109,8 @@ lemma mem_iff' {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f Meas
     (MeasureTheory.AEEqFun.mk f hf) MeasureTheory.volume := by
     apply MeasureTheory.AEEqFun.aestronglyMeasurable
   simp only [h1, true_and]
-  rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top]
+  rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top (Ne.symm (NeZero.ne' 2))
+    ENNReal.ofNat_ne_top]
   simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat, Integrable]
   have h0 : MeasureTheory.AEStronglyMeasurable
     (fun x => Complex.abs (f x) ^ 2) MeasureTheory.volume := by
@@ -121,8 +120,6 @@ lemma mem_iff' {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f Meas
   simp only [h0, true_and]
   simp only [HasFiniteIntegral, enorm_pow]
   simp only [enorm, nnnorm, Complex.norm_eq_abs, Real.norm_eq_abs, Complex.abs_abs]
-  exact Ne.symm (NeZero.ne' 2)
-  exact ENNReal.ofNat_ne_top
 
 /-!
 
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index 3f3bdd7b..dcc056d7 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -319,7 +319,6 @@ def harmonicOscillator : Note where
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator .complete,
     .h1 "The eigenfunctions of the Schrodinger Operator",
     .name ``PhysLean.physHermite .complete,
-    .name ``PhysLean.physHermiteFun .complete,
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction .complete,
     .h2 "Properties of the eigenfunctions",
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable .complete,