Mul Operator has Dense Domain

lemma mulOperator_hasDenseDomain    {μ : Measure (Space d)} {f : Space d → ℂ} (hf : AEStronglyMeasurable f μ) :    (𝓜 μ f).HasDenseDomain := by  intro ψ  apply mem_closure_iff_seq_limit.mpr  obtain ⟨u, hu, hfu⟩ := hf.aemeasurable  let s : ℕ → Set (Space d) := fun n ↦ u ⁻¹' (Metric.closedBall 0 n)  let φ : ℕ → SpaceDHilbertSpace d μ := fun n ↦    mk ((memHS_coe ψ).indicator (Ω := s n) (by measurability))  have hφ : ∀ n, φ n =ᵐ[μ] (s n).indicator ψ := fun n ↦ coeFn_mk _  use φ  constructor  · intro n    refine memHS_iff.mpr ⟨by measurability, by measurability, ?_⟩    refine HasFiniteIntegral.mono (memHS_iff.mp <| memHS_coe (n • φ n)).2.2 ?_    filter_upwards [hfu, coeFn_smul n (φ n), hφ n] with x h₁ h₂ h₃    by_cases hx : x ∈ s n    · simp_rw [norm_pow, norm_norm, sq_le_sq, abs_norm]      calc        _ = ‖u x‖ * ‖φ n x‖ := by simp [h₁]        _ ≤ n * ‖φ n x‖ := mul_le_mul_of_nonneg_right (by simp_all [s]) (norm_nonneg _)        _ = ‖(n • φ n) x‖ := by simp [h₂, ← Nat.cast_smul_eq_nsmul ℂ]    · simp [h₃, hx]  · apply tendsto_sub_nhds_zero_iff.mp    apply tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq.mpr    have h : ∀ n, ∫⁻ x, ‖(φ n - ψ) x‖ₑ ^ 2 ∂μ = ∫⁻ x, ‖(s n)ᶜ.indicator ψ x‖ₑ ^ 2 ∂μ := by      intro n      refine lintegral_congr_ae ?_      filter_upwards [coeFn_sub (φ n) ψ, hφ n] with x h₁ h₂      by_cases hx : x ∈ s n <;> simp [hx, h₁, h₂]    simp_rw [h]    rw [← MeasureTheory.lintegral_zero (α := Space d) (μ := μ)]    refine tendsto_lintegral_of_dominated_convergence' (fun x ↦ ‖ψ x‖ₑ ^ 2) ?_ ?_ ?_ ?_    · measurability    · intro n      filter_upwards with x      by_cases hx : x ∈ s n <;> simp [hx]    · have : ∫⁻ x, ‖‖ψ x‖ ^ 2‖ₑ ∂μ ≠ ⊤ := (memHS_iff.mp <| memHS_coe ψ).2.2.ne      simp_all    · filter_upwards with x      rw [← zero_pow two_ne_zero, ← enorm_zero (E := ℂ)]      refine ENNReal.Tendsto.pow (Tendsto.enorm (tendsto_nhds_of_eventually_eq ?_))      refine eventually_atTop.mpr ⟨⌈‖u x‖⌉₊, fun n hn ↦ ?_⟩      suffices ‖u x‖ ≤ n by simp [s, this]      exact (Nat.le_ceil _).trans (by exact_mod_cast hn)