Mul Operator adjoint eq conj

lemma mulOperator_adjoint_eq_conj {μ : Measure (Space d)} [IsFiniteMeasureOnCompacts μ]    {f : Space d → ℂ} (hf : AEStronglyMeasurable f μ) :    (𝓜 μ f)† = 𝓜 μ (conj ∘ f) := by  have hFA : (𝓜 μ f).IsFormalAdjoint (𝓜 μ (conj ∘ f)) := by    intro ψ φ    refine integral_congr_ae ?_    filter_upwards [mulOperator_apply_ae ψ, mulOperator_apply_ae φ] with x h₁ h₂    simp [h₁, h₂, mul_assoc, mul_left_comm]  refine eq_of_le_of_ge ?_ (hFA.le_adjoint <| mulOperator_hasDenseDomain hf)  refine ⟨mulOperator_adjoint_domain_le hf, fun ψ ψ' hψ ↦ ?_⟩  refine adjoint_apply_eq (mulOperator_hasDenseDomain hf) ψ fun φ ↦ ?_  rw [← inner_conj_symm, hψ, (hFA φ ψ').symm, inner_conj_symm]