Deriv eigenfunction zero

lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) =    Complex.ofReal (- 1 / Q.ξ ^2) • Complex.ofReal * Q.eigenfunction 0 := by  rw [eigenfunction_zero]  simp only [deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_neg, Algebra.smul_mul_assoc]  ext x  have h1 : deriv (fun (x : ℝ) => Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2))) x =      - x /Q.ξ^2 * Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2)) := by    rw [show (fun (x : ℝ) => Complex.exp (- x ^ 2 / (2 * Q.ξ ^ 2)))          = Complex.exp ∘ (fun (x : ℝ) => - x ^ 2 / (2 * Q.ξ ^ 2)) from rfl,      deriv_comp _ (by fun_prop) (by fun_prop)]    simp only [Complex.deriv_exp, deriv_div_const, deriv.fun_neg']    have h1' : deriv (fun x => (Complex.ofReal x) ^ 2) x = 2 * x := by      simp only [pow_two]      rw [deriv_fun_mul Complex.differentiableAt_ofReal Complex.differentiableAt_ofReal]      simp only [Complex.deriv_ofReal, one_mul, mul_one]      ring    rw [h1']    field_simp  simp only [Pi.smul_apply, Pi.mul_apply, smul_eq_mul]  rw [h1]  simp only [Real.sqrt_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,    Complex.ofReal_one, Complex.ofReal_pow]  ring