Momentum Operator Unbounded is Symmetric

lemma momentumOperatorUnbounded_isSymmetric : momentumOperatorUnbounded.IsSymmetric := by  intro ψ1 ψ2  have hint : ∀ f g : 𝓢(ℝ, ℂ),      MeasureTheory.Integrable (fun x => star (f x) * g x) MeasureTheory.volume :=    fun f g => ((ContinuousLinearEquiv.integrable_comp_iff (starL' ℝ)).mpr      (SchwartzMap.integrable f)).mul_of_top_left (SchwartzMap.memLp_top g)  dsimp [momentumOperatorUnbounded]  rw [schwartzIncl_inner, schwartzIncl_inner]  conv_rhs =>    enter [2, x]    rw [momentumOperatorSchwartz_apply, ← fderiv_apply_one_eq_deriv, ← mul_assoc,      mul_comm _ (-Complex.I * ↑↑ℏ), mul_assoc]  rw [MeasureTheory.integral_const_mul, integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable,    ← MeasureTheory.integral_neg, ← MeasureTheory.integral_const_mul]  simp only [starRingEnd_apply, fderiv_star]  simp [momentumOperatorSchwartz_apply, mul_assoc]  · simp only [starRingEnd_apply, fderiv_star]    exact hint (SchwartzMap.derivCLM ℂ ℂ ψ1) ψ2  · exact hint ψ1 (SchwartzMap.derivCLM ℂ ℂ ψ2)  · exact hint ψ1 ψ2  · exact fun x _ => (SchwartzMap.differentiable ψ1).star x  · fun_prop