Eigenfunction normalized

lemma eigenfunction_normalized (n : ℕ) : ⟪HilbertSpace.mk (Q.eigenfunction_memHS n),    HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 1 := by  rw [inner_mk_mk]  conv_lhs =>    enter [2, x]    rw [eigenfunction_conj, Q.eigenfunction_mul_self]  rw [MeasureTheory.integral_const_mul, integral_complex_ofReal]  have hc : (∫ (x : ℝ), physHermite n (x /Q.ξ) ^ 2 * Real.exp (- x ^ 2 / Q.ξ^2))      = ∫ (x : ℝ), (physHermite n (1/Q.ξ * x) *      physHermite n (1/Q.ξ * x)) * Real.exp (- (1/Q.ξ)^2 * x ^ 2) := by    congr    funext x    ring_nf  rw [hc, physHermite_norm_cons]  simp only [one_div, mul_inv_rev, inv_inv, ξ_abs]  have : (n ! : ℂ) ≠ 0 := Complex.ne_zero_of_re_pos <| by simpa using factorial_pos n  have := Complex.ofReal_ne_zero.mpr (ne_of_gt Q.ξ_pos)  have := Complex.ofReal_ne_zero.mpr (Real.sqrt_ne_zero'.mpr Real.pi_pos)  simp only [smul_eq_mul, Complex.ofReal_mul, Complex.ofReal_natCast, Complex.ofReal_pow,    Complex.ofReal_ofNat]  field_simp