Exists global smooth W1p approx of localized Witness

theorem exists_global_smooth_W1p_approx_of_localizedWitness    {Ω : Set E} (hΩ : IsOpen Ω)    {p : ℝ} (hp : 1 < p)    {u : E → ℝ}    (hw : MemW1pWitness (ENNReal.ofReal p) u Ω)    (hu_compact : HasCompactSupport u)    (hu_sub : tsupport u ⊆ Ω) :    ∃ ψ : ℕ → E → ℝ,      (∀ n, ContDiff ℝ (⊤ : ℕ∞) (ψ n)) ∧      (∀ n, HasCompactSupport (ψ n)) ∧      Tendsto        (fun n => eLpNorm (fun x => ψ n x - u x) (ENNReal.ofReal p) volume)        atTop (nhds 0) ∧      (∀ i : Fin d,        Tendsto          (fun n =>            eLpNorm              (fun x => (fderiv ℝ (ψ n) x) (EuclideanSpace.single i 1) -                Ω.indicator (fun y => hw.weakGrad y i) x)              (ENNReal.ofReal p) volume)          atTop (nhds 0)) := by  have hu0 : MemW01p (ENNReal.ofReal p) u Ω :=    memW01p_of_memW1p_of_tsupport_subset hΩ hp hw.memW1p hu_compact hu_sub  let hwExt := zeroExtend_memW1pWitness_p (d := d) hΩ hp hu0 hw  have hu_eq_ind : Ω.indicator u = u := by    ext x    by_cases hx : x ∈ Ω    · simp [hx]    · simp [hx, zero_outside_of_tsupport_subset (Ω := Ω) hu_sub hx]  have huExt0 : MemW01p (ENNReal.ofReal p) (Ω.indicator u) Set.univ :=    zeroExtend_memW01p_p (d := d) hΩ hp hu0  rcases huExt0.2 with ⟨hw0, φ, hφ_smooth, hφ_compact, hφ_sub, hφ_fun, hφ_grad⟩  refine ⟨φ, hφ_smooth, hφ_compact, ?_, ?_⟩  · simpa [hu_eq_ind] using hφ_fun  · intro i    have hp_le : 1 ≤ p := le_of_lt hp    have hcomp :        (fun x => hw0.weakGrad x i) =ᵐ[volume.restrict Set.univ]          (fun x => (Ω.indicator (fun y => hw.weakGrad y i)) x) := by      filter_upwards [MemW1pWitness.ae_eq_p (d := d) isOpen_univ hp_le hw0 hwExt] with x hx      simpa [zeroExtend_memW1pWitness_p, hwExt] using congrArg (fun z : E => z i) hx    have hEqSeq :        (fun n =>          eLpNorm            (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) -              Ω.indicator (fun y => hw.weakGrad y i) x)            (ENNReal.ofReal p) volume) =          (fun n =>            eLpNorm              (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - hw0.weakGrad x i)              (ENNReal.ofReal p) volume) := by      funext n      refine eLpNorm_congr_ae ?_      have hcomp' :          (fun x => hw0.weakGrad x i) =ᵐ[volume]            (fun x => (Ω.indicator (fun y => hw.weakGrad y i)) x) := by        simpa [Measure.restrict_univ] using hcomp      filter_upwards [hcomp'] with x hx      simp [hx]    rw [hEqSeq]    simpa [Measure.restrict_univ] using hφ_grad i