Mul Operator comp Restricted le

lemma mulOperator_compRestricted_le (μ : Measure (Space d)) (f g : Space d → ℂ) :    𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g) := by  constructor  · intro ψ hψ    obtain ⟨hψ, hgψ⟩ := mem_compRestricted_domain_iff.mp hψ    refine (mem_mulOperator_domain_iff.mp hgψ).ae_eq ?_    filter_upwards [mulOperator_apply_ae ⟨ψ, hψ⟩]    simp_all [mul_assoc]  · intro ψ φ hψφ    apply ext_iff.mpr    obtain ⟨hψ, hgψ⟩ := mem_compRestricted_domain_iff.mp ψ.2    filter_upwards [mulOperator_apply_ae φ, mulOperator_apply_ae ⟨ψ, hψ⟩,      mulOperator_apply_ae ⟨𝓜 μ g ⟨ψ, hψ⟩, hgψ⟩]    simp_all [mul_assoc]