Exists smooth W12 approx on unit Ball

theorem exists_smooth_W12_approx_on_unitBall    {u : E → ℝ}    (hw : MemW1pWitness 2 u (Metric.ball (0 : E) 1)) :    ∃ ψ : ℕ → E → ℝ,      (∀ n, ContDiff ℝ (⊤ : ℕ∞) (ψ n)) ∧      (∀ n, HasCompactSupport (ψ n)) ∧      Tendsto        (fun n => eLpNorm (fun x => ψ n x - u x)          2 (volume.restrict (Metric.ball (0 : E) 1)))        atTop (nhds 0) ∧      (∀ i : Fin d,        Tendsto          (fun n => eLpNorm            (fun x => (fderiv ℝ (ψ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i)            2 (volume.restrict (Metric.ball (0 : E) 1)))          atTop (nhds 0)) := by  let hw' : MemW1pWitness (ENNReal.ofReal (2 : ℝ)) u (Metric.ball (0 : E) 1) :=    { memLp := by        simpa using hw.memLp      weakGrad := hw.weakGrad      weakGrad_component_memLp := by        intro i        simpa using hw.weakGrad_component_memLp i      isWeakGrad := hw.isWeakGrad }  rcases exists_smooth_W1p_approx_on_unitBall (d := d) (p := (2 : ℝ)) (by norm_num) hw' with    ⟨ψ, hψ_smooth, hψ_compact, hψ_fun, hψ_grad⟩  refine ⟨ψ, hψ_smooth, hψ_compact, ?_, ?_⟩  · simpa [hw'] using hψ_fun  · intro i    simpa [hw'] using hψ_grad i