From c0c0f28049ddd44d5882781cb3ed50af85227687 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Feb 2025 16:59:46 +0000
Subject: [PATCH] refactor: Simplify terminal simp

---
 .../OneDimension/HarmonicOscillator/Eigenfunction.lean         | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
index 5be53cce..a93a5dc2 100644
--- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
+++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean
@@ -100,8 +100,7 @@ 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 !) *