Exists smooth W1p approx on unit Ball

theorem exists_smooth_W1p_approx_on_unitBall    {p : ℝ} (hp : 1 < p) {u : E → ℝ}    (hw : MemW1pWitness (ENNReal.ofReal p) u (Metric.ball (0 : E) 1)) :    ∃ ψ : ℕ → E → ℝ,      (∀ n, ContDiff ℝ (⊤ : ℕ∞) (ψ n)) ∧      (∀ n, HasCompactSupport (ψ n)) ∧      Tendsto        (fun n => eLpNorm (fun x => ψ n x - u x)          (ENNReal.ofReal p) (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)            (ENNReal.ofReal p) (volume.restrict (Metric.ball (0 : E) 1)))          atTop (nhds 0)) := by  let eps : ℕ → ℝ := fun n => ((n : ℝ) + 1)⁻¹  have heps_pos : ∀ n, 0 < eps n := by    intro n    exact inv_pos.mpr (by positivity)  choose ψ hψ using    fun n => exists_smooth_W1p_oneShot_on_unitBall (d := d) (p := p) hp hw      (ε := eps n) (heps_pos n)  have hψ_smooth : ∀ n, ContDiff ℝ (⊤ : ℕ∞) (ψ n) := fun n => (hψ n).1  have hψ_compact : ∀ n, HasCompactSupport (ψ n) := fun n => (hψ n).2.1  have hψ_fun :      ∀ n,        eLpNorm (fun x => ψ n x - u x)          (ENNReal.ofReal p) (volume.restrict (Metric.ball (0 : E) 1)) <          ENNReal.ofReal (eps n) := fun n => (hψ n).2.2.1  have hψ_grad :      ∀ n (i : Fin d),        eLpNorm          (fun x => (fderiv ℝ (ψ n) x) (EuclideanSpace.single i 1) - hw.weakGrad x i)          (ENNReal.ofReal p) (volume.restrict (Metric.ball (0 : E) 1)) <          ENNReal.ofReal (eps n) := fun n => (hψ n).2.2.2  refine ⟨ψ, hψ_smooth, hψ_compact, ?_, ?_⟩  · have h_eps_tendsto_real' :        Tendsto (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1)) atTop (nhds (0 : ℝ)) := by      exact tendsto_one_div_add_atTop_nhds_zero_nat    have h_eps_tendsto_real : Tendsto eps atTop (nhds (0 : ℝ)) := by      simpa [eps] using h_eps_tendsto_real'    have h_eps_tendsto : Tendsto (fun n => ENNReal.ofReal (eps n)) atTop (nhds 0) := by      simpa using (ENNReal.continuous_ofReal.tendsto (0 : ℝ)).comp h_eps_tendsto_real    refine ENNReal.tendsto_nhds_zero.2 ?_    intro ε hε    filter_upwards [ENNReal.tendsto_nhds_zero.1 h_eps_tendsto ε hε] with n hn    exact le_trans (le_of_lt (hψ_fun n)) hn  · intro i    have h_eps_tendsto_real' :        Tendsto (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1)) atTop (nhds (0 : ℝ)) := by      exact tendsto_one_div_add_atTop_nhds_zero_nat    have h_eps_tendsto_real : Tendsto eps atTop (nhds (0 : ℝ)) := by      simpa [eps] using h_eps_tendsto_real'    have h_eps_tendsto : Tendsto (fun n => ENNReal.ofReal (eps n)) atTop (nhds 0) := by      simpa using (ENNReal.continuous_ofReal.tendsto (0 : ℝ)).comp h_eps_tendsto_real    refine ENNReal.tendsto_nhds_zero.2 ?_    intro ε hε    filter_upwards [ENNReal.tendsto_nhds_zero.1 h_eps_tendsto ε hε] with n hn    exact le_trans (le_of_lt (hψ_grad n i)) hn