refactor: Simplify terminal simp

HEPLean · Feb 26, 2025 · c0c0f28 · c0c0f28
1 parent 1b28ae3
commit c0c0f28
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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 !) *